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)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos 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)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos r))

let p be Point of (TOP-REAL n); :: thesis: ( 1 <= i & i < j & j <= n implies (@ p) "*" (Col ((Rotation (i,j,n,r)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos r)) )

assume that

A1: 1 <= i and

A2: i < j and

A3: j <= n ; :: thesis: (@ p) "*" (Col ((Rotation (i,j,n,r)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos r))

set O = Rotation (i,j,n,r);

set C = Col ((Rotation (i,j,n,r)),j);

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)),j)) . j = (Rotation (i,j,n,r)) * (j,j) by A4, MATRIX_0:def 8;

A8: i <= n by A2, A3, XXREAL_0:2;

then A9: i in Seg n by A1;

then A10: (Col ((Rotation (i,j,n,r)),j)) . i = (Rotation (i,j,n,r)) * (i,j) by A6, MATRIX_0:def 8;

( len p = n & len (Col ((Rotation (i,j,n,r)),j)) = n ) by A5, CARD_1:def 7;

then len (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) = n by MATRIX_3:6;

then A11: dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) = Seg n by FINSEQ_1:def 3;

then A12: i in dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) by A1, A8;

A13: 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)),j)))) & k <> i & k <> j holds

(mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . k = 0. F_Real

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)),j)))) /. i = (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . i by A9, A11, PARTFUN1:def 6

.= pii * ((Rotation (i,j,n,r)) * (i,j)) by A10, A12, FVSUM_1:60

.= (p . i) * (sin r) by A1, A2, A3, Def3 ;

(mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) /. j = (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . j by A4, A11, PARTFUN1:def 6

.= pj * ((Rotation (i,j,n,r)) * (j,j)) by A4, A7, A11, FVSUM_1:60

.= (p . j) * (cos r) by A1, A2, A3, Def3 ;

hence (@ p) "*" (Col ((Rotation (i,j,n,r)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos r)) by A19, A20; :: thesis: verum

for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n holds

(@ p) "*" (Col ((Rotation (i,j,n,r)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos 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)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos r))

let p be Point of (TOP-REAL n); :: thesis: ( 1 <= i & i < j & j <= n implies (@ p) "*" (Col ((Rotation (i,j,n,r)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos r)) )

assume that

A1: 1 <= i and

A2: i < j and

A3: j <= n ; :: thesis: (@ p) "*" (Col ((Rotation (i,j,n,r)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos r))

set O = Rotation (i,j,n,r);

set C = Col ((Rotation (i,j,n,r)),j);

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)),j)) . j = (Rotation (i,j,n,r)) * (j,j) by A4, MATRIX_0:def 8;

A8: i <= n by A2, A3, XXREAL_0:2;

then A9: i in Seg n by A1;

then A10: (Col ((Rotation (i,j,n,r)),j)) . i = (Rotation (i,j,n,r)) * (i,j) by A6, MATRIX_0:def 8;

( len p = n & len (Col ((Rotation (i,j,n,r)),j)) = n ) by A5, CARD_1:def 7;

then len (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) = n by MATRIX_3:6;

then A11: dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) = Seg n by FINSEQ_1:def 3;

then A12: i in dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) by A1, A8;

A13: 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)),j)))) & k <> i & k <> j holds

(mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . k = 0. F_Real

proof

then A19:
Sum (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) = ((mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) /. i) + ((mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) /. j)
by A2, A4, A9, A11, MATRIX15:7;
let k be Nat; :: thesis: ( k in dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) & k <> i & k <> j implies (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . k = 0. F_Real )

assume that

A14: k in dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) and

A15: k <> i and

A16: k <> j ; :: thesis: (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . k = 0. F_Real

not k in {i,j} by A15, A16, TARSKI:def 2;

then A17: {k,j} <> {i,j} by TARSKI:def 2;

reconsider pk = (@ p) . k as Element of F_Real by XREAL_0:def 1;

A18: [k,j] in Indices (Rotation (i,j,n,r)) by A4, A11, A13, A14, ZFMISC_1:87;

(Col ((Rotation (i,j,n,r)),j)) . k = (Rotation (i,j,n,r)) * (k,j) by A6, A11, A14, MATRIX_0:def 8;

hence (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . k = pk * ((Rotation (i,j,n,r)) * (k,j)) by A14, FVSUM_1:60

.= pk * (0. F_Real) by A1, A2, A3, A16, A17, A18, Def3

.= 0. F_Real ;

:: thesis: verum

end;assume that

A14: k in dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) and

A15: k <> i and

A16: k <> j ; :: thesis: (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . k = 0. F_Real

not k in {i,j} by A15, A16, TARSKI:def 2;

then A17: {k,j} <> {i,j} by TARSKI:def 2;

reconsider pk = (@ p) . k as Element of F_Real by XREAL_0:def 1;

A18: [k,j] in Indices (Rotation (i,j,n,r)) by A4, A11, A13, A14, ZFMISC_1:87;

(Col ((Rotation (i,j,n,r)),j)) . k = (Rotation (i,j,n,r)) * (k,j) by A6, A11, A14, MATRIX_0:def 8;

hence (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . k = pk * ((Rotation (i,j,n,r)) * (k,j)) by A14, FVSUM_1:60

.= pk * (0. F_Real) by A1, A2, A3, A16, A17, A18, Def3

.= 0. F_Real ;

:: thesis: verum

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)),j)))) /. i = (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . i by A9, A11, PARTFUN1:def 6

.= pii * ((Rotation (i,j,n,r)) * (i,j)) by A10, A12, FVSUM_1:60

.= (p . i) * (sin r) by A1, A2, A3, Def3 ;

(mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) /. j = (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . j by A4, A11, PARTFUN1:def 6

.= pj * ((Rotation (i,j,n,r)) * (j,j)) by A4, A7, A11, FVSUM_1:60

.= (p . j) * (cos r) by A1, A2, A3, Def3 ;

hence (@ p) "*" (Col ((Rotation (i,j,n,r)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos r)) by A19, A20; :: thesis: verum