let V be RealLinearSpace; :: thesis: for u, v, x, y being VECTOR of V st Gen x,y holds
Ortm (x,y,(u + v)) = (Ortm (x,y,u)) + (Ortm (x,y,v))
let u, v, x, y 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 6
.= (((pr1 (x,y,u)) * x) + ((pr1 (x,y,v)) * x)) + (((pr2 (x,y,u)) + (pr2 (x,y,v))) * (- y)) by RLVECT_1:24
.= (((pr1 (x,y,u)) * x) + ((pr1 (x,y,v)) * x)) + (- (((pr2 (x,y,u)) + (pr2 (x,y,v))) * y)) by RLVECT_1:25
.= (((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) + ((pr1 (x,y,v)) * x)) + ((- ((pr2 (x,y,u)) * y)) + (- ((pr2 (x,y,v)) * y))) by RLVECT_1:31
.= ((pr1 (x,y,u)) * x) + (((pr1 (x,y,v)) * x) + ((- ((pr2 (x,y,u)) * y)) + (- ((pr2 (x,y,v)) * y)))) by RLVECT_1:def 3
.= ((pr1 (x,y,u)) * x) + ((- ((pr2 (x,y,u)) * y)) + (((pr1 (x,y,v)) * x) + (- ((pr2 (x,y,v)) * y)))) by RLVECT_1:def 3
.= (((pr1 (x,y,u)) * x) + (- ((pr2 (x,y,u)) * y))) + (((pr1 (x,y,v)) * x) + (- ((pr2 (x,y,v)) * y))) by RLVECT_1:def 3
.= (((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * (- y))) + (((pr1 (x,y,v)) * x) + (- ((pr2 (x,y,v)) * y))) by RLVECT_1:25
.= (((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * (- y))) + (((pr1 (x,y,v)) * x) + ((pr2 (x,y,v)) * (- y))) by RLVECT_1:25
.= (((pr1 (x,y,u)) * x) + ((- (pr2 (x,y,u))) * y)) + (((pr1 (x,y,v)) * x) + ((pr2 (x,y,v)) * (- y))) by RLVECT_1:24
.= (Ortm (x,y,u)) + (Ortm (x,y,v)) by RLVECT_1:24 ;
:: thesis: verum