let V be RealLinearSpace; :: thesis: for u, v, w, y being VECTOR of V
for a, b being Real st u,v are_Ort_wrt w,y holds
a * u,b * v are_Ort_wrt w,y
let u, v, w, y be VECTOR of V; :: thesis: for a, b being Real st u,v are_Ort_wrt w,y holds
a * u,b * v are_Ort_wrt w,y
let a, b be Real; :: thesis: ( u,v are_Ort_wrt w,y implies a * u,b * v are_Ort_wrt w,y )
assume u,v are_Ort_wrt w,y ; :: thesis: a * u,b * v are_Ort_wrt w,y
then consider a1, a2, b1, b2 being Real such that
A1: u = (a1 * w) + (a2 * y) and
A2: v = (b1 * w) + (b2 * y) and
A3: (a1 * b1) + (a2 * b2) = 0 ;
A4: b * v = (b * (b1 * w)) + (b * (b2 * y)) by A2, RLVECT_1:def 5
.= ((b * b1) * w) + (b * (b2 * y)) by RLVECT_1:def 7
.= ((b * b1) * w) + ((b * b2) * y) by RLVECT_1:def 7 ;
A5: ((a * a1) * (b * b1)) + ((a * a2) * (b * b2)) = (b * a) * ((a1 * b1) + (a2 * b2))
.= 0 by A3 ;
a * u = (a * (a1 * w)) + (a * (a2 * y)) by A1, RLVECT_1:def 5
.= ((a * a1) * w) + (a * (a2 * y)) by RLVECT_1:def 7
.= ((a * a1) * w) + ((a * a2) * y) by RLVECT_1:def 7 ;
hence a * u,b * v are_Ort_wrt w,y by A4, A5; :: thesis: verum