let V be RealLinearSpace; :: thesis: for p, q, r being Element of V st p,q,r are_LinDep & not are_Prop p,q & p,q,r are_Prop_Vect holds

ex a, b being Real st r = (a * p) + (b * q)

let p, q, r be Element of V; :: thesis: ( p,q,r are_LinDep & not are_Prop p,q & p,q,r are_Prop_Vect implies ex a, b being Real st r = (a * p) + (b * q) )

assume that

A1: p,q,r are_LinDep and

A2: not are_Prop p,q and

A3: p,q,r are_Prop_Vect ; :: thesis: ex a, b being Real st r = (a * p) + (b * q)

consider a, b, c being Real such that

A4: ((a * p) + (b * q)) + (c * r) = 0. V and

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

not q is zero by A3;

then A6: q <> 0. V ;

not p is zero by A3;

then A7: p <> 0. V ;

A8: c <> 0

.= (- (a * p)) + (- (b * q)) by RLVECT_1:31

.= ((- a) * p) + (- (b * q)) by Lm8

.= ((- a) * p) + ((- b) * q) by Lm8 ;

then (c ") * (c * r) = ((c ") * ((- a) * p)) + ((c ") * ((- b) * q)) by RLVECT_1:def 5

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

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

then (((c ") * (- a)) * p) + (((c ") * (- b)) * q) = ((c ") * c) * r by RLVECT_1:def 7

.= 1 * r by A8, XCMPLX_0:def 7

.= r by RLVECT_1:def 8 ;

hence ex a, b being Real st r = (a * p) + (b * q) ; :: thesis: verum

ex a, b being Real st r = (a * p) + (b * q)

let p, q, r be Element of V; :: thesis: ( p,q,r are_LinDep & not are_Prop p,q & p,q,r are_Prop_Vect implies ex a, b being Real st r = (a * p) + (b * q) )

assume that

A1: p,q,r are_LinDep and

A2: not are_Prop p,q and

A3: p,q,r are_Prop_Vect ; :: thesis: ex a, b being Real st r = (a * p) + (b * q)

consider a, b, c being Real such that

A4: ((a * p) + (b * q)) + (c * r) = 0. V and

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

not q is zero by A3;

then A6: q <> 0. V ;

not p is zero by A3;

then A7: p <> 0. V ;

A8: c <> 0

proof

c * r =
- ((a * p) + (b * q))
by A4, RLVECT_1:def 10
assume A9:
not c <> 0
; :: thesis: contradiction

then 0. V = ((a * p) + (b * q)) + (0. V) by A4, RLVECT_1:10

.= (a * p) + (b * q) by RLVECT_1:4 ;

then A10: a * p = - (b * q) by RLVECT_1:6

.= (- b) * q by Lm8 ;

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

hence contradiction by A2, A11, A10; :: thesis: verum

end;then 0. V = ((a * p) + (b * q)) + (0. V) by A4, RLVECT_1:10

.= (a * p) + (b * q) by RLVECT_1:4 ;

then A10: a * p = - (b * q) by RLVECT_1:6

.= (- b) * q by Lm8 ;

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

proof

hence contradiction by A14, A12; :: thesis: verum

end;

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

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

then 0. V = ((a * p) + (0. V)) + (0 * r) by A4, A9, RLVECT_1:10

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

.= (a * p) + (0. V) by RLVECT_1:4

.= a * p by RLVECT_1:4 ;

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

end;then 0. V = ((a * p) + (0. V)) + (0 * r) by A4, A9, RLVECT_1:10

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

.= (a * p) + (0. V) by RLVECT_1:4

.= a * p by RLVECT_1:4 ;

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

A14: now :: thesis: not a = 0

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

then 0. V = ((0. V) + (b * q)) + (0 * r) by A4, A9, RLVECT_1:10

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

.= (b * q) + (0. V) by RLVECT_1:4

.= b * q by RLVECT_1:4 ;

hence contradiction by A6, A5, A9, A15, RLVECT_1:11; :: thesis: verum

end;then 0. V = ((0. V) + (b * q)) + (0 * r) by A4, A9, RLVECT_1:10

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

.= (b * q) + (0. V) by RLVECT_1:4

.= b * q by RLVECT_1:4 ;

hence contradiction by A6, A5, A9, A15, RLVECT_1:11; :: thesis: verum

hence contradiction by A14, A12; :: thesis: verum

hence contradiction by A2, A11, A10; :: thesis: verum

.= (- (a * p)) + (- (b * q)) by RLVECT_1:31

.= ((- a) * p) + (- (b * q)) by Lm8

.= ((- a) * p) + ((- b) * q) by Lm8 ;

then (c ") * (c * r) = ((c ") * ((- a) * p)) + ((c ") * ((- b) * q)) by RLVECT_1:def 5

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

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

then (((c ") * (- a)) * p) + (((c ") * (- b)) * q) = ((c ") * c) * r by RLVECT_1:def 7

.= 1 * r by A8, XCMPLX_0:def 7

.= r by RLVECT_1:def 8 ;

hence ex a, b being Real st r = (a * p) + (b * q) ; :: thesis: verum