let r be Real; 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 by XREAL_0:def 1;
A2:
sqr <*pk*> = <*(pk ^2)*>
by RVSUM_1:55;
reconsider pij1 = (pk * (cos r)) + (pj * (- (sin r))), pij2 = (pk * (sin r)) + (pj * (cos r)) as Element of REAL by XREAL_0:def 1;
A3:
sqr <*pij1*> = <*(pij1 ^2)*>
by RVSUM_1:55;
A4:
sqr <*pij2*> = <*(pij2 ^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 RVSUM_1:144
.=
((sqr (((P | (i -' 1)) ^ <*pk*>) ^ ((P /^ i) | ((j -' i) -' 1)))) ^ (sqr <*pj*>)) ^ (sqr (P /^ j))
by RVSUM_1:144
.=
(((sqr ((P | (i -' 1)) ^ <*pk*>)) ^ (sqr ((P /^ i) | ((j -' i) -' 1)))) ^ (sqr <*pj*>)) ^ (sqr (P /^ j))
by RVSUM_1:144
.=
((((sqr (P | (i -' 1))) ^ (sqr <*pk*>)) ^ (sqr ((P /^ i) | ((j -' i) -' 1)))) ^ (sqr <*pj*>)) ^ (sqr (P /^ j))
by RVSUM_1:144
;
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: (pij1 ^2) + (pij2 ^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)) ^ <*pij1*>) ^ ((P /^ i) | ((j -' i) -' 1))) ^ <*pij2*>) ^ (P /^ j)
by A1, Th23;
then sqr ((Mx2Tran (Rotation (i,j,n,r))) . p) =
(sqr ((((P | (i -' 1)) ^ <*pij1*>) ^ ((P /^ i) | ((j -' i) -' 1))) ^ <*pij2*>)) ^ (sqr (P /^ j))
by RVSUM_1:144
.=
((sqr (((P | (i -' 1)) ^ <*pij1*>) ^ ((P /^ i) | ((j -' i) -' 1)))) ^ (sqr <*pij2*>)) ^ (sqr (P /^ j))
by RVSUM_1:144
.=
(((sqr ((P | (i -' 1)) ^ <*pij1*>)) ^ (sqr ((P /^ i) | ((j -' i) -' 1)))) ^ (sqr <*pij2*>)) ^ (sqr (P /^ j))
by RVSUM_1:144
.=
((((sqr (P | (i -' 1))) ^ (sqr <*pij1*>)) ^ (sqr ((P /^ i) | ((j -' i) -' 1)))) ^ (sqr <*pij2*>)) ^ (sqr (P /^ j))
by RVSUM_1:144
;
then Sum (sqr ((Mx2Tran (Rotation (i,j,n,r))) . p)) =
(Sum ((((sqr (P | (i -' 1))) ^ (sqr <*pij1*>)) ^ (sqr ((P /^ i) | ((j -' i) -' 1)))) ^ (sqr <*pij2*>))) + (Sum (sqr (P /^ j)))
by RVSUM_1:75
.=
((Sum (((sqr (P | (i -' 1))) ^ (sqr <*pij1*>)) ^ (sqr ((P /^ i) | ((j -' i) -' 1))))) + (pij2 ^2)) + (Sum (sqr (P /^ j)))
by A4, RVSUM_1:74
.=
(((Sum ((sqr (P | (i -' 1))) ^ (sqr <*pij1*>))) + (Sum (sqr ((P /^ i) | ((j -' i) -' 1))))) + (pij2 ^2)) + (Sum (sqr (P /^ j)))
by RVSUM_1:75
.=
((((Sum (sqr (P | (i -' 1)))) + (pij1 ^2)) + (Sum (sqr ((P /^ i) | ((j -' i) -' 1))))) + (pij2 ^2)) + (Sum (sqr (P /^ j)))
by A3, RVSUM_1:74
;
hence
|.p.| = |.((Mx2Tran (Rotation (i,j,n,r))) . p).|
by A6, A8; verum