let V be RealLinearSpace; :: thesis: for p, q, r, u, v, w, y being Element of V st u,v,q are_LinDep & w,y,q are_LinDep & u,w,p are_LinDep & v,y,p are_LinDep & u,y,r are_LinDep & v,w,r are_LinDep & p,q,r are_LinDep & not p is zero & not q is zero & not r is zero & not u,v,y are_LinDep & not u,v,w are_LinDep & not u,w,y are_LinDep holds

v,w,y are_LinDep

let p, q, r, u, v, w, y be Element of V; :: thesis: ( u,v,q are_LinDep & w,y,q are_LinDep & u,w,p are_LinDep & v,y,p are_LinDep & u,y,r are_LinDep & v,w,r are_LinDep & p,q,r are_LinDep & not p is zero & not q is zero & not r is zero & not u,v,y are_LinDep & not u,v,w are_LinDep & not u,w,y are_LinDep implies v,w,y are_LinDep )

assume that

A1: u,v,q are_LinDep and

A2: w,y,q are_LinDep and

A3: u,w,p are_LinDep and

A4: v,y,p are_LinDep and

A5: u,y,r are_LinDep and

A6: v,w,r are_LinDep and

A7: p,q,r are_LinDep and

A8: not p is zero and

A9: not q is zero and

A10: not r is zero ; :: thesis: ( u,v,y are_LinDep or u,v,w are_LinDep or u,w,y are_LinDep or v,w,y are_LinDep )

assume A11: ( not u,v,y are_LinDep & not u,v,w are_LinDep & not u,w,y are_LinDep & not v,w,y are_LinDep ) ; :: thesis: contradiction

then A12: not v is zero by Th12;

A13: not w is zero by A11, Th12;

A14: not y is zero by A11, Th12;

A15: not u is zero by A11, Th12;

not are_Prop v,y by A11, Th12;

then consider a19, b19 being Real such that

A16: p = (a19 * v) + (b19 * y) by A4, A12, A14, Th6;

not are_Prop u,v by A11, Th12;

then consider a2, b2 being Real such that

A17: q = (a2 * u) + (b2 * v) by A1, A15, A12, Th6;

not are_Prop v,w by A11, Th12;

then consider a39, b39 being Real such that

A18: r = (a39 * v) + (b39 * w) by A6, A12, A13, Th6;

not are_Prop u,w by A11, Th12;

then consider a1, b1 being Real such that

A19: p = (a1 * u) + (b1 * w) by A3, A15, A13, Th6;

not are_Prop w,y by A11, Th12;

then consider a29, b29 being Real such that

A20: q = (a29 * w) + (b29 * y) by A2, A13, A14, Th6;

not are_Prop y,u by A11, Th12;

then consider a3, b3 being Real such that

A21: r = (a3 * u) + (b3 * y) by A5, A15, A14, Th6;

consider A, B, C being Real such that

A22: ((A * p) + (B * q)) + (C * r) = 0. V and

A23: ( A <> 0 or B <> 0 or C <> 0 ) by A7;

A24: 0. V = ((((A * a1) + (C * a3)) * u) + (((A * b1) + (B * a29)) * w)) + (((B * b29) + (C * b3)) * y) by A19, A20, A21, A22, Lm9;

then A25: (A * a1) + (C * a3) = 0 by A11;

A26: 0. V = ((C * ((a39 * v) + (b39 * w))) + (B * ((a29 * w) + (b29 * y)))) + (A * ((a19 * v) + (b19 * y))) by A16, A20, A18, A22, RLVECT_1:def 3

.= ((((C * a39) + (A * a19)) * v) + (((C * b39) + (B * a29)) * w)) + (((B * b29) + (A * b19)) * y) by Lm9 ;

then A27: (C * a39) + (A * a19) = 0 by A11;

A28: 0. V = ((((B * a2) + (C * a3)) * u) + (((B * b2) + (A * a19)) * v)) + (((A * b19) + (C * b3)) * y) by A16, A17, A21, A22, Lm9;

