let r be Real; for i, j, n being Nat
for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n holds
(Mx2Tran (Rotation (i,j,n,r))) . p = ((((p | (i -' 1)) ^ <*(((p . i) * (cos r)) + ((p . j) * (- (sin r))))*>) ^ ((p /^ i) | ((j -' i) -' 1))) ^ <*(((p . i) * (sin r)) + ((p . j) * (cos r)))*>) ^ (p /^ j)
let i, j, n be Nat; for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n holds
(Mx2Tran (Rotation (i,j,n,r))) . p = ((((p | (i -' 1)) ^ <*(((p . i) * (cos r)) + ((p . j) * (- (sin r))))*>) ^ ((p /^ i) | ((j -' i) -' 1))) ^ <*(((p . i) * (sin r)) + ((p . j) * (cos r)))*>) ^ (p /^ j)
let p be Point of (TOP-REAL n); ( 1 <= i & i < j & j <= n implies (Mx2Tran (Rotation (i,j,n,r))) . p = ((((p | (i -' 1)) ^ <*(((p . i) * (cos r)) + ((p . j) * (- (sin r))))*>) ^ ((p /^ i) | ((j -' i) -' 1))) ^ <*(((p . i) * (sin r)) + ((p . j) * (cos r)))*>) ^ (p /^ j) )
assume that
A1:
1 <= i
and
A2:
i < j
and
A3:
j <= n
; (Mx2Tran (Rotation (i,j,n,r))) . p = ((((p | (i -' 1)) ^ <*(((p . i) * (cos r)) + ((p . j) * (- (sin r))))*>) ^ ((p /^ i) | ((j -' i) -' 1))) ^ <*(((p . i) * (sin r)) + ((p . j) * (cos r)))*>) ^ (p /^ j)
set M = Mx2Tran (Rotation (i,j,n,r));
set Mp = (Mx2Tran (Rotation (i,j,n,r))) . p;
set i1 = i -' 1;
set ji = j -' i;
A4:
i < n
by A2, A3, XXREAL_0:2;
A5:
( i -' 1 < (i -' 1) + 1 & i -' 1 = i - 1 )
by A1, NAT_1:13, XREAL_1:233;
A6:
now for k being Nat st 1 <= k & k <= i -' 1 holds
(((Mx2Tran (Rotation (i,j,n,r))) . p) | (i -' 1)) . k = (p | (i -' 1)) . klet k be
Nat;
( 1 <= k & k <= i -' 1 implies (((Mx2Tran (Rotation (i,j,n,r))) . p) | (i -' 1)) . k = (p | (i -' 1)) . k )assume that
1
<= k
and A7:
k <= i -' 1
;
(((Mx2Tran (Rotation (i,j,n,r))) . p) | (i -' 1)) . k = (p | (i -' 1)) . kA8:
(
(((Mx2Tran (Rotation (i,j,n,r))) . p) | (i -' 1)) . k = ((Mx2Tran (Rotation (i,j,n,r))) . p) . k &
(p | (i -' 1)) . k = p . k )
by A7, FINSEQ_3:112;
k < i
by A5, A7, XXREAL_0:2;
hence
(((Mx2Tran (Rotation (i,j,n,r))) . p) | (i -' 1)) . k = (p | (i -' 1)) . k
by A1, A2, A3, A8, Th20;
verum end;
A9:
len ((Mx2Tran (Rotation (i,j,n,r))) . p) = n
by CARD_1:def 7;
then A10:
len (((Mx2Tran (Rotation (i,j,n,r))) . p) | (i -' 1)) = i -' 1
by A5, A4, FINSEQ_1:59, XXREAL_0:2;
A11:
len p = n
by CARD_1:def 7;
then A12:
len (p /^ i) = n - i
by A4, RFINSEQ:def 1;
A13:
j -' i = j - i
by A2, XREAL_1:233;
then A14:
( (j -' i) -' 1 < ((j -' i) -' 1) + 1 & j -' i <= n - i )
by A3, NAT_1:13, XREAL_1:6;
j - i > i - i
by A2, XREAL_1:8;
then A15:
(j -' i) -' 1 = (j -' i) - 1
by A13, NAT_1:14, XREAL_1:233;
A16:
len (p /^ j) = n - j
by A3, A11, RFINSEQ:def 1;
A17:
len (((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) = n - i
by A9, A4, RFINSEQ:def 1;
then A18:
len ((((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) | ((j -' i) -' 1)) = (j -' i) -' 1
by A14, A15, FINSEQ_1:59, XXREAL_0:2;
A19:
(j -' i) -' 1 < n - i
by A14, A15, XXREAL_0:2;
A20:
now for k being Nat st 1 <= k & k <= (j -' i) -' 1 holds
((((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) | ((j -' i) -' 1)) . k = ((p /^ i) | ((j -' i) -' 1)) . klet k be
Nat;
( 1 <= k & k <= (j -' i) -' 1 implies ((((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) | ((j -' i) -' 1)) . k = ((p /^ i) | ((j -' i) -' 1)) . k )assume that A21:
1
<= k
and A22:
k <= (j -' i) -' 1
;
((((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) | ((j -' i) -' 1)) . k = ((p /^ i) | ((j -' i) -' 1)) . kA23:
((p /^ i) | ((j -' i) -' 1)) . k = (p /^ i) . k
by A22, FINSEQ_3:112;
A24:
k <= n - i
by A19, A22, XXREAL_0:2;
then
k in dom (((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i)
by A17, A21, FINSEQ_3:25;
then A25:
(((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) . k = ((Mx2Tran (Rotation (i,j,n,r))) . p) . (i + k)
by A9, A4, RFINSEQ:def 1;
k < ((j -' i) -' 1) + 1
by A22, NAT_1:13;
then A26:
i + k < i + (j -' i)
by A15, XREAL_1:8;
k in dom (p /^ i)
by A12, A21, A24, FINSEQ_3:25;
then A27:
(p /^ i) . k = p . (i + k)
by A11, A4, RFINSEQ:def 1;
(
k + i <> i &
((((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) | ((j -' i) -' 1)) . k = (((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) . k )
by A21, A22, FINSEQ_3:112, NAT_1:14;
hence
((((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) | ((j -' i) -' 1)) . k = ((p /^ i) | ((j -' i) -' 1)) . k
by A1, A2, A3, A13, A25, A26, A27, A23, Th20;
verum end;
len ((p /^ i) | ((j -' i) -' 1)) = (j -' i) -' 1
by A14, A15, A12, FINSEQ_1:59, XXREAL_0:2;
then A28:
(((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) | ((j -' i) -' 1) = (p /^ i) | ((j -' i) -' 1)
by A20, A18;
A29:
len (((Mx2Tran (Rotation (i,j,n,r))) . p) /^ j) = n - j
by A3, A9, RFINSEQ:def 1;
now for k being Nat st 1 <= k & k <= n - j holds
(((Mx2Tran (Rotation (i,j,n,r))) . p) /^ j) . k = (p /^ j) . klet k be
Nat;
( 1 <= k & k <= n - j implies (((Mx2Tran (Rotation (i,j,n,r))) . p) /^ j) . k = (p /^ j) . k )assume that A30:
1
<= k
and A31:
k <= n - j
;
(((Mx2Tran (Rotation (i,j,n,r))) . p) /^ j) . k = (p /^ j) . k
k in dom (((Mx2Tran (Rotation (i,j,n,r))) . p) /^ j)
by A29, A30, A31, FINSEQ_3:25;
then A32:
(((Mx2Tran (Rotation (i,j,n,r))) . p) /^ j) . k = ((Mx2Tran (Rotation (i,j,n,r))) . p) . (j + k)
by A3, A9, RFINSEQ:def 1;
k in dom (p /^ j)
by A16, A30, A31, FINSEQ_3:25;
then A33:
(p /^ j) . k = p . (j + k)
by A3, A11, RFINSEQ:def 1;
(
j + k >= j &
j + k <> j )
by A30, NAT_1:11, NAT_1:14;
hence
(((Mx2Tran (Rotation (i,j,n,r))) . p) /^ j) . k = (p /^ j) . k
by A1, A2, A3, A32, A33, Th20;
verum end;
then A34:
((Mx2Tran (Rotation (i,j,n,r))) . p) /^ j = p /^ j
by A16, A29;
len (p | (i -' 1)) = i -' 1
by A5, A11, A4, FINSEQ_1:59, XXREAL_0:2;
then A35:
((Mx2Tran (Rotation (i,j,n,r))) . p) | (i -' 1) = p | (i -' 1)
by A6, A10;
A36:
((Mx2Tran (Rotation (i,j,n,r))) . p) . i = ((p . i) * (cos r)) + ((p . j) * (- (sin r)))
by A1, A2, A3, Th21;
(Mx2Tran (Rotation (i,j,n,r))) . p = @ (@ ((Mx2Tran (Rotation (i,j,n,r))) . p))
;
then
(Mx2Tran (Rotation (i,j,n,r))) . p = ((((((Mx2Tran (Rotation (i,j,n,r))) . p) | (i -' 1)) ^ <*(((Mx2Tran (Rotation (i,j,n,r))) . p) . i)*>) ^ ((((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) | ((j -' i) -' 1))) ^ <*(((Mx2Tran (Rotation (i,j,n,r))) . p) . j)*>) ^ (((Mx2Tran (Rotation (i,j,n,r))) . p) /^ j)
by A1, A2, A3, A9, FINSEQ_7:1;
hence
(Mx2Tran (Rotation (i,j,n,r))) . p = ((((p | (i -' 1)) ^ <*(((p . i) * (cos r)) + ((p . j) * (- (sin r))))*>) ^ ((p /^ i) | ((j -' i) -' 1))) ^ <*(((p . i) * (sin r)) + ((p . j) * (cos r)))*>) ^ (p /^ j)
by A1, A2, A3, A34, A28, A35, A36, Th22; verum