let V be RealLinearSpace; 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; ( 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
; 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
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)
; verum