let V be RealLinearSpace; 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; ( ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) implies w,u,v are_LinDep )
A1:
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;
( are_Prop u,v implies w,u,v are_LinDep )
A2:
0 * w = 0. V
by RLVECT_1:10;
assume
are_Prop u,
v
;
w,u,v are_LinDep
then consider a,
b being
Real such that A3:
a * u = b * v
and A4:
a <> 0
and
b <> 0
;
0. V =
(a * u) + (- (b * v))
by A3, RLVECT_1:5
.=
(a * u) + ((- 1) * (b * v))
by RLVECT_1:16
.=
(a * u) + (((- 1) * b) * v)
by RLVECT_1:def 7
;
then
0. V = ((0 * w) + (a * u)) + (((- 1) * b) * v)
by A2;
hence
w,
u,
v are_LinDep
by A4;
verum
end;
A5:
now ( are_Prop w,u & ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) implies w,u,v are_LinDep )assume
are_Prop w,
u
;
( ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) implies w,u,v are_LinDep )then
v,
w,
u are_LinDep
by A1;
hence
( (
are_Prop u,
v or
are_Prop w,
u or
are_Prop v,
w ) implies
w,
u,
v are_LinDep )
by Th5;
verum end;
A6:
now ( are_Prop v,w & ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) implies w,u,v are_LinDep )assume
are_Prop v,
w
;
( ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) implies w,u,v are_LinDep )then
u,
v,
w are_LinDep
by A1;
hence
( (
are_Prop u,
v or
are_Prop w,
u or
are_Prop v,
w ) implies
w,
u,
v are_LinDep )
by Th5;
verum end;
assume
( are_Prop u,v or are_Prop w,u or are_Prop v,w )
; w,u,v are_LinDep
hence
w,u,v are_LinDep
by A1, A5, A6; verum