then A29: (B * a2) + (C * a3) = 0 by A11;

A30: 0. V = ((((B * a2) + (A * a1)) * u) + (((B * b2) + (C * a39)) * v)) + (((C * b39) + (A * b1)) * w) by A19, A17, A18, A22, Lm9;

then A31: (B * a2) + (A * a1) = 0 by A11;

A32: (C * b39) + (B * a29) = 0 by A11, A26;

A33: (C * b39) + (A * b1) = 0 by A11, A30;

A34: (B * b29) + (A * b19) = 0 by A11, A26;

A35: (A * b19) + (C * b3) = 0 by A11, A28;

A36: (B * b29) + (C * b3) = 0 by A11, A24;

A40: (B * b2) + (A * a19) = 0 by A11, A28;

v,w,y are_LinDep

let p, q, r, u, v, w, y be Element of V; :: thesis: ( u,v,q are_LinDep & w,y,q are_LinDep & u,w,p are_LinDep & v,y,p are_LinDep & u,y,r are_LinDep & v,w,r are_LinDep & p,q,r are_LinDep & not p is zero & not q is zero & not r is zero & not u,v,y are_LinDep & not u,v,w are_LinDep & not u,w,y are_LinDep implies v,w,y are_LinDep )

assume that

A1: u,v,q are_LinDep and

A2: w,y,q are_LinDep and

A3: u,w,p are_LinDep and

A4: v,y,p are_LinDep and

A5: u,y,r are_LinDep and

A6: v,w,r are_LinDep and

A7: p,q,r are_LinDep and

A8: not p is zero and

A9: not q is zero and

A10: not r is zero ; :: thesis: ( u,v,y are_LinDep or u,v,w are_LinDep or u,w,y are_LinDep or v,w,y are_LinDep )

assume A11: ( not u,v,y are_LinDep & not u,v,w are_LinDep & not u,w,y are_LinDep & not v,w,y are_LinDep ) ; :: thesis: contradiction

then A12: not v is zero by Th12;

A13: not w is zero by A11, Th12;

A14: not y is zero by A11, Th12;

A15: not u is zero by A11, Th12;

not are_Prop v,y by A11, Th12;

then consider a19, b19 being Real such that

A16: p = (a19 * v) + (b19 * y) by A4, A12, A14, Th6;

not are_Prop u,v by A11, Th12;

then consider a2, b2 being Real such that

A17: q = (a2 * u) + (b2 * v) by A1, A15, A12, Th6;

not are_Prop v,w by A11, Th12;

then consider a39, b39 being Real such that

A18: r = (a39 * v) + (b39 * w) by A6, A12, A13, Th6;

not are_Prop u,w by A11, Th12;

then consider a1, b1 being Real such that

A19: p = (a1 * u) + (b1 * w) by A3, A15, A13, Th6;

not are_Prop w,y by A11, Th12;

then consider a29, b29 being Real such that

A20: q = (a29 * w) + (b29 * y) by A2, A13, A14, Th6;

not are_Prop y,u by A11, Th12;

then consider a3, b3 being Real such that

A21: r = (a3 * u) + (b3 * y) by A5, A15, A14, Th6;

consider A, B, C being Real such that

A22: ((A * p) + (B * q)) + (C * r) = 0. V and

A23: ( A <> 0 or B <> 0 or C <> 0 ) by A7;

A24: 0. V = ((((A * a1) + (C * a3)) * u) + (((A * b1) + (B * a29)) * w)) + (((B * b29) + (C * b3)) * y) by A19, A20, A21, A22, Lm9;

then A25: (A * a1) + (C * a3) = 0 by A11;

A26: 0. V = ((C * ((a39 * v) + (b39 * w))) + (B * ((a29 * w) + (b29 * y)))) + (A * ((a19 * v) + (b19 * y))) by A16, A20, A18, A22, RLVECT_1:def 3

