let r be real number ; for i, j, n being Nat st 1 <= i & i < j & j <= n holds
Mx2Tran (Rotation (i,j,n,r)) is rotation
let i, j, n be Nat; ( 1 <= i & i < j & j <= n implies Mx2Tran (Rotation (i,j,n,r)) is rotation )
assume A1:
( 1 <= i & i < j & j <= n )
; Mx2Tran (Rotation (i,j,n,r)) is rotation
let p be Point of (TOP-REAL n); MATRTOP3:def 4 |.p.| = |.((Mx2Tran (Rotation (i,j,n,r))) . p).|
p = @ (@ p)
;
then reconsider P = p as FinSequence of REAL ;
set M = Mx2Tran (Rotation (i,j,n,r));
set Mp = (Mx2Tran (Rotation (i,j,n,r))) . p;
set p1 = P | (i -' 1);
set p2 = (P /^ i) | ((j -' i) -' 1);
set p3 = P /^ j;
set s = sin r;
set c = cos r;
reconsider pk = P . i, pj = P . j as Element of REAL ;
A2:
sqr <*pk*> = <*(pk ^2)*>
by RVSUM_1:55;
set pij1 = (pk * (cos r)) + (pj * (- (sin r)));
set pij2 = (pk * (sin r)) + (pj * (cos r));
A3:
sqr <*((pk * (cos r)) + (pj * (- (sin r))))*> = <*(((pk * (cos r)) + (pj * (- (sin r)))) ^2)*>
by RVSUM_1:55;
A4:
sqr <*((pk * (sin r)) + (pj * (cos r)))*> = <*(((pk * (sin r)) + (pj * (cos r))) ^2)*>
by RVSUM_1:55;
A5:
sqr <*pj*> = <*(pj ^2)*>
by RVSUM_1:55;
len p = n
by CARD_1:def 7;
then
p = ((((P | (i -' 1)) ^ <*pk*>) ^ ((P /^ i) | ((j -' i) -' 1))) ^ <*pj*>) ^ (P /^ j)
by A1, FINSEQ_7:1;
then sqr p =
(sqr ((((P | (i -' 1)) ^ <*pk*>) ^ ((P /^ i) | ((j -' i) -' 1))) ^ <*pj*>)) ^ (sqr (P /^ j))
by TOPREAL7:10
.=
((sqr (((P | (i -' 1)) ^ <*pk*>) ^ ((P /^ i) | ((j -' i) -' 1)))) ^ (sqr <*pj*>)) ^ (sqr (P /^ j))
by TOPREAL7:10
.=
(((sqr ((P | (i -' 1)) ^ <*pk*>)) ^ (sqr ((P /^ i) | ((j -' i) -' 1)))) ^ (sqr <*pj*>)) ^ (sqr (P /^ j))
by TOPREAL7:10
.=
((((sqr (P | (i -' 1))) ^ (sqr <*pk*>)) ^ (sqr ((P /^ i) | ((j -' i) -' 1)))) ^ (sqr <*pj*>)) ^ (sqr (P /^ j))
by TOPREAL7:10
;
then A6: Sum (sqr p) =
(Sum ((((sqr (P | (i -' 1))) ^ (sqr <*pk*>)) ^ (sqr ((P /^ i) | ((j -' i) -' 1)))) ^ (sqr <*pj*>))) + (Sum (sqr (P /^ j)))
by RVSUM_1:75
.=
((Sum (((sqr (P | (i -' 1))) ^ (sqr <*pk*>)) ^ (sqr ((P /^ i) | ((j -' i) -' 1))))) + (pj ^2)) + (Sum (sqr (P /^ j)))
by A5, RVSUM_1:74
.=
(((Sum ((sqr (P | (i -' 1))) ^ (sqr <*pk*>))) + (Sum (sqr ((P /^ i) | ((j -' i) -' 1))))) + (pj ^2)) + (Sum (sqr (P /^ j)))
by RVSUM_1:75
.=
((((Sum (sqr (P | (i -' 1)))) + (pk ^2)) + (Sum (sqr ((P /^ i) | ((j -' i) -' 1))))) + (pj ^2)) + (Sum (sqr (P /^ j)))
by A2, RVSUM_1:74
;
A7:
((cos r) * (cos r)) + ((sin r) * (sin r)) = 1
by SIN_COS:29;
A8: (((pk * (cos r)) + (pj * (- (sin r)))) ^2) + (((pk * (sin r)) + (pj * (cos r))) ^2) =
((pk * pk) * (((cos r) * (cos r)) + ((sin r) * (sin r)))) + ((pj * pj) * (((cos r) * (cos r)) + ((sin r) * (sin r))))
.=
(pk ^2) + (pj ^2)
by A7
;
(Mx2Tran (Rotation (i,j,n,r))) . p = ((((P | (i -' 1)) ^ <*((pk * (cos r)) + (pj * (- (sin r))))*>) ^ ((P /^ i) | ((j -' i) -' 1))) ^ <*((pk * (sin r)) + (pj * (cos r)))*>) ^ (P /^ j)
by A1, Th21;
then sqr ((Mx2Tran (Rotation (i,j,n,r))) . p) =
(sqr ((((P | (i -' 1)) ^ <*((pk * (cos r)) + (pj * (- (sin r))))*>) ^ ((P /^ i) | ((j -' i) -' 1))) ^ <*((pk * (sin r)) + (pj * (cos r)))*>)) ^ (sqr (P /^ j))
by TOPREAL7:10
.=
((sqr (((P | (i -' 1)) ^ <*((pk * (cos r)) + (pj * (- (sin r))))*>) ^ ((P /^ i) | ((j -' i) -' 1)))) ^ (sqr <*((pk * (sin r)) + (pj * (cos r)))*>)) ^ (sqr (P /^ j))
by TOPREAL7:10
.=
(((sqr ((P | (i -' 1)) ^ <*((pk * (cos r)) + (pj * (- (sin r))))*>)) ^ (sqr ((P /^ i) | ((j -' i) -' 1)))) ^ (sqr <*((pk * (sin r)) + (pj * (cos r)))*>)) ^ (sqr (P /^ j))
by TOPREAL7:10
.=
((((sqr (P | (i -' 1))) ^ (sqr <*((pk * (cos r)) + (pj * (- (sin r))))*>)) ^ (sqr ((P /^ i) | ((j -' i) -' 1)))) ^ (sqr <*((pk * (sin r)) + (pj * (cos r)))*>)) ^ (sqr (P /^ j))
by TOPREAL7:10
;
then Sum (sqr ((Mx2Tran (Rotation (i,j,n,r))) . p)) =
(Sum ((((sqr (P | (i -' 1))) ^ (sqr <*((pk * (cos r)) + (pj * (- (sin r))))*>)) ^ (sqr ((P /^ i) | ((j -' i) -' 1)))) ^ (sqr <*((pk * (sin r)) + (pj * (cos r)))*>))) + (Sum (sqr (P /^ j)))
by RVSUM_1:75
.=
((Sum (((sqr (P | (i -' 1))) ^ (sqr <*((pk * (cos r)) + (pj * (- (sin r))))*>)) ^ (sqr ((P /^ i) | ((j -' i) -' 1))))) + (((pk * (sin r)) + (pj * (cos r))) ^2)) + (Sum (sqr (P /^ j)))
by A4, RVSUM_1:74
.=
(((Sum ((sqr (P | (i -' 1))) ^ (sqr <*((pk * (cos r)) + (pj * (- (sin r))))*>))) + (Sum (sqr ((P /^ i) | ((j -' i) -' 1))))) + (((pk * (sin r)) + (pj * (cos r))) ^2)) + (Sum (sqr (P /^ j)))
by RVSUM_1:75
.=
((((Sum (sqr (P | (i -' 1)))) + (((pk * (cos r)) + (pj * (- (sin r)))) ^2)) + (Sum (sqr ((P /^ i) | ((j -' i) -' 1))))) + (((pk * (sin r)) + (pj * (cos r))) ^2)) + (Sum (sqr (P /^ j)))
by A3, RVSUM_1:74
;
hence
|.p.| = |.((Mx2Tran (Rotation (i,j,n,r))) . p).|
by A6, A8; verum