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

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

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

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;
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;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

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