.= ((((C * a39) + (A * a19)) * v) + (((C * b39) + (B * a29)) * w)) + (((B * b29) + (A * b19)) * y) by Lm9 ;

then A27: (C * a39) + (A * a19) = 0 by A11;

A28: 0. V = ((((B * a2) + (C * a3)) * u) + (((B * b2) + (A * a19)) * v)) + (((A * b19) + (C * b3)) * y) by A16, A17, A21, A22, Lm9;

then A29: (B * a2) + (C * a3) = 0 by A11;

A30: 0. V = ((((B * a2) + (A * a1)) * u) + (((B * b2) + (C * a39)) * v)) + (((C * b39) + (A * b1)) * w) by A19, A17, A18, A22, Lm9;

then A31: (B * a2) + (A * a1) = 0 by A11;

A32: (C * b39) + (B * a29) = 0 by A11, A26;

A33: (C * b39) + (A * b1) = 0 by A11, A30;

A34: (B * b29) + (A * b19) = 0 by A11, A26;

A35: (A * b19) + (C * b3) = 0 by A11, A28;

A36: (B * b29) + (C * b3) = 0 by A11, A24;

A37: now :: thesis: not C <> 0

A39:
(B * b2) + (C * a39) = 0
by A11, A30;assume A38:
C <> 0
; :: thesis: contradiction

then a3 = 0 by A25, A29, A31, XCMPLX_1:6;

then r = (0 * u) + (0 * y) by A21, A36, A35, A34, A38, XCMPLX_1:6

.= (0. V) + (0 * y) by RLVECT_1:10

.= (0. V) + (0. V) by RLVECT_1:10

.= 0. V ;

hence contradiction by A10; :: thesis: verum

end;then a3 = 0 by A25, A29, A31, XCMPLX_1:6;

then r = (0 * u) + (0 * y) by A21, A36, A35, A34, A38, XCMPLX_1:6

.= (0. V) + (0 * y) by RLVECT_1:10

.= (0. V) + (0. V) by RLVECT_1:10

.= 0. V ;

hence contradiction by A10; :: thesis: verum

A40: (B * b2) + (A * a19) = 0 by A11, A28;

A41: now :: thesis: not B <> 0

A43:
(A * b1) + (B * a29) = 0
by A11, A24;assume A42:
B <> 0
; :: thesis: contradiction

then a2 = 0 by A25, A29, A31, XCMPLX_1:6;

then q = (0 * u) + (0 * v) by A17, A40, A39, A27, A42, XCMPLX_1:6

.= (0. V) + (0 * v) by RLVECT_1:10

.= (0. V) + (0. V) by RLVECT_1:10

.= 0. V ;

hence contradiction by A9; :: thesis: verum

end;then a2 = 0 by A25, A29, A31, XCMPLX_1:6;

then q = (0 * u) + (0 * v) by A17, A40, A39, A27, A42, XCMPLX_1:6

.= (0. V) + (0 * v) by RLVECT_1:10

.= (0. V) + (0. V) by RLVECT_1:10

.= 0. V ;

hence contradiction by A9; :: thesis: verum

now :: thesis: not A <> 0

hence
contradiction
by A23, A41, A37; :: thesis: verumassume A44:
A <> 0
; :: thesis: contradiction

then a1 = 0 by A25, A29, A31, XCMPLX_1:6;

then p = (0 * u) + (0 * w) by A19, A43, A33, A32, A44, XCMPLX_1:6

.= (0. V) + (0 * w) by RLVECT_1:10

.= (0. V) + (0. V) by RLVECT_1:10

.= 0. V ;

hence contradiction by A8; :: thesis: verum

end;then a1 = 0 by A25, A29, A31, XCMPLX_1:6;

then p = (0 * u) + (0 * w) by A19, A43, A33, A32, A44, XCMPLX_1:6

.= (0. V) + (0 * w) by RLVECT_1:10

.= (0. V) + (0. V) by RLVECT_1:10

.= 0. V ;

hence contradiction by A8; :: thesis: verum