let V be RealLinearSpace; :: thesis: for q, o, p, 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 q, o, p, 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 A1: ( q = o + (a * p) & r = o + (b * s) & are_Prop q,r & a <> 0 ) ; :: thesis: o,p,s are_LinDep
then consider A being Real such that
A2: ( A <> 0 & o + (a * p) = A * (o + (b * s)) ) by ANPROJ_1:5;
o + (a * p) = (A * o) + (A * (b * s)) by A2, RLVECT_1:def 9
.= (A * o) + ((A * b) * s) by RLVECT_1:def 9 ;
then (- (A * o)) + (o + (a * p)) = ((- (A * o)) + (A * o)) + ((A * b) * s) by RLVECT_1:def 6
.= (0. V) + ((A * b) * s) by RLVECT_1:16
.= (A * b) * s by RLVECT_1:10 ;
then ((- (A * o)) + o) + (a * p) = (A * b) * s by RLVECT_1:def 6;
then (A * b) * s = (((- A) * o) + o) + (a * p) by Lm8
.= (((- A) * o) + (1 * o)) + (a * p) by RLVECT_1:def 9
.= (((- A) + 1) * o) + (a * p) by RLVECT_1:def 9 ;
then ((((- A) + 1) * o) + (a * p)) + (- ((A * b) * s)) = 0. V by RLVECT_1:16;
then 0. V = ((((- A) + 1) * o) + (a * p)) + ((- (A * b)) * s) by Lm8;
hence o,p,s are_LinDep by A1, ANPROJ_1:def 3; :: thesis: verum