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 are_Prop u,v & not are_Prop v,w & not are_Prop w,u & not u is zero & not v is zero & not w is zero ) by A1, Th17;
then consider a1, b1 being Real such that
A5: p = (a1 * u) + (b1 * v) by A2, Th11;
consider a2, b2 being Real such that
A6: q = (a2 * v) + (b2 * w) by A3, A4, Th11;
A7: 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 A5, A6, 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;

A8: now

assume A9: ( 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 )

A10: now

assume A11: 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 )
A12: u,w,w are_LinDep by Th16;
p,q,w are_LinDep by A11, Th16;
hence ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A4, A12; :: thesis: verum

end;

A13: 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 A14: p = 0. V by STRUCT_0:def 15;
A15: u,w,w are_LinDep by Th16;
p,q,w are_LinDep by A14, Th15;
hence ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A4, A15; :: thesis: verum

end;

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 A16: q = 0. V by STRUCT_0:def 15;
A17: u,w,w are_LinDep by Th16;
p,q,w are_LinDep by A16, Th15;
hence ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A4, A17; :: 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 A9, A10, A13; :: thesis: verum

end;

A18: now

assume A19: ( not are_Prop p,q & not p is zero & not q is zero & 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);
A20: not (1 * p) + (0 * q) is zero

proof

(1 * p) + (0 * q) = p + (0 * q) by RLVECT_1:def 9
.= p + (0. V) by RLVECT_1:23
.= p by RLVECT_1:10 ;
hence not (1 * p) + (0 * q) is zero by A19; :: thesis: verum

end;

(1 * b1) + (0 * a2) = 0 by A19;
then (1 * p) + (0 * q) = (((1 * a1) * u) + (0 * v)) + ((0 * b2) * w) by A7
.= (((1 * a1) * u) + (0. V)) + ((0 * b2) * w) by RLVECT_1:23
.= ((1 * a1) * u) + ((0 * b2) * w) by RLVECT_1:10 ;
then A21: u,w,(1 * p) + (0 * q) are_LinDep by A4, Th11;
p,q,(1 * p) + (0 * q) are_LinDep by A19, Th11;
hence ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A20, A21; :: 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;

now

assume A22: ( not are_Prop p,q & not p is zero & not q is zero & 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

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 )
set c = 0 ;
set d = 1;
set y = (0 * p) + (1 * q);
A25: not (0 * p) + (1 * q) is zero

proof

(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 ;
hence not (0 * p) + (1 * q) is zero by A22; :: thesis: verum

end;

(0 * b1) + (1 * a2) = 0 by A24;
then (0 * p) + (1 * q) = (((0 * a1) * u) + (0 * v)) + ((1 * b2) * w) by A7
.= (((0 * a1) * u) + (0. V)) + ((1 * b2) * w) by RLVECT_1:23
.= ((0 * a1) * u) + ((1 * b2) * w) by RLVECT_1:10 ;
then A26: u,w,(0 * p) + (1 * q) are_LinDep by A4, Th11;
p,q,(0 * p) + (1 * q) are_LinDep by A22, Th11;
hence ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A25, A26; :: thesis: verum

end;

now

assume A27: a2 <> 0 ; :: 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 = - (b1 * (a2 " ));
set y = (1 * p) + ((- (b1 * (a2 " ))) * q);
a2 " <> 0 by A27, XCMPLX_1:203;
then A28: b1 * (a2 " ) <> 0 by A22, XCMPLX_1:6;
A29: 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 15
.= (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 A22, A28, Def2; :: thesis: verum

end;

(1 * b1) + ((- (b1 * (a2 " ))) * a2) = b1 + ((- b1) * ((a2 " ) * a2))
.= b1 + ((- b1) * 1) by A27, XCMPLX_0:def 7
.= 0 ;
then (1 * p) + ((- (b1 * (a2 " ))) * q) = (((1 * a1) * u) + (0 * v)) + (((- (b1 * (a2 " ))) * b2) * w) by A7
.= (((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 A30: u,w,(1 * p) + ((- (b1 * (a2 " ))) * q) are_LinDep by A4, Th11;
p,q,(1 * p) + ((- (b1 * (a2 " ))) * q) are_LinDep by A22, Th11;
hence ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A29, A30; :: 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;

hence ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A8, A18; :: thesis: verum