let V be RealLinearSpace; for u, x, y being VECTOR of V
for n being Real st Gen x,y holds
Ortm (x,y,(n * u)) = n * (Ortm (x,y,u))
let u, x, y be VECTOR of V; for n being Real st Gen x,y holds
Ortm (x,y,(n * u)) = n * (Ortm (x,y,u))
let n be Real; ( Gen x,y implies Ortm (x,y,(n * u)) = n * (Ortm (x,y,u)) )
assume A1:
Gen x,y
; Ortm (x,y,(n * u)) = n * (Ortm (x,y,u))
hence Ortm (x,y,(n * u)) =
((n * (pr1 (x,y,u))) * x) + ((- (pr2 (x,y,(n * u)))) * y)
by Lm7
.=
((n * (pr1 (x,y,u))) * x) + ((- (n * (pr2 (x,y,u)))) * y)
by A1, Lm7
.=
((n * (pr1 (x,y,u))) * x) + ((n * (pr2 (x,y,u))) * (- y))
by RLVECT_1:24
.=
((n * (pr1 (x,y,u))) * x) + (- ((n * (pr2 (x,y,u))) * y))
by RLVECT_1:25
.=
((n * (pr1 (x,y,u))) * x) + (- (n * ((pr2 (x,y,u)) * y)))
by RLVECT_1:def 7
.=
((n * (pr1 (x,y,u))) * x) + (n * (- ((pr2 (x,y,u)) * y)))
by RLVECT_1:25
.=
(n * ((pr1 (x,y,u)) * x)) + (n * (- ((pr2 (x,y,u)) * y)))
by RLVECT_1:def 7
.=
n * (((pr1 (x,y,u)) * x) + (- ((pr2 (x,y,u)) * y)))
by RLVECT_1:def 5
.=
n * (((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * (- y)))
by RLVECT_1:25
.=
n * (Ortm (x,y,u))
by RLVECT_1:24
;
verum