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
proof
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 )
proof
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;
A14: now :: thesis: not a = 0
assume 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;
assume ( not a <> 0 or not b <> 0 ) ; :: thesis: contradiction
hence contradiction by A14, A12; :: thesis: verum
end;
then - b <> 0 ;
hence contradiction by A2, A11, A10; :: thesis: verum
end;
c * r = - ((a * p) + (b * q)) by A4, RLVECT_1:def 10
.= (- (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