let r be Real; :: thesis: for i, j, n being Nat
for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n holds
((Mx2Tran (Rotation (i,j,n,r))) . p) . i = ((p . i) * (cos r)) + ((p . j) * (- (sin r)))
let i, j, n be Nat; :: thesis: for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n holds
((Mx2Tran (Rotation (i,j,n,r))) . p) . i = ((p . i) * (cos r)) + ((p . j) * (- (sin r)))
let p be Point of (TOP-REAL n); :: thesis: ( 1 <= i & i < j & j <= n implies ((Mx2Tran (Rotation (i,j,n,r))) . p) . i = ((p . i) * (cos r)) + ((p . j) * (- (sin r))) )
set O = Rotation (i,j,n,r);
set M = Mx2Tran (Rotation (i,j,n,r));
set Mp = (Mx2Tran (Rotation (i,j,n,r))) . p;
set S = Seg n;
assume that
A1: 1 <= i and
A2: ( i < j & j <= n ) ; :: thesis: ((Mx2Tran (Rotation (i,j,n,r))) . p) . i = ((p . i) * (cos r)) + ((p . j) * (- (sin r)))
i <= n by A2, XXREAL_0:2;
hence ((Mx2Tran (Rotation (i,j,n,r))) . p) . i = (@ p) "*" (Col ((Rotation (i,j,n,r)),i)) by A1, MATRTOP1:18
.= ((p . i) * (cos r)) + ((p . j) * (- (sin r))) by A1, A2, Th15 ;
:: thesis: verum