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
(@ p) "*" (Col ((Rotation (i,j,n,r)),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
(@ p) "*" (Col ((Rotation (i,j,n,r)),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 (@ p) "*" (Col ((Rotation (i,j,n,r)),i)) = ((p . i) * (cos r)) + ((p . j) * (- (sin r))) )
assume that
A1: 1 <= i and
A2: i < j and
A3: j <= n ; :: thesis: (@ p) "*" (Col ((Rotation (i,j,n,r)),i)) = ((p . i) * (cos r)) + ((p . j) * (- (sin r)))
set O = Rotation (i,j,n,r);
set C = Col ((Rotation (i,j,n,r)),i);
set S = Seg n;
1 <= j by A1, A2, XXREAL_0:2;
then A4: j in Seg n by A3;
A5: len (Rotation (i,j,n,r)) = n by MATRIX_0:25;
then A6: dom (Rotation (i,j,n,r)) = Seg n by FINSEQ_1:def 3;
then A7: (Col ((Rotation (i,j,n,r)),i)) . j = (Rotation (i,j,n,r)) * (j,i) by A4, MATRIX_0:def 8;
i <= n by A2, A3, XXREAL_0:2;
then A8: i in Seg n by A1;
then A9: (Col ((Rotation (i,j,n,r)),i)) . i = (Rotation (i,j,n,r)) * (i,i) by A6, MATRIX_0:def 8;
( len p = n & len (Col ((Rotation (i,j,n,r)),i)) = n ) by A5, CARD_1:def 7;
then A10: len (mlt ((@ p),(Col ((Rotation (i,j,n,r)),i)))) = n by MATRIX_3:6;
then A11: dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),i)))) = Seg n by FINSEQ_1:def 3;
A12: Indices (Rotation (i,j,n,r)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
for k being Nat st k in dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),i)))) & k <> i & k <> j holds
(mlt ((@ p),(Col ((Rotation (i,j,n,r)),i)))) . k = 0. F_Real

proof

let k be Nat; :: thesis: ( k in dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),i)))) & k <> i & k <> j implies (mlt ((@ p),(Col ((Rotation (i,j,n,r)),i)))) . k = 0. F_Real )
assume that
A13: k in dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),i)))) and
A14: k <> i and
A15: k <> j ; :: thesis: (mlt ((@ p),(Col ((Rotation (i,j,n,r)),i)))) . k = 0. F_Real
not k in {i,j} by A14, A15, TARSKI:def 2;
then A16: {k,i} <> {i,j} by TARSKI:def 2;
reconsider pk = (@ p) . k as Element of F_Real by XREAL_0:def 1;
A17: [k,i] in Indices (Rotation (i,j,n,r)) by A8, A11, A12, A13, ZFMISC_1:87;
(Col ((Rotation (i,j,n,r)),i)) . k = (Rotation (i,j,n,r)) * (k,i) by A6, A11, A13, MATRIX_0:def 8;
hence (mlt ((@ p),(Col ((Rotation (i,j,n,r)),i)))) . k = pk * ((Rotation (i,j,n,r)) * (k,i)) by A13, FVSUM_1:60
.= pk * (0. F_Real) by A1, A2, A3, A14, A16, A17, Def3
.= 0. F_Real ;
:: thesis: verum

end;

then A18: Sum (mlt ((@ p),(Col ((Rotation (i,j,n,r)),i)))) = ((mlt ((@ p),(Col ((Rotation (i,j,n,r)),i)))) /. i) + ((mlt ((@ p),(Col ((Rotation (i,j,n,r)),i)))) /. j) by A2, A4, A8, A11, MATRIX15:7;
A19: i in dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),i)))) by A8, A10, FINSEQ_1:def 3;
reconsider pii = (@ p) . i, pj = (@ p) . j as Element of F_Real by XREAL_0:def 1;
A20: (mlt ((@ p),(Col ((Rotation (i,j,n,r)),i)))) /. i = (mlt ((@ p),(Col ((Rotation (i,j,n,r)),i)))) . i by A8, A11, PARTFUN1:def 6
.= pii * ((Rotation (i,j,n,r)) * (i,i)) by A9, A19, FVSUM_1:60
.= (p . i) * (cos r) by A1, A2, A3, Def3 ;
(mlt ((@ p),(Col ((Rotation (i,j,n,r)),i)))) /. j = (mlt ((@ p),(Col ((Rotation (i,j,n,r)),i)))) . j by A4, A11, PARTFUN1:def 6
.= pj * ((Rotation (i,j,n,r)) * (j,i)) by A4, A7, A11, FVSUM_1:60
.= (p . j) * (- (sin r)) by A1, A2, A3, Def3 ;
hence (@ p) "*" (Col ((Rotation (i,j,n,r)),i)) = ((p . i) * (cos r)) + ((p . j) * (- (sin r))) by A18, A20; :: thesis: verum