let V be RealLinearSpace; :: thesis: for o, u, u2 being Element of V st o,u,u2 are_LinDep & not are_Prop o,u & not are_Prop o,u2 & not are_Prop u,u2 & o,u,u2 are_Prop_Vect holds

( ex a1, b1 being Real st

( b1 * u2 = o + (a1 * u) & a1 <> 0 & b1 <> 0 ) & ex a2, c2 being Real st

( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 ) )

let o, u, u2 be Element of V; :: thesis: ( o,u,u2 are_LinDep & not are_Prop o,u & not are_Prop o,u2 & not are_Prop u,u2 & o,u,u2 are_Prop_Vect implies ( ex a1, b1 being Real st

( b1 * u2 = o + (a1 * u) & a1 <> 0 & b1 <> 0 ) & ex a2, c2 being Real st

( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 ) ) )

assume that

A1: o,u,u2 are_LinDep and

A2: not are_Prop o,u and

A3: not are_Prop o,u2 and

A4: not are_Prop u,u2 and

A5: o,u,u2 are_Prop_Vect ; :: thesis: ( ex a1, b1 being Real st

( b1 * u2 = o + (a1 * u) & a1 <> 0 & b1 <> 0 ) & ex a2, c2 being Real st

( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 ) )

consider a, b, c being Real such that

A6: ((a * o) + (b * u)) + (c * u2) = 0. V and

A7: ( a <> 0 or b <> 0 or c <> 0 ) by A1;

not u is zero by A5;

then A8: u <> 0. V ;

not u2 is zero by A5;

then A9: u2 <> 0. V ;

not o is zero by A5;

then A10: o <> 0. V ;

A11: ( a <> 0 & b <> 0 & c <> 0 )

a " <> 0 by A11, XCMPLX_1:202;

then A37: ( (a ") * b <> 0 & - ((a ") * c) <> 0 ) by A11, XCMPLX_1:6;

(a ") * (- (c * u2)) = (a ") * ((a * o) + (b * u)) by A6, RLVECT_1:6

.= ((a ") * (a * o)) + ((a ") * (b * u)) by RLVECT_1:def 5

