let V be RealLinearSpace; :: thesis: for u, v, w being Element of V st ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) holds
w,u,v are_LinDep
let u, v, w be Element of V; :: thesis: ( ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) implies w,u,v are_LinDep )
assume A1:
( are_Prop u,v or are_Prop w,u or are_Prop v,w )
; :: thesis: w,u,v are_LinDep
A2:
for u, v, w being Element of V st are_Prop u,v holds
w,u,v are_LinDep
proof
let u,
v,
w be
Element of
V;
:: thesis: ( are_Prop u,v implies w,u,v are_LinDep )
assume
are_Prop u,
v
;
:: thesis: w,u,v are_LinDep
then consider a,
b being
Real such that A3:
(
a * u = b * v &
a <> 0 &
b <> 0 )
by Def2;
A4:
0. V =
(a * u) + (- (b * v))
by A3, RLVECT_1:16
.=
(a * u) + ((- 1) * (b * v))
by RLVECT_1:29
.=
(a * u) + (((- 1) * b) * v)
by RLVECT_1:def 9
;
0 * w = 0. V
by RLVECT_1:23;
then
0. V = ((0 * w) + (a * u)) + (((- 1) * b) * v)
by A4, RLVECT_1:10;
hence
w,
u,
v are_LinDep
by A3, Def3;
:: thesis: verum
end;
hence
w,u,v are_LinDep
by A1, A2, A5; :: thesis: verum