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