let V be RealLinearSpace; :: thesis: for x, y, u, v being VECTOR of V st Gen x,y holds
Ortm x,y,(u + v) = (Ortm x,y,u) + (Ortm x,y,v)
let x, y, u, v be VECTOR of V; :: thesis: ( Gen x,y implies Ortm x,y,(u + v) = (Ortm x,y,u) + (Ortm x,y,v) )
assume A1: Gen x,y ; :: thesis: Ortm x,y,(u + v) = (Ortm x,y,u) + (Ortm x,y,v)
hence Ortm x,y,(u + v) = (((pr1 x,y,u) + (pr1 x,y,v)) * x) + ((- (pr2 x,y,(u + v))) * y) by Lm7
.= (((pr1 x,y,u) + (pr1 x,y,v)) * x) + ((- ((pr2 x,y,u) + (pr2 x,y,v))) * y) by A1, Lm7
.= (((pr1 x,y,u) * x) + ((pr1 x,y,v) * x)) + ((- ((pr2 x,y,u) + (pr2 x,y,v))) * y) by RLVECT_1:def 9
.= (((pr1 x,y,u) * x) + ((pr1 x,y,v) * x)) + (((pr2 x,y,u) + (pr2 x,y,v)) * (- y)) by RLVECT_1:38
.= (((pr1 x,y,u) * x) + ((pr1 x,y,v) * x)) + (- (((pr2 x,y,u) + (pr2 x,y,v)) * y)) by RLVECT_1:39
.= (((pr1 x,y,u) * x) + ((pr1 x,y,v) * x)) + (- (((pr2 x,y,u) * y) + ((pr2 x,y,v) * y))) by RLVECT_1:def 9
.= (((pr1 x,y,u) * x) + ((pr1 x,y,v) * x)) + ((- ((pr2 x,y,u) * y)) + (- ((pr2 x,y,v) * y))) by RLVECT_1:45
.= ((pr1 x,y,u) * x) + (((pr1 x,y,v) * x) + ((- ((pr2 x,y,u) * y)) + (- ((pr2 x,y,v) * y)))) by RLVECT_1:def 6
.= ((pr1 x,y,u) * x) + ((- ((pr2 x,y,u) * y)) + (((pr1 x,y,v) * x) + (- ((pr2 x,y,v) * y)))) by RLVECT_1:def 6
.= (((pr1 x,y,u) * x) + (- ((pr2 x,y,u) * y))) + (((pr1 x,y,v) * x) + (- ((pr2 x,y,v) * y))) by RLVECT_1:def 6
.= (((pr1 x,y,u) * x) + ((pr2 x,y,u) * (- y))) + (((pr1 x,y,v) * x) + (- ((pr2 x,y,v) * y))) by RLVECT_1:39
.= (((pr1 x,y,u) * x) + ((pr2 x,y,u) * (- y))) + (((pr1 x,y,v) * x) + ((pr2 x,y,v) * (- y))) by RLVECT_1:39
.= (((pr1 x,y,u) * x) + ((- (pr2 x,y,u)) * y)) + (((pr1 x,y,v) * x) + ((pr2 x,y,v) * (- y))) by RLVECT_1:38
.= (Ortm x,y,u) + (Ortm x,y,v) by RLVECT_1:38 ;
:: thesis: verum