let V be RealLinearSpace; :: thesis: for p, q, r, s being Element of V st ( for w being Element of V ex a, b, c, d being Real st w = (((a * p) + (b * q)) + (c * r)) + (d * s) ) & ( for a, b, c, d being Real st (((a * p) + (b * q)) + (c * r)) + (d * s) = 0. V holds
( a = 0 & b = 0 & c = 0 & d = 0 ) ) holds
for u, v being Element of V st not u is zero & not v is zero holds
ex y, w being Element of V st
( u,v,w are_LinDep & q,r,y are_LinDep & p,w,y are_LinDep & not y is zero & not w is zero )
let p, q, r, s be Element of V; :: thesis: ( ( for w being Element of V ex a, b, c, d being Real st w = (((a * p) + (b * q)) + (c * r)) + (d * s) ) & ( for a, b, c, d being Real st (((a * p) + (b * q)) + (c * r)) + (d * s) = 0. V holds
( a = 0 & b = 0 & c = 0 & d = 0 ) ) implies for u, v being Element of V st not u is zero & not v is zero holds
ex y, w being Element of V st
( u,v,w are_LinDep & q,r,y are_LinDep & p,w,y are_LinDep & not y is zero & not w is zero ) )
assume A1: ( ( for w being Element of V ex a, b, c, d being Real st w = (((a * p) + (b * q)) + (c * r)) + (d * s) ) & ( for a, b, c, d being Real st (((a * p) + (b * q)) + (c * r)) + (d * s) = 0. V holds
( a = 0 & b = 0 & c = 0 & d = 0 ) ) ) ; :: thesis: for u, v being Element of V st not u is zero & not v is zero holds
ex y, w being Element of V st
( u,v,w are_LinDep & q,r,y are_LinDep & p,w,y are_LinDep & not y is zero & not w is zero )
let u, v be Element of V; :: thesis: ( not u is zero & not v is zero implies ex y, w being Element of V st
( u,v,w are_LinDep & q,r,y are_LinDep & p,w,y are_LinDep & not y is zero & not w is zero ) )
assume A2: ( not u is zero & not v is zero ) ; :: thesis: ex y, w being Element of V st
( u,v,w are_LinDep & q,r,y are_LinDep & p,w,y are_LinDep & not y is zero & not w is zero )
A3: ( not p is zero & not q is zero & not are_Prop p,q & not r is zero & not s is zero & not are_Prop r,s & not p,q,r are_LinDep & not r,s,p are_LinDep ) by A1, Th2;
consider a1, b1, c1, d1 being Real such that
A4: u = (((a1 * p) + (b1 * q)) + (c1 * r)) + (d1 * s) by A1;
consider a2, b2, c2, d2 being Real such that
A5: v = (((a2 * p) + (b2 * q)) + (c2 * r)) + (d2 * s) by A1;
A6: for a3, b3 being Real holds (a3 * u) + (b3 * v) = (((((a3 * a1) + (b3 * a2)) * p) + (((a3 * b1) + (b3 * b2)) * q)) + (((a3 * c1) + (b3 * c2)) * r)) + (((a3 * d1) + (b3 * d2)) * s)
proof
let a3, b3 be Real; :: thesis: (a3 * u) + (b3 * v) = (((((a3 * a1) + (b3 * a2)) * p) + (((a3 * b1) + (b3 * b2)) * q)) + (((a3 * c1) + (b3 * c2)) * r)) + (((a3 * d1) + (b3 * d2)) * s)
a3 * u = ((((a3 * a1) * p) + ((a3 * b1) * q)) + ((a3 * c1) * r)) + ((a3 * d1) * s) by A4, Lm4;
hence (a3 * u) + (b3 * v) = (((((a3 * a1) * p) + ((a3 * b1) * q)) + ((a3 * c1) * r)) + ((a3 * d1) * s)) + (((((b3 * a2) * p) + ((b3 * b2) * q)) + ((b3 * c2) * r)) + ((b3 * d2) * s)) by A5, Lm4
.= (((((a3 * a1) * p) + ((b3 * a2) * p)) + (((a3 * b1) * q) + ((b3 * b2) * q))) + (((a3 * c1) * r) + ((b3 * c2) * r))) + (((a3 * d1) * s) + ((b3 * d2) * s)) by Lm5
.= (((((a3 * a1) + (b3 * a2)) * p) + (((a3 * b1) * q) + ((b3 * b2) * q))) + (((a3 * c1) * r) + ((b3 * c2) * r))) + (((a3 * d1) * s) + ((b3 * d2) * s)) by RLVECT_1:def 9
.= (((((a3 * a1) + (b3 * a2)) * p) + (((a3 * b1) + (b3 * b2)) * q)) + (((a3 * c1) * r) + ((b3 * c2) * r))) + (((a3 * d1) * s) + ((b3 * d2) * s)) by RLVECT_1:def 9
.= (((((a3 * a1) + (b3 * a2)) * p) + (((a3 * b1) + (b3 * b2)) * q)) + (((a3 * c1) + (b3 * c2)) * r)) + (((a3 * d1) * s) + ((b3 * d2) * s)) by RLVECT_1:def 9
.= (((((a3 * a1) + (b3 * a2)) * p) + (((a3 * b1) + (b3 * b2)) * q)) + (((a3 * c1) + (b3 * c2)) * r)) + (((a3 * d1) + (b3 * d2)) * s) by RLVECT_1:def 9 ;
:: thesis: verum
end;
A7: not are_Prop q,r by A3, ANPROJ_1:16;
A8: now
assume A9: are_Prop u,v ; :: thesis: ex y, w being Element of V st
( u,v,w are_LinDep & q,r,y are_LinDep & p,w,y are_LinDep & not y is zero & not w is zero )
A10: ( q,r,q are_LinDep & p,p,q are_LinDep ) by ANPROJ_1:16;
u,v,p are_LinDep by A9, ANPROJ_1:16;
hence ex y, w being Element of V st
( u,v,w are_LinDep & q,r,y are_LinDep & p,w,y are_LinDep & not y is zero & not w is zero ) by A3, A10; :: thesis: verum
end;
now
assume A11: not are_Prop u,v ; :: thesis: ex y, w being Element of V st
( u,v,w are_LinDep & q,r,y are_LinDep & p,w,y are_LinDep & not y is zero & not w is zero )
ex w being Element of V st
( not w is zero & u,v,w are_LinDep & ex A, B, C being Real st w = ((A * p) + (B * q)) + (C * r) )
proof
A12: now
assume A13: d1 = 0 ; :: thesis: ex w, w being Element of V st
( not w is zero & u,v,w are_LinDep & ex A, B, C being Real st w = ((A * p) + (B * q)) + (C * r) )
take w = u; :: thesis: ex w being Element of V st
( not w is zero & u,v,w are_LinDep & ex A, B, C being Real st w = ((A * p) + (B * q)) + (C * r) )
A14: u,v,w are_LinDep by ANPROJ_1:16;
w = (((a1 * p) + (b1 * q)) + (c1 * r)) + (0. V) by A4, A13, RLVECT_1:23
.= ((a1 * p) + (b1 * q)) + (c1 * r) by RLVECT_1:10 ;
hence ex w being Element of V st
( not w is zero & u,v,w are_LinDep & ex A, B, C being Real st w = ((A * p) + (B * q)) + (C * r) ) by A2, A14; :: thesis: verum
end;
A15: now
assume A16: d2 = 0 ; :: thesis: ex w, w being Element of V st
( not w is zero & u,v,w are_LinDep & ex A, B, C being Real st w = ((A * p) + (B * q)) + (C * r) )
take w = v; :: thesis: ex w being Element of V st
( not w is zero & u,v,w are_LinDep & ex A, B, C being Real st w = ((A * p) + (B * q)) + (C * r) )
A17: u,v,w are_LinDep by ANPROJ_1:16;
w = (((a2 * p) + (b2 * q)) + (c2 * r)) + (0. V) by A5, A16, RLVECT_1:23
.= ((a2 * p) + (b2 * q)) + (c2 * r) by RLVECT_1:10 ;
hence ex w being Element of V st
( not w is zero & u,v,w are_LinDep & ex A, B, C being Real st w = ((A * p) + (B * q)) + (C * r) ) by A2, A17; :: thesis: verum
end;
now
assume A18: ( d1 <> 0 & d2 <> 0 ) ; :: thesis: ex w being Element of V st
( not w is zero & u,v,w are_LinDep & ex A, B, C being Real st w = ((A * p) + (B * q)) + (C * r) )
set a3 = - (d2 * (d1 " ));
set b3 = 1;
set w = ((- (d2 * (d1 " ))) * u) + (1 * v);
((- (d2 * (d1 " ))) * d1) + (1 * d2) = (- (d2 * ((d1 " ) * d1))) + d2
.= (- (d2 * 1)) + d2 by A18, XCMPLX_0:def 7
.= 0 ;
then A19: ((- (d2 * (d1 " ))) * u) + (1 * v) = ((((((- (d2 * (d1 " ))) * a1) + (1 * a2)) * p) + ((((- (d2 * (d1 " ))) * b1) + (1 * b2)) * q)) + ((((- (d2 * (d1 " ))) * c1) + (1 * c2)) * r)) + (0 * s) by A6
.= ((((((- (d2 * (d1 " ))) * a1) + (1 * a2)) * p) + ((((- (d2 * (d1 " ))) * b1) + (1 * b2)) * q)) + ((((- (d2 * (d1 " ))) * c1) + (1 * c2)) * r)) + (0. V) by RLVECT_1:23
.= (((((- (d2 * (d1 " ))) * a1) + (1 * a2)) * p) + ((((- (d2 * (d1 " ))) * b1) + (1 * b2)) * q)) + ((((- (d2 * (d1 " ))) * c1) + (1 * c2)) * r) by RLVECT_1:10 ;
A20: u,v,((- (d2 * (d1 " ))) * u) + (1 * v) are_LinDep by A2, A11, ANPROJ_1:11;
set A = ((- (d2 * (d1 " ))) * a1) + (1 * a2);
set B = ((- (d2 * (d1 " ))) * b1) + (1 * b2);
set C = ((- (d2 * (d1 " ))) * c1) + (1 * c2);
A21: ((- (d2 * (d1 " ))) * u) + (1 * v) = ((((((- (d2 * (d1 " ))) * a1) + (1 * a2)) * p) + ((((- (d2 * (d1 " ))) * b1) + (1 * b2)) * q)) + ((((- (d2 * (d1 " ))) * c1) + (1 * c2)) * r)) + (0. V) by A19, RLVECT_1:10
.= ((((((- (d2 * (d1 " ))) * a1) + (1 * a2)) * p) + ((((- (d2 * (d1 " ))) * b1) + (1 * b2)) * q)) + ((((- (d2 * (d1 " ))) * c1) + (1 * c2)) * r)) + (0 * s) by RLVECT_1:23 ;
A22: ( ((- (d2 * (d1 " ))) * a1) + (1 * a2) <> 0 or ((- (d2 * (d1 " ))) * b1) + (1 * b2) <> 0 or ((- (d2 * (d1 " ))) * c1) + (1 * c2) <> 0 )
proof
assume ( not ((- (d2 * (d1 " ))) * a1) + (1 * a2) <> 0 & not ((- (d2 * (d1 " ))) * b1) + (1 * b2) <> 0 & not ((- (d2 * (d1 " ))) * c1) + (1 * c2) <> 0 ) ; :: thesis: contradiction
then A23: ( - (- ((d2 * (d1 " )) * a1)) = a2 & - (- ((d2 * (d1 " )) * b1)) = b2 & - (- ((d2 * (d1 " )) * c1)) = c2 ) ;
A24: (d2 * (d1 " )) * d1 = d2
proof
thus (d2 * (d1 " )) * d1 = d2 * ((d1 " ) * d1)
.= d2 * 1 by A18, XCMPLX_0:def 7
.= d2 ; :: thesis: verum
end;
A25: d2 * (d1 " ) <> 0 (d2 * (d1 " )) * u = v by A4, A5, A23, A24, Lm4;
hence contradiction by A11, A25, ANPROJ_1:5; :: thesis: verum
end;
not ((- (d2 * (d1 " ))) * u) + (1 * v) is zero
proof
assume ((- (d2 * (d1 " ))) * u) + (1 * v) is zero ; :: thesis: contradiction
then ((- (d2 * (d1 " ))) * u) + (1 * v) = 0. V by STRUCT_0:def 15;
hence contradiction by A1, A21, A22; :: thesis: verum
end;
hence ex w being Element of V st
( not w is zero & u,v,w are_LinDep & ex A, B, C being Real st w = ((A * p) + (B * q)) + (C * r) ) by A19, A20; :: thesis: verum
end;
hence ex w being Element of V st
( not w is zero & u,v,w are_LinDep & ex A, B, C being Real st w = ((A * p) + (B * q)) + (C * r) ) by A12, A15; :: thesis: verum
end;
then consider w being Element of V such that
A26: ( not w is zero & u,v,w are_LinDep & ex A, B, C being Real st w = ((A * p) + (B * q)) + (C * r) ) ;
consider A, B, C being Real such that
A27: w = ((A * p) + (B * q)) + (C * r) by A26;
A28: now
assume are_Prop p,w ; :: thesis: ex y, w being Element of V st
( u,v,w are_LinDep & q,r,y are_LinDep & p,w,y are_LinDep & not y is zero & not w is zero )
then ( q,r,q are_LinDep & p,w,q are_LinDep ) by ANPROJ_1:16;
hence ex y, w being Element of V st
( u,v,w are_LinDep & q,r,y are_LinDep & p,w,y are_LinDep & not y is zero & not w is zero ) by A3, A26; :: thesis: verum
end;
now
assume A29: not are_Prop p,w ; :: thesis: ex y, w being Element of V st
( u,v,w are_LinDep & q,r,y are_LinDep & p,w,y are_LinDep & not y is zero & not w is zero )
A30: ( B <> 0 or C <> 0 )
proof
assume ( not B <> 0 & not C <> 0 ) ; :: thesis: contradiction
then A31: w = ((A * p) + (0. V)) + (0 * r) by A27, RLVECT_1:23
.= ((A * p) + (0. V)) + (0. V) by RLVECT_1:23
.= (A * p) + (0. V) by RLVECT_1:10
.= A * p by RLVECT_1:10 ;
A <> 0 hence contradiction by A29, A31, ANPROJ_1:5; :: thesis: verum
end;
set b = 1;
set a = - A;
set y = ((- A) * p) + (1 * w);
A32: ((- A) * p) + (1 * w) = ((((- A) + (1 * A)) * p) + ((1 * B) * q)) + ((1 * C) * r) by A27, Lm7
.= ((0. V) + ((1 * B) * q)) + ((1 * C) * r) by RLVECT_1:23
.= (B * q) + (C * r) by RLVECT_1:10 ;
A33: not ((- A) * p) + (1 * w) is zero
proof
assume ((- A) * p) + (1 * w) is zero ; :: thesis: contradiction
then 0. V = (B * q) + (C * r) by A32, STRUCT_0:def 15
.= ((0. V) + (B * q)) + (C * r) by RLVECT_1:10
.= ((0 * p) + (B * q)) + (C * r) by RLVECT_1:23
.= (((0 * p) + (B * q)) + (C * r)) + (0. V) by RLVECT_1:10
.= (((0 * p) + (B * q)) + (C * r)) + (0 * s) by RLVECT_1:23 ;
hence contradiction by A1, A30; :: thesis: verum
end;
( q,r,((- A) * p) + (1 * w) are_LinDep & p,w,((- A) * p) + (1 * w) are_LinDep ) by A3, A7, A26, A29, A32, ANPROJ_1:11;
hence ex y, w being Element of V st
( u,v,w are_LinDep & q,r,y are_LinDep & p,w,y are_LinDep & not y is zero & not w is zero ) by A26, A33; :: thesis: verum
end;
hence ex y, w being Element of V st
( u,v,w are_LinDep & q,r,y are_LinDep & p,w,y are_LinDep & not y is zero & not w is zero ) by A28; :: thesis: verum
end;
hence ex y, w being Element of V st
( u,v,w are_LinDep & q,r,y are_LinDep & p,w,y are_LinDep & not y is zero & not w is zero ) by A8; :: thesis: verum