let V be RealLinearSpace; :: thesis: for u, v, w, p, q 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 u, v, w, p, q 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, Th17;
A5: not w is zero by A1, Th17;

A6: now

A7: now

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 by STRUCT_0:def 12;
then A8: p,q,w are_LinDep by Th15;
u,w,w are_LinDep by Th16;
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

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 by STRUCT_0:def 12;
then A10: p,q,w are_LinDep by Th15;
u,w,w are_LinDep by Th16;
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

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 Th16;
u,w,w are_LinDep by Th16;
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, Th17;
not are_Prop u,v by A1, Th17;
then consider a1, b1 being Real such that
A14: p = (a1 * u) + (b1 * v) by A2, A13, A4, Th11;
A15: not are_Prop w,u by A1, Th17;
not are_Prop v,w by A1, Th17;
then consider a2, b2 being Real such that
A16: q = (a2 * v) + (b2 * w) by A3, A4, A5, Th11;
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 6
.= (((c * a1) * u) + (((c * b1) * v) + ((d * a2) * v))) + ((d * b2) * w) by RLVECT_1:def 6
.= (((c * a1) * u) + (((c * b1) + (d * a2)) * v)) + ((d * b2) * w) by RLVECT_1:def 9 ; :: thesis: verum

end;

A18: now

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

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:203;
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) by STRUCT_0:def 12
.= (1 * p) + ((b1 * (a2 " )) * (- q)) by RLVECT_1:38
.= (1 * p) + (- ((b1 * (a2 " )) * q)) by RLVECT_1:39 ;
then - (1 * p) = - ((b1 * (a2 " )) * q) by RLVECT_1:def 11;
then 1 * p = (b1 * (a2 " )) * q by RLVECT_1:31;
hence contradiction by A19, A25, Def2; :: 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:23
.= ((1 * a1) * u) + (((- (b1 * (a2 " ))) * b2) * w) by RLVECT_1:10 ;
then A27: u,w,(1 * p) + ((- (b1 * (a2 " ))) * q) are_LinDep by A15, A13, A5, Th11;
p,q,(1 * p) + ((- (b1 * (a2 " ))) * q) are_LinDep by A19, A20, A21, Th11;
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

set c = 0 ;
set d = 1;
set y = (0 * p) + (1 * q);
A28: (0 * p) + (1 * q) = (0. V) + (1 * q) by RLVECT_1:23
.= (0. V) + q by RLVECT_1:def 9
.= q by RLVECT_1:10 ;
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:23
.= ((0 * a1) * u) + ((1 * b2) * w) by RLVECT_1:10 ;
then A29: u,w,(0 * p) + (1 * q) are_LinDep by A15, A13, A5, Th11;
p,q,(0 * p) + (1 * q) are_LinDep by A19, A20, A21, Th11;
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

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

set c = 1;
set d = 0 ;
set y = (1 * p) + (0 * q);
A34: (1 * p) + (0 * q) = p + (0 * q) by RLVECT_1:def 9
.= p + (0. V) by RLVECT_1:23
.= p by RLVECT_1:10 ;
(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:23
.= ((1 * a1) * u) + ((0 * b2) * w) by RLVECT_1:10 ;
then A35: u,w,(1 * p) + (0 * q) are_LinDep by A15, A13, A5, Th11;
p,q,(1 * p) + (0 * q) are_LinDep by A30, A31, A32, Th11;
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