let V be RealLinearSpace; :: thesis: for o, p, q, r, s being Element of V
for a, b being Real st q = o + (a * p) & r = o + (b * s) & are_Prop q,r & a <> 0 holds
o,p,s are_LinDep
let o, p, q, r, s be Element of V; :: thesis: for a, b being Real st q = o + (a * p) & r = o + (b * s) & are_Prop q,r & a <> 0 holds
o,p,s are_LinDep
let a, b be Real; :: thesis: ( q = o + (a * p) & r = o + (b * s) & are_Prop q,r & a <> 0 implies o,p,s are_LinDep )
assume that
A1: ( q = o + (a * p) & r = o + (b * s) & are_Prop q,r ) and
A2: a <> 0 ; :: thesis: o,p,s are_LinDep
consider A being Real such that
A <> 0 and
A3: o + (a * p) = A * (o + (b * s)) by A1, ANPROJ_1:1;
o + (a * p) = (A * o) + (A * (b * s)) by A3, RLVECT_1:def 5
.= (A * o) + ((A * b) * s) by RLVECT_1:def 7 ;
then (- (A * o)) + (o + (a * p)) = ((- (A * o)) + (A * o)) + ((A * b) * s) by RLVECT_1:def 3
.= (0. V) + ((A * b) * s) by RLVECT_1:5
.= (A * b) * s by RLVECT_1:4 ;
then ((- (A * o)) + o) + (a * p) = (A * b) * s by RLVECT_1:def 3;
then (A * b) * s = (((- A) * o) + o) + (a * p) by Lm8
.= (((- A) * o) + (1 * o)) + (a * p) by RLVECT_1:def 8
.= (((- A) + 1) * o) + (a * p) by RLVECT_1:def 6 ;
then ((((- A) + 1) * o) + (a * p)) + (- ((A * b) * s)) = 0. V by RLVECT_1:5;
then 0. V = ((((- A) + 1) * o) + (a * p)) + ((- (A * b)) * s) by Lm8;
hence o,p,s are_LinDep by A2; :: thesis: verum