let V be RealLinearSpace; for p, q, u, v, w being Element of V st not are_Prop p,q & p,q,u are_LinDep & p,q,v are_LinDep & p,q,w are_LinDep & not p is zero & not q is zero holds
u,v,w are_LinDep
let p, q, u, v, w be Element of V; ( not are_Prop p,q & p,q,u are_LinDep & p,q,v are_LinDep & p,q,w are_LinDep & not p is zero & not q is zero implies u,v,w are_LinDep )
assume that
A1:
not are_Prop p,q
and
A2:
p,q,u are_LinDep
and
A3:
p,q,v are_LinDep
and
A4:
p,q,w are_LinDep
and
A5:
( not p is zero & not q is zero )
; u,v,w are_LinDep
consider a1, b1 being Real such that
A6:
u = (a1 * p) + (b1 * q)
by A1, A2, A5, Th6;
consider a3, b3 being Real such that
A7:
w = (a3 * p) + (b3 * q)
by A1, A4, A5, Th6;
consider a2, b2 being Real such that
A8:
v = (a2 * p) + (b2 * q)
by A1, A3, A5, Th6;
set a = (a2 * b3) - (a3 * b2);
set b = (- (a1 * b3)) + (a3 * b1);
set c = (a1 * b2) - (a2 * b1);
A9:
now ( (a2 * b3) - (a3 * b2) = 0 & (- (a1 * b3)) + (a3 * b1) = 0 & (a1 * b2) - (a2 * b1) = 0 implies u,v,w are_LinDep )A10:
(
w = 0. V &
v = 0. V & (
are_Prop v,
w or
v = 0. V or
w = 0. V ) implies
u,
v,
w are_LinDep )
by Th10;
A11:
(
w = 0. V &
u = 0. V & (
are_Prop v,
w or
v = 0. V or
w = 0. V ) implies
u,
v,
w are_LinDep )
by Th10;
A12:
(
u = 0. V &
v = 0. V & (
are_Prop v,
w or
v = 0. V or
w = 0. V ) implies
u,
v,
w are_LinDep )
by Th10;
A13:
( ( (
w = 0. V &
are_Prop u,
v &
w = 0. V ) or (
u = 0. V &
u = 0. V &
are_Prop v,
w ) or (
are_Prop w,
u &
v = 0. V &
v = 0. V ) ) implies
u,
v,
w are_LinDep )
by Th11;
A14:
(
are_Prop w,
u &
are_Prop u,
v &
are_Prop v,
w implies
u,
v,
w are_LinDep )
by Th11;
assume that A15:
(a2 * b3) - (a3 * b2) = 0
and A16:
(- (a1 * b3)) + (a3 * b1) = 0
and A17:
(a1 * b2) - (a2 * b1) = 0
;
u,v,w are_LinDep
0 = (a3 * b1) - (a1 * b3)
by A16;
hence
u,
v,
w are_LinDep
by A1, A5, A6, A8, A7, A15, A17, A14, A13, A11, A10, A12, Th9;
verum end;
( 0. V = (((((a2 * b3) - (a3 * b2)) * a1) + (((- (a1 * b3)) + (a3 * b1)) * a2)) + (((a1 * b2) - (a2 * b1)) * a3)) * p & 0. V = (((((a2 * b3) - (a3 * b2)) * b1) + (((- (a1 * b3)) + (a3 * b1)) * b2)) + (((a1 * b2) - (a2 * b1)) * b3)) * q )
by RLVECT_1:10;
then A18:
0. V = ((((((a2 * b3) - (a3 * b2)) * a1) + (((- (a1 * b3)) + (a3 * b1)) * a2)) + (((a1 * b2) - (a2 * b1)) * a3)) * p) + ((((((a2 * b3) - (a3 * b2)) * b1) + (((- (a1 * b3)) + (a3 * b1)) * b2)) + (((a1 * b2) - (a2 * b1)) * b3)) * q)
;
(((((a2 * b3) - (a3 * b2)) * a1) + (((- (a1 * b3)) + (a3 * b1)) * a2)) + (((a1 * b2) - (a2 * b1)) * a3)) * p = (((((a2 * b3) - (a3 * b2)) * a1) * p) + ((((- (a1 * b3)) + (a3 * b1)) * a2) * p)) + ((((a1 * b2) - (a2 * b1)) * a3) * p)
by Lm3;
then
0. V = ((((((a2 * b3) - (a3 * b2)) * a1) * p) + ((((- (a1 * b3)) + (a3 * b1)) * a2) * p)) + ((((a1 * b2) - (a2 * b1)) * a3) * p)) + ((((((a2 * b3) - (a3 * b2)) * b1) * q) + ((((- (a1 * b3)) + (a3 * b1)) * b2) * q)) + ((((a1 * b2) - (a2 * b1)) * b3) * q))
by A18, Lm3;
then A19:
0. V = ((((((a2 * b3) - (a3 * b2)) * a1) * p) + ((((a2 * b3) - (a3 * b2)) * b1) * q)) + (((((- (a1 * b3)) + (a3 * b1)) * a2) * p) + ((((- (a1 * b3)) + (a3 * b1)) * b2) * q))) + (((((a1 * b2) - (a2 * b1)) * a3) * p) + ((((a1 * b2) - (a2 * b1)) * b3) * q))
by Lm4;
A20:
((((a1 * b2) - (a2 * b1)) * a3) * p) + ((((a1 * b2) - (a2 * b1)) * b3) * q) = ((a1 * b2) - (a2 * b1)) * ((a3 * p) + (b3 * q))
by Lm5;
( ((((a2 * b3) - (a3 * b2)) * a1) * p) + ((((a2 * b3) - (a3 * b2)) * b1) * q) = ((a2 * b3) - (a3 * b2)) * ((a1 * p) + (b1 * q)) & ((((- (a1 * b3)) + (a3 * b1)) * a2) * p) + ((((- (a1 * b3)) + (a3 * b1)) * b2) * q) = ((- (a1 * b3)) + (a3 * b1)) * ((a2 * p) + (b2 * q)) )
by Lm5;
hence
u,v,w are_LinDep
by A6, A8, A7, A19, A20, A9; verum