.= (((a ") * a) * o) + ((a ") * (b * u)) by RLVECT_1:def 7

.= (((a ") * a) * o) + (((a ") * b) * u) by RLVECT_1:def 7

.= (1 * o) + (((a ") * b) * u) by A11, XCMPLX_0:def 7

.= o + (((a ") * b) * u) by RLVECT_1:def 8 ;

then o + (((a ") * b) * u) = (a ") * (c * (- u2)) by RLVECT_1:25

.= ((a ") * c) * (- u2) by RLVECT_1:def 7

.= (- ((a ") * c)) * u2 by RLVECT_1:24 ;

hence ex a1, b1 being Real st

( b1 * u2 = o + (a1 * u) & a1 <> 0 & b1 <> 0 ) by A37; :: thesis: ex a2, c2 being Real st

( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 )

- b <> 0 by A11;

then A38: (c ") * (- b) <> 0 by A36, XCMPLX_1:6;

c * u2 = - ((a * o) + (b * u)) by A6, RLVECT_1:def 10

.= (- (a * o)) + (- (b * u)) by RLVECT_1:31

.= ((- a) * o) + (- (b * u)) by Lm8

.= ((- a) * o) + ((- b) * u) by Lm8 ;

then (c ") * (c * u2) = ((c ") * ((- a) * o)) + ((c ") * ((- b) * u)) by RLVECT_1:def 5

.= (((c ") * (- a)) * o) + ((c ") * ((- b) * u)) by RLVECT_1:def 7

.= (((c ") * (- a)) * o) + (((c ") * (- b)) * u) by RLVECT_1:def 7 ;

then A39: (((c ") * (- a)) * o) + (((c ") * (- b)) * u) = ((c ") * c) * u2 by RLVECT_1:def 7

.= 1 * u2 by A11, XCMPLX_0:def 7

.= u2 by RLVECT_1:def 8 ;

- a <> 0 by A11;

then (c ") * (- a) <> 0 by A36, XCMPLX_1:6;

hence ex a2, c2 being Real st

( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 ) by A39, A38; :: thesis: verum

( ex a1, b1 being Real st

( b1 * u2 = o + (a1 * u) & a1 <> 0 & b1 <> 0 ) & ex a2, c2 being Real st

( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 ) )

let o, u, u2 be Element of V; :: thesis: ( o,u,u2 are_LinDep & not are_Prop o,u & not are_Prop o,u2 & not are_Prop u,u2 & o,u,u2 are_Prop_Vect implies ( ex a1, b1 being Real st

( b1 * u2 = o + (a1 * u) & a1 <> 0 & b1 <> 0 ) & ex a2, c2 being Real st

( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 ) ) )

assume that

A1: o,u,u2 are_LinDep and

A2: not are_Prop o,u and

A3: not are_Prop o,u2 and

A4: not are_Prop u,u2 and

A5: o,u,u2 are_Prop_Vect ; :: thesis: ( ex a1, b1 being Real st

( b1 * u2 = o + (a1 * u) & a1 <> 0 & b1 <> 0 ) & ex a2, c2 being Real st

( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 ) )

consider a, b, c being Real such that

A6: ((a * o) + (b * u)) + (c * u2) = 0. V and

A7: ( a <> 0 or b <> 0 or c <> 0 ) by A1;

not u is zero by A5;

then A8: u <> 0. V ;

not u2 is zero by A5;

then A9: u2 <> 0. V ;

not o is zero by A5;

then A10: o <> 0. V ;

A11: ( a <> 0 & b <> 0 & c <> 0 )

proof

hence contradiction by A20, A12, A28; :: thesis: verum

end;

then A36:
c " <> 0
by XCMPLX_1:202;A12: now :: thesis: not b = 0

assume A13:
b = 0
; :: thesis: contradiction

then 0. V = ((a * o) + (0. V)) + (c * u2) by A6, RLVECT_1:10

.= (a * o) + (c * u2) by RLVECT_1:4 ;

then a * o = - (c * u2) by RLVECT_1:6

.= c * (- u2) by RLVECT_1:25 ;

then A14: a * o = (- c) * u2 by RLVECT_1:24;

A15: ( a <> 0 & c <> 0 )

hence contradiction by A3, A15, A14; :: thesis: verum

end;then 0. V = ((a * o) + (0. V)) + (c * u2) by A6, RLVECT_1:10

.= (a * o) + (c * u2) by RLVECT_1:4 ;

then a * o = - (c * u2) by RLVECT_1:6

.= c * (- u2) by RLVECT_1:25 ;

then A14: a * o = (- c) * u2 by RLVECT_1:24;

A15: ( a <> 0 & c <> 0 )

proof

hence contradiction by A18, A16; :: thesis: verum

end;

then
- c <> 0
;A16: now :: thesis: not c = 0

assume A17:
c = 0
; :: thesis: contradiction

then 0. V = ((a * o) + (0 * u)) + (0. V) by A6, A13, RLVECT_1:10

.= (a * o) + (0 * u) by RLVECT_1:4

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

.= a * o by RLVECT_1:4 ;

hence contradiction by A7, A10, A13, A17, RLVECT_1:11; :: thesis: verum

end;then 0. V = ((a * o) + (0 * u)) + (0. V) by A6, A13, RLVECT_1:10

.= (a * o) + (0 * u) by RLVECT_1:4

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

.= a * o by RLVECT_1:4 ;

hence contradiction by A7, A10, A13, A17, RLVECT_1:11; :: thesis: verum

A18: now :: thesis: not a = 0

assume
( not a <> 0 or not c <> 0 )
; :: thesis: contradictionassume A19:
a = 0
; :: thesis: contradiction

then 0. V = ((0. V) + (0 * u)) + (c * u2) by A6, A13, RLVECT_1:10

.= (0 * u) + (c * u2) by RLVECT_1:4

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

.= c * u2 by RLVECT_1:4 ;

hence contradiction by A7, A9, A13, A19, RLVECT_1:11; :: thesis: verum

end;then 0. V = ((0. V) + (0 * u)) + (c * u2) by A6, A13, RLVECT_1:10

.= (0 * u) + (c * u2) by RLVECT_1:4

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

.= c * u2 by RLVECT_1:4 ;

hence contradiction by A7, A9, A13, A19, RLVECT_1:11; :: thesis: verum

hence contradiction by A18, A16; :: thesis: verum

hence contradiction by A3, A15, A14; :: thesis: verum

A20: now :: thesis: not a = 0

assume A21:
a = 0
; :: thesis: contradiction

then 0. V = ((0. V) + (b * u)) + (c * u2) by A6, RLVECT_1:10

.= (b * u) + (c * u2) by RLVECT_1:4 ;

then b * u = - (c * u2) by RLVECT_1:6

.= c * (- u2) by RLVECT_1:25 ;

then A22: b * u = (- c) * u2 by RLVECT_1:24;

A23: ( b <> 0 & c <> 0 )

hence contradiction by A4, A23, A22; :: thesis: verum

end;then 0. V = ((0. V) + (b * u)) + (c * u2) by A6, RLVECT_1:10

.= (b * u) + (c * u2) by RLVECT_1:4 ;

then b * u = - (c * u2) by RLVECT_1:6

.= c * (- u2) by RLVECT_1:25 ;

then A22: b * u = (- c) * u2 by RLVECT_1:24;

A23: ( b <> 0 & c <> 0 )

proof

hence contradiction by A26, A24; :: thesis: verum

end;

then
- c <> 0
;A24: now :: thesis: not c = 0

assume A25:
c = 0
; :: thesis: contradiction

then 0. V = ((0. V) + (b * u)) + (0 * u2) by A6, A21, RLVECT_1:10

.= (b * u) + (0 * u2) by RLVECT_1:4

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

.= b * u by RLVECT_1:4 ;

hence contradiction by A7, A8, A21, A25, RLVECT_1:11; :: thesis: verum

end;then 0. V = ((0. V) + (b * u)) + (0 * u2) by A6, A21, RLVECT_1:10

.= (b * u) + (0 * u2) by RLVECT_1:4

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

.= b * u by RLVECT_1:4 ;

hence contradiction by A7, A8, A21, A25, RLVECT_1:11; :: thesis: verum

A26: now :: thesis: not b = 0

assume
( not b <> 0 or not c <> 0 )
; :: thesis: contradictionassume A27:
b = 0
; :: thesis: contradiction

then 0. V = ((0. V) + (0 * u)) + (c * u2) by A6, A21, RLVECT_1:10

.= (0 * u) + (c * u2) by RLVECT_1:4

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

.= c * u2 by RLVECT_1:4 ;

hence contradiction by A7, A9, A21, A27, RLVECT_1:11; :: thesis: verum

end;then 0. V = ((0. V) + (0 * u)) + (c * u2) by A6, A21, RLVECT_1:10

.= (0 * u) + (c * u2) by RLVECT_1:4

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

.= c * u2 by RLVECT_1:4 ;

hence contradiction by A7, A9, A21, A27, RLVECT_1:11; :: thesis: verum

hence contradiction by A26, A24; :: thesis: verum

hence contradiction by A4, A23, A22; :: thesis: verum

A28: now :: thesis: not c = 0

assume
( not a <> 0 or not b <> 0 or not c <> 0 )
; :: thesis: contradictionassume A29:
c = 0
; :: thesis: contradiction

then 0. V = ((a * o) + (b * u)) + (0. V) by A6, RLVECT_1:10

.= (a * o) + (b * u) by RLVECT_1:4 ;

then a * o = - (b * u) by RLVECT_1:6

.= b * (- u) by RLVECT_1:25 ;

then A30: a * o = (- b) * u by RLVECT_1:24;

A31: ( a <> 0 & b <> 0 )

hence contradiction by A2, A31, A30; :: thesis: verum

end;then 0. V = ((a * o) + (b * u)) + (0. V) by A6, RLVECT_1:10

.= (a * o) + (b * u) by RLVECT_1:4 ;

then a * o = - (b * u) by RLVECT_1:6

.= b * (- u) by RLVECT_1:25 ;

then A30: a * o = (- b) * u by RLVECT_1:24;

A31: ( a <> 0 & b <> 0 )

proof

hence contradiction by A34, A32; :: thesis: verum

end;

then
- b <> 0
;A32: now :: thesis: not b = 0

assume A33:
b = 0
; :: thesis: contradiction

then 0. V = ((a * o) + (0 * u)) + (0. V) by A6, A29, RLVECT_1:10

.= (a * o) + (0 * u) by RLVECT_1:4

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

.= a * o by RLVECT_1:4 ;

hence contradiction by A7, A10, A29, A33, RLVECT_1:11; :: thesis: verum

end;then 0. V = ((a * o) + (0 * u)) + (0. V) by A6, A29, RLVECT_1:10

.= (a * o) + (0 * u) by RLVECT_1:4

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

.= a * o by RLVECT_1:4 ;

hence contradiction by A7, A10, A29, A33, RLVECT_1:11; :: thesis: verum

A34: now :: thesis: not a = 0

assume
( not a <> 0 or not b <> 0 )
; :: thesis: contradictionassume A35:
a = 0
; :: thesis: contradiction

then 0. V = ((0. V) + (b * u)) + (0 * u2) by A6, A29, RLVECT_1:10

.= (b * u) + (0 * u2) by RLVECT_1:4

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

.= b * u by RLVECT_1:4 ;

hence contradiction by A7, A8, A29, A35, RLVECT_1:11; :: thesis: verum

end;then 0. V = ((0. V) + (b * u)) + (0 * u2) by A6, A29, RLVECT_1:10

.= (b * u) + (0 * u2) by RLVECT_1:4

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

.= b * u by RLVECT_1:4 ;

hence contradiction by A7, A8, A29, A35, RLVECT_1:11; :: thesis: verum

hence contradiction by A34, A32; :: thesis: verum

hence contradiction by A2, A31, A30; :: thesis: verum

hence contradiction by A20, A12, A28; :: thesis: verum

a " <> 0 by A11, XCMPLX_1:202;

then A37: ( (a ") * b <> 0 & - ((a ") * c) <> 0 ) by A11, XCMPLX_1:6;

(a ") * (- (c * u2)) = (a ") * ((a * o) + (b * u)) by A6, RLVECT_1:6

.= ((a ") * (a * o)) + ((a ") * (b * u)) by RLVECT_1:def 5

.= (((a ") * a) * o) + ((a ") * (b * u)) by RLVECT_1:def 7

.= (((a ") * a) * o) + (((a ") * b) * u) by RLVECT_1:def 7

.= (1 * o) + (((a ") * b) * u) by A11, XCMPLX_0:def 7

.= o + (((a ") * b) * u) by RLVECT_1:def 8 ;

then o + (((a ") * b) * u) = (a ") * (c * (- u2)) by RLVECT_1:25

.= ((a ") * c) * (- u2) by RLVECT_1:def 7

.= (- ((a ") * c)) * u2 by RLVECT_1:24 ;

hence ex a1, b1 being Real st

( b1 * u2 = o + (a1 * u) & a1 <> 0 & b1 <> 0 ) by A37; :: thesis: ex a2, c2 being Real st

( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 )

- b <> 0 by A11;

then A38: (c ") * (- b) <> 0 by A36, XCMPLX_1:6;

c * u2 = - ((a * o) + (b * u)) by A6, RLVECT_1:def 10

.= (- (a * o)) + (- (b * u)) by RLVECT_1:31

.= ((- a) * o) + (- (b * u)) by Lm8

.= ((- a) * o) + ((- b) * u) by Lm8 ;

then (c ") * (c * u2) = ((c ") * ((- a) * o)) + ((c ") * ((- b) * u)) by RLVECT_1:def 5

.= (((c ") * (- a)) * o) + ((c ") * ((- b) * u)) by RLVECT_1:def 7

.= (((c ") * (- a)) * o) + (((c ") * (- b)) * u) by RLVECT_1:def 7 ;

then A39: (((c ") * (- a)) * o) + (((c ") * (- b)) * u) = ((c ") * c) * u2 by RLVECT_1:def 7

.= 1 * u2 by A11, XCMPLX_0:def 7

.= u2 by RLVECT_1:def 8 ;

- a <> 0 by A11;

then (c ") * (- a) <> 0 by A36, XCMPLX_1:6;

hence ex a2, c2 being Real st

( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 ) by A39, A38; :: thesis: verum