let V be RealLinearSpace; :: thesis: for p, q, u, v, w being Element of V st not u,v,w are_LinDep & u,v,p are_LinDep & v,w,q are_LinDep holds
ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
let p, q, u, v, w be Element of V; :: thesis: ( not u,v,w are_LinDep & u,v,p are_LinDep & v,w,q are_LinDep implies ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) )
assume that
A1: not u,v,w are_LinDep and
A2: u,v,p are_LinDep and
A3: v,w,q are_LinDep ; :: thesis: ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
A4: not v is zero by A1, Th12;
A5: not w is zero by A1, Th12;
A6: now :: thesis: ( ( are_Prop p,q or p is zero or q is zero ) implies ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) )
A7: now :: thesis: ( q is zero implies ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) )
assume q is zero ; :: thesis: ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
then q = 0. V ;
then A8: p,q,w are_LinDep by Th10;
u,w,w are_LinDep by Th11;
hence ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A5, A8; :: thesis: verum
end;
A9: now :: thesis: ( p is zero implies ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) )
assume p is zero ; :: thesis: ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
then p = 0. V ;
then A10: p,q,w are_LinDep by Th10;
u,w,w are_LinDep by Th11;
hence ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A5, A10; :: thesis: verum
end;
A11: now :: thesis: ( are_Prop p,q implies ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) )
assume are_Prop p,q ; :: thesis: ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
then A12: p,q,w are_LinDep by Th11;
u,w,w are_LinDep by Th11;
hence ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A5, A12; :: thesis: verum
end;
assume ( are_Prop p,q or p is zero or q is zero ) ; :: thesis: ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
hence ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A11, A9, A7; :: thesis: verum
end;
A13: not u is zero by A1, Th12;
not are_Prop u,v by A1, Th12;
then consider a1, b1 being Real such that
A14: p = (a1 * u) + (b1 * v) by A2, A13, A4, Th6;
A15: not are_Prop w,u by A1, Th12;
not are_Prop v,w by A1, Th12;
then consider a2, b2 being Real such that
A16: q = (a2 * v) + (b2 * w) by A3, A4, A5, Th6;
A17: for c, d being Real holds (c * p) + (d * q) = (((c * a1) * u) + (((c * b1) + (d * a2)) * v)) + ((d * b2) * w)
proof
let c, d be Real; :: thesis: (c * p) + (d * q) = (((c * a1) * u) + (((c * b1) + (d * a2)) * v)) + ((d * b2) * w)
thus (c * p) + (d * q) = (((c * a1) * u) + ((c * b1) * v)) + (d * ((a2 * v) + (b2 * w))) by A14, A16, Lm7
.= (((c * a1) * u) + ((c * b1) * v)) + (((d * a2) * v) + ((d * b2) * w)) by Lm7
.= ((((c * a1) * u) + ((c * b1) * v)) + ((d * a2) * v)) + ((d * b2) * w) by RLVECT_1:def 3
.= (((c * a1) * u) + (((c * b1) * v) + ((d * a2) * v))) + ((d * b2) * w) by RLVECT_1:def 3
.= (((c * a1) * u) + (((c * b1) + (d * a2)) * v)) + ((d * b2) * w) by RLVECT_1:def 6 ; :: thesis: verum
end;
A18: now :: thesis: ( not are_Prop p,q & not p is zero & not q is zero & b1 <> 0 implies ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) )
assume that
A19: not are_Prop p,q and
A20: not p is zero and
A21: not q is zero and
A22: b1 <> 0 ; :: thesis: ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
A23: now :: thesis: ( a2 <> 0 implies ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) )
set c = 1;
set d = - (b1 * (a2 "));
set y = (1 * p) + ((- (b1 * (a2 "))) * q);
assume A24: a2 <> 0 ; :: thesis: ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
then a2 " <> 0 by XCMPLX_1:202;
then A25: b1 * (a2 ") <> 0 by A22, XCMPLX_1:6;
A26: not (1 * p) + ((- (b1 * (a2 "))) * q) is zero
proof
assume (1 * p) + ((- (b1 * (a2 "))) * q) is zero ; :: thesis: contradiction
then 0. V = (1 * p) + ((- (b1 * (a2 "))) * q)
.= (1 * p) + ((b1 * (a2 ")) * (- q)) by RLVECT_1:24
.= (1 * p) + (- ((b1 * (a2 ")) * q)) by RLVECT_1:25 ;
then - (1 * p) = - ((b1 * (a2 ")) * q) by RLVECT_1:def 10;
then 1 * p = (b1 * (a2 ")) * q by RLVECT_1:18;
hence contradiction by A19, A25; :: thesis: verum
end;
(1 * b1) + ((- (b1 * (a2 "))) * a2) = b1 + ((- b1) * ((a2 ") * a2))
.= b1 + ((- b1) * 1) by A24, XCMPLX_0:def 7
.= 0 ;
then (1 * p) + ((- (b1 * (a2 "))) * q) = (((1 * a1) * u) + (0 * v)) + (((- (b1 * (a2 "))) * b2) * w) by A17
.= (((1 * a1) * u) + (0. V)) + (((- (b1 * (a2 "))) * b2) * w) by RLVECT_1:10
.= ((1 * a1) * u) + (((- (b1 * (a2 "))) * b2) * w) ;
then A27: u,w,(1 * p) + ((- (b1 * (a2 "))) * q) are_LinDep by A15, A13, A5, Th6;
p,q,(1 * p) + ((- (b1 * (a2 "))) * q) are_LinDep by A19, A20, A21, Th6;
hence ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A26, A27; :: thesis: verum
end;
now :: thesis: ( a2 = 0 implies ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) )
set c = 0 ;
set d = 1;
set y = (0 * p) + (1 * q);
A28: (0 * p) + (1 * q) = (0. V) + (1 * q) by RLVECT_1:10
.= (0. V) + q by RLVECT_1:def 8
.= q ;
assume a2 = 0 ; :: thesis: ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
then (0 * b1) + (1 * a2) = 0 ;
then (0 * p) + (1 * q) = (((0 * a1) * u) + (0 * v)) + ((1 * b2) * w) by A17
.= (((0 * a1) * u) + (0. V)) + ((1 * b2) * w) by RLVECT_1:10
.= ((0 * a1) * u) + ((1 * b2) * w) ;
then A29: u,w,(0 * p) + (1 * q) are_LinDep by A15, A13, A5, Th6;
p,q,(0 * p) + (1 * q) are_LinDep by A19, A20, A21, Th6;
hence ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A21, A28, A29; :: thesis: verum
end;
hence ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A23; :: thesis: verum
end;
now :: thesis: ( not are_Prop p,q & not p is zero & not q is zero & b1 = 0 implies ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) )
assume that
A30: not are_Prop p,q and
A31: not p is zero and
A32: not q is zero and
A33: b1 = 0 ; :: thesis: ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
now :: thesis: ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
set c = 1;
set d = 0 ;
set y = (1 * p) + (0 * q);
A34: (1 * p) + (0 * q) = p + (0 * q) by RLVECT_1:def 8
.= p + (0. V) by RLVECT_1:10
.= p ;
(1 * b1) + (0 * a2) = 0 by A33;
then (1 * p) + (0 * q) = (((1 * a1) * u) + (0 * v)) + ((0 * b2) * w) by A17
.= (((1 * a1) * u) + (0. V)) + ((0 * b2) * w) by RLVECT_1:10
.= ((1 * a1) * u) + ((0 * b2) * w) ;
then A35: u,w,(1 * p) + (0 * q) are_LinDep by A15, A13, A5, Th6;
p,q,(1 * p) + (0 * q) are_LinDep by A30, A31, A32, Th6;
hence ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A31, A34, A35; :: thesis: verum
end;
hence ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) ; :: thesis: verum
end;
hence ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A6, A18; :: thesis: verum