let r1, r2 be Real; for i, j, n being Nat st 1 <= i & i < j & j <= n holds
(Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2)) = Rotation (i,j,n,(r1 + r2))
let i, j, n be Nat; ( 1 <= i & i < j & j <= n implies (Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2)) = Rotation (i,j,n,(r1 + r2)) )
assume that
A1:
1 <= i
and
A2:
i < j
and
A3:
j <= n
; (Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2)) = Rotation (i,j,n,(r1 + r2))
set S = Seg n;
1 <= j
by A1, A2, XXREAL_0:2;
then A4:
j in Seg n
by A3;
set O1 = Rotation (i,j,n,r1);
set O2 = Rotation (i,j,n,r2);
set O = Rotation (i,j,n,(r1 + r2));
set O12 = (Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2));
A5:
width (Rotation (i,j,n,r1)) = n
by MATRIX_0:24;
i <= n
by A2, A3, XXREAL_0:2;
then A6:
i in Seg n
by A1;
A7:
Indices (Rotation (i,j,n,r1)) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
A8:
Indices ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
A9:
Indices (Rotation (i,j,n,(r1 + r2))) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
A10:
len (Rotation (i,j,n,r2)) = n
by MATRIX_0:25;
for k, m being Nat st [k,m] in Indices ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) holds
((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)
proof
let k,
m be
Nat;
( [k,m] in Indices ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) implies ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m) )
assume A11:
[k,m] in Indices ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2)))
;
((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)
then A12:
k in Seg n
by A8, ZFMISC_1:87;
A13:
((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (
k,
m)
= (Line ((Rotation (i,j,n,r1)),k)) "*" (Col ((Rotation (i,j,n,r2)),m))
by A5, A10, A11, MATRIX_3:def 4;
len (@ (Line ((Rotation (i,j,n,r1)),k))) = n
by A5, CARD_1:def 7;
then reconsider L =
@ (Line ((Rotation (i,j,n,r1)),k)) as
Element of
(TOP-REAL n) by TOPREAL3:46;
A14:
m in Seg n
by A8, A11, ZFMISC_1:87;
then A15:
L . m = (Rotation (i,j,n,r1)) * (
k,
m)
by A5, MATRIX_0:def 7;
A16:
@ L = Line (
(Rotation (i,j,n,r1)),
k)
;
A17:
L . i = (Rotation (i,j,n,r1)) * (
k,
i)
by A5, A6, MATRIX_0:def 7;
A18:
L . j = (Rotation (i,j,n,r1)) * (
k,
j)
by A4, A5, MATRIX_0:def 7;
per cases
( m = i or m = j or ( m <> i & m <> j ) )
;
suppose A19:
m = i
;
((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)then A20:
(Line ((Rotation (i,j,n,r1)),k)) "*" (Col ((Rotation (i,j,n,r2)),m)) = ((L . i) * (cos r2)) + ((L . j) * (- (sin r2)))
by A1, A2, A3, A16, Th15;
per cases
( k = i or k = j or ( k <> j & k <> i ) )
;
suppose A21:
k = i
;
((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)hence ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (
k,
m) =
((cos r1) * (cos r2)) + ((L . j) * (- (sin r2)))
by A1, A2, A3, A13, A17, A20, Def3
.=
((cos r1) * (cos r2)) + ((sin r1) * (- (sin r2)))
by A1, A2, A3, A18, A21, Def3
.=
((cos r1) * (cos r2)) - ((sin r1) * (sin r2))
.=
cos (r1 + r2)
by SIN_COS:75
.=
(Rotation (i,j,n,(r1 + r2))) * (
k,
m)
by A1, A2, A3, A19, A21, Def3
;
verum end; suppose A22:
k = j
;
((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)hence ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (
k,
m) =
((- (sin r1)) * (cos r2)) + ((L . j) * (- (sin r2)))
by A1, A2, A3, A13, A17, A20, Def3
.=
((- (sin r1)) * (cos r2)) + ((cos r1) * (- (sin r2)))
by A1, A2, A3, A18, A22, Def3
.=
- (((sin r1) * (cos r2)) + ((cos r1) * (sin r2)))
.=
- (sin (r1 + r2))
by SIN_COS:75
.=
(Rotation (i,j,n,(r1 + r2))) * (
k,
m)
by A1, A2, A3, A19, A22, Def3
;
verum end; suppose
(
k <> j &
k <> i )
;
((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)then
not
k in {i,j}
by TARSKI:def 2;
then A23:
(
{k,i} <> {i,j} &
{k,j} <> {i,j} )
by TARSKI:def 2;
A24:
[k,j] in [:(Seg n),(Seg n):]
by A4, A12, ZFMISC_1:87;
A25:
[k,i] in [:(Seg n),(Seg n):]
by A6, A12, ZFMISC_1:87;
then
(Rotation (i,j,n,r1)) * (
k,
i)
= 0. F_Real
by A1, A2, A3, A7, A23, Def3;
hence ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (
k,
m) =
(0 * (cos r2)) + (0 * (- (sin r2)))
by A1, A2, A3, A7, A13, A17, A18, A20, A23, A24, Def3
.=
(Rotation (i,j,n,(r1 + r2))) * (
k,
m)
by A1, A2, A3, A9, A19, A23, A25, Def3
;
verum end; end; end; suppose A26:
m = j
;
((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)then A27:
(Line ((Rotation (i,j,n,r1)),k)) "*" (Col ((Rotation (i,j,n,r2)),m)) = ((L . i) * (sin r2)) + ((L . j) * (cos r2))
by A1, A2, A3, A16, Th16;
per cases
( k = i or k = j or ( k <> j & k <> i ) )
;
suppose A28:
k = i
;
((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)hence ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (
k,
m) =
((cos r1) * (sin r2)) + ((L . j) * (cos r2))
by A1, A2, A3, A13, A17, A27, Def3
.=
((cos r1) * (sin r2)) + ((sin r1) * (cos r2))
by A1, A2, A3, A18, A28, Def3
.=
sin (r1 + r2)
by SIN_COS:75
.=
(Rotation (i,j,n,(r1 + r2))) * (
k,
m)
by A1, A2, A3, A26, A28, Def3
;
verum end; suppose A29:
k = j
;
((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)hence ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (
k,
m) =
((- (sin r1)) * (sin r2)) + ((L . j) * (cos r2))
by A1, A2, A3, A13, A17, A27, Def3
.=
((cos r1) * (cos r2)) - ((sin r1) * (sin r2))
by A1, A2, A3, A18, A29, Def3
.=
cos (r1 + r2)
by SIN_COS:75
.=
(Rotation (i,j,n,(r1 + r2))) * (
k,
m)
by A1, A2, A3, A26, A29, Def3
;
verum end; suppose
(
k <> j &
k <> i )
;
((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)then
not
k in {i,j}
by TARSKI:def 2;
then A30:
(
{k,i} <> {i,j} &
{k,j} <> {i,j} )
by TARSKI:def 2;
A31:
[k,j] in [:(Seg n),(Seg n):]
by A4, A12, ZFMISC_1:87;
[k,i] in [:(Seg n),(Seg n):]
by A6, A12, ZFMISC_1:87;
then
(Rotation (i,j,n,r1)) * (
k,
i)
= 0. F_Real
by A1, A2, A3, A7, A30, Def3;
hence ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (
k,
m) =
(0 * (sin r2)) + (0 * (cos r2))
by A1, A2, A3, A7, A13, A17, A18, A27, A30, A31, Def3
.=
(Rotation (i,j,n,(r1 + r2))) * (
k,
m)
by A1, A2, A3, A9, A26, A30, A31, Def3
;
verum end; end; end; suppose A32:
(
m <> i &
m <> j )
;
((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)then A33:
((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (
k,
m)
= L . m
by A1, A2, A3, A13, A14, A16, Th14;
A34:
[k,m] in [:(Seg n),(Seg n):]
by A11, MATRIX_0:24;
per cases
( k = m or k <> m )
;
suppose A35:
k = m
;
((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)then
(Rotation (i,j,n,r1)) * (
k,
m)
= 1. F_Real
by A1, A2, A3, A7, A8, A11, A32, Def3;
hence
((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (
k,
m)
= (Rotation (i,j,n,(r1 + r2))) * (
k,
m)
by A1, A2, A3, A9, A15, A32, A33, A34, A35, Def3;
verum end; suppose A36:
k <> m
;
((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)
not
m in {i,j}
by A32, TARSKI:def 2;
then A37:
{k,m} <> {i,j}
by TARSKI:def 2;
then
(Rotation (i,j,n,r1)) * (
k,
m)
= 0. F_Real
by A1, A2, A3, A7, A8, A11, A36, Def3;
hence
((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (
k,
m)
= (Rotation (i,j,n,(r1 + r2))) * (
k,
m)
by A1, A2, A3, A9, A15, A33, A34, A36, A37, Def3;
verum end; end; end; end;
end;
hence
(Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2)) = Rotation (i,j,n,(r1 + r2))
by MATRIX_0:27; verum