let V be RealLinearSpace; :: thesis: for p, q, r being Element of V st ( for w being Element of V ex a, b, c being Real st w = ((a * p) + (b * q)) + (c * r) ) & ( for a, b, c being Real st ((a * p) + (b * q)) + (c * r) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ) holds
for u, u1 being Element of V ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )
let p, q, r be Element of V; :: thesis: ( ( for w being Element of V ex a, b, c being Real st w = ((a * p) + (b * q)) + (c * r) ) & ( for a, b, c being Real st ((a * p) + (b * q)) + (c * r) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ) implies for u, u1 being Element of V ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) )
assume that
A1: for w being Element of V ex a, b, c being Real st w = ((a * p) + (b * q)) + (c * r) and
A2: for a, b, c being Real st ((a * p) + (b * q)) + (c * r) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ; :: thesis: for u, u1 being Element of V ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )
let u, u1 be Element of V; :: thesis: ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )
consider a, b, c being Real such that
A3: u = ((a * p) + (b * q)) + (c * r) by A1;
consider a1, b1, c1 being Real such that
A4: u1 = ((a1 * p) + (b1 * q)) + (c1 * r) by A1;
A5: ( not p is zero & not q is zero & not r is zero & not p,q,r are_LinDep & not are_Prop p,q ) by A2, Th1;
A6: for a3, b3 being Real holds (a3 * u) + (b3 * u1) = ((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) + (b3 * b1)) * q)) + (((a3 * c) + (b3 * c1)) * r)
proof
let a3, b3 be Real; :: thesis: (a3 * u) + (b3 * u1) = ((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) + (b3 * b1)) * q)) + (((a3 * c) + (b3 * c1)) * r)
a3 * u = (((a3 * a) * p) + ((a3 * b) * q)) + ((a3 * c) * r) by A3, Lm2;
hence (a3 * u) + (b3 * u1) = ((((a3 * a) * p) + ((a3 * b) * q)) + ((a3 * c) * r)) + ((((b3 * a1) * p) + ((b3 * b1) * q)) + ((b3 * c1) * r)) by A4, Lm2
.= ((((a3 * a) * p) + ((b3 * a1) * p)) + (((a3 * b) * q) + ((b3 * b1) * q))) + (((a3 * c) * r) + ((b3 * c1) * r)) by Lm3
.= ((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) * q) + ((b3 * b1) * q))) + (((a3 * c) * r) + ((b3 * c1) * r)) by RLVECT_1:def 9
.= ((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) + (b3 * b1)) * q)) + (((a3 * c) * r) + ((b3 * c1) * r)) by RLVECT_1:def 9
.= ((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) + (b3 * b1)) * q)) + (((a3 * c) + (b3 * c1)) * r) by RLVECT_1:def 9 ;
:: thesis: verum
end;
A7: now
assume A8: ( are_Prop u,u1 or u is zero or u1 is zero ) ; :: thesis: ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )
A9: now
assume A10: are_Prop u,u1 ; :: thesis: ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )
A11: p,q,q are_LinDep by ANPROJ_1:16;
u,u1,q are_LinDep by A10, ANPROJ_1:16;
hence ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) by A5, A11; :: thesis: verum
end;
A12: now
assume u is zero ; :: thesis: ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )
then A13: u = 0. V by STRUCT_0:def 15;
A14: p,q,q are_LinDep by ANPROJ_1:16;
u,u1,q are_LinDep by A13, ANPROJ_1:15;
hence ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) by A5, A14; :: thesis: verum
end;
now
assume u1 is zero ; :: thesis: ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )
then A15: u1 = 0. V by STRUCT_0:def 15;
A16: p,q,q are_LinDep by ANPROJ_1:16;
u,u1,q are_LinDep by A15, ANPROJ_1:15;
hence ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) by A5, A16; :: thesis: verum
end;
hence ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) by A8, A9, A12; :: thesis: verum
end;
A17: now
assume A18: ( not are_Prop u,u1 & not u is zero & not u1 is zero & c = 0 ) ; :: thesis: ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )
now
set a3 = 1;
set b3 = 0 ;
set y = (1 * u) + (0 * u1);
A19: not (1 * u) + (0 * u1) is zero
proof
(1 * u) + (0 * u1) = u + (0 * u1) by RLVECT_1:def 9
.= u + (0. V) by RLVECT_1:23
.= u by RLVECT_1:10 ;
hence not (1 * u) + (0 * u1) is zero by A18; :: thesis: verum
end;
(1 * c) + (0 * c1) = 0 by A18;
then (1 * u) + (0 * u1) = ((((1 * a) + (0 * a1)) * p) + (((1 * b) + (0 * b1)) * q)) + (0 * r) by A6
.= ((((1 * a) + (0 * a1)) * p) + (((1 * b) + (0 * b1)) * q)) + (0. V) by RLVECT_1:23
.= (((1 * a) + (0 * a1)) * p) + (((1 * b) + (0 * b1)) * q) by RLVECT_1:10 ;
then A20: p,q,(1 * u) + (0 * u1) are_LinDep by A5, ANPROJ_1:11;
u,u1,(1 * u) + (0 * u1) are_LinDep by A18, ANPROJ_1:11;
hence ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) by A19, A20; :: thesis: verum
end;
hence ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) ; :: thesis: verum
end;
now
assume A21: ( not are_Prop u,u1 & not u is zero & not u1 is zero & c <> 0 ) ; :: thesis: ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )
A22: now
assume A23: c1 = 0 ; :: thesis: ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )
set a3 = 0 ;
set b3 = 1;
set y = (0 * u) + (1 * u1);
A24: not (0 * u) + (1 * u1) is zero
proof
(0 * u) + (1 * u1) = (0 * u) + u1 by RLVECT_1:def 9
.= (0. V) + u1 by RLVECT_1:23
.= u1 by RLVECT_1:10 ;
hence not (0 * u) + (1 * u1) is zero by A21; :: thesis: verum
end;
(0 * c) + (1 * c1) = 0 by A23;
then (0 * u) + (1 * u1) = ((((0 * a) + (1 * a1)) * p) + (((0 * b) + (1 * b1)) * q)) + (0 * r) by A6
.= ((((0 * a) + (1 * a1)) * p) + (((0 * b) + (1 * b1)) * q)) + (0. V) by RLVECT_1:23
.= (((0 * a) + (1 * a1)) * p) + (((0 * b) + (1 * b1)) * q) by RLVECT_1:10 ;
then A25: p,q,(0 * u) + (1 * u1) are_LinDep by A5, ANPROJ_1:11;
u,u1,(0 * u) + (1 * u1) are_LinDep by A21, ANPROJ_1:11;
hence ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) by A24, A25; :: thesis: verum
end;
now
assume A26: c1 <> 0 ; :: thesis: ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )
set a3 = 1;
set b3 = - (c * (c1 " ));
set y = (1 * u) + ((- (c * (c1 " ))) * u1);
c1 " <> 0 by A26, XCMPLX_1:203;
then A27: c * (c1 " ) <> 0 by A21, XCMPLX_1:6;
A28: not (1 * u) + ((- (c * (c1 " ))) * u1) is zero
proof
assume (1 * u) + ((- (c * (c1 " ))) * u1) is zero ; :: thesis: contradiction
then 0. V = (1 * u) + ((- (c * (c1 " ))) * u1) by STRUCT_0:def 15
.= (1 * u) + ((c * (c1 " )) * (- u1)) by RLVECT_1:38
.= (1 * u) + (- ((c * (c1 " )) * u1)) by RLVECT_1:39 ;
then - (1 * u) = - ((c * (c1 " )) * u1) by RLVECT_1:def 11;
then 1 * u = (c * (c1 " )) * u1 by RLVECT_1:31;
hence contradiction by A21, A27, ANPROJ_1:def 2; :: thesis: verum
end;
(1 * c) + ((- (c * (c1 " ))) * c1) = c + ((- c) * ((c1 " ) * c1))
.= c + ((- c) * 1) by A26, XCMPLX_0:def 7
.= 0 ;
then (1 * u) + ((- (c * (c1 " ))) * u1) = ((((1 * a) + ((- (c * (c1 " ))) * a1)) * p) + (((1 * b) + ((- (c * (c1 " ))) * b1)) * q)) + (0 * r) by A6
.= ((((1 * a) + ((- (c * (c1 " ))) * a1)) * p) + (((1 * b) + ((- (c * (c1 " ))) * b1)) * q)) + (0. V) by RLVECT_1:23
.= (((1 * a) + ((- (c * (c1 " ))) * a1)) * p) + (((1 * b) + ((- (c * (c1 " ))) * b1)) * q) by RLVECT_1:10 ;
then A29: p,q,(1 * u) + ((- (c * (c1 " ))) * u1) are_LinDep by A5, ANPROJ_1:11;
u,u1,(1 * u) + ((- (c * (c1 " ))) * u1) are_LinDep by A21, ANPROJ_1:11;
hence ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) by A28, A29; :: thesis: verum
end;
hence ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) by A22; :: thesis: verum
end;
hence ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) by A7, A17; :: thesis: verum