let r be Real; :: thesis: for i, j, n being Nat st 1 <= i & i < j & j <= n holds
(Rotation (i,j,n,r)) @ = Rotation (i,j,n,(- r))
let i, j, n be Nat; :: thesis: ( 1 <= i & i < j & j <= n implies (Rotation (i,j,n,r)) @ = Rotation (i,j,n,(- r)) )
set O1 = Rotation (i,j,n,r);
set O2 = Rotation (i,j,n,(- r));
set S = Seg n;
assume A1: ( 1 <= i & i < j & j <= n ) ; :: thesis: (Rotation (i,j,n,r)) @ = Rotation (i,j,n,(- r))
A2: Indices (Rotation (i,j,n,(- r))) = [:(Seg n),(Seg n):] by MATRIX_0:24;
A3: Indices (Rotation (i,j,n,r)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
A4: Indices ((Rotation (i,j,n,r)) @) = [:(Seg n),(Seg n):] by MATRIX_0:24;
for k, m being Nat st [k,m] in [:(Seg n),(Seg n):] holds
((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)
proof
A5: cos r = cos (- r) by SIN_COS:31;
let k, m be Nat; :: thesis: ( [k,m] in [:(Seg n),(Seg n):] implies ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) )
A6: - (sin r) = sin (- r) by SIN_COS:31;
assume A7: [k,m] in [:(Seg n),(Seg n):] ; :: thesis: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)
then A8: [m,k] in [:(Seg n),(Seg n):] by A3, A4, MATRIX_0:def 6;
then A9: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,r)) * (m,k) by A3, MATRIX_0:def 6;
per cases ( ( k = m & k = i ) or ( k = m & k = j ) or ( k = m & k <> i & k <> j ) or ( k <> m & k = i & m = j ) or ( k <> m & k = i & m <> j ) or ( k <> m & k = j & m = i ) or ( k <> m & k = j & m <> i ) or ( k <> m & k <> j & k <> i ) or ( k <> m & m <> j & m <> i ) ) ;
suppose A10: ( k = m & k = i ) ; :: thesis: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)
then (Rotation (i,j,n,r)) * (m,k) = cos r by A1, Def3;
hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A5, A9, A10, Def3; :: thesis: verum
end;
suppose A11: ( k = m & k = j ) ; :: thesis: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)
then (Rotation (i,j,n,r)) * (m,k) = cos r by A1, Def3;
hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A5, A9, A11, Def3; :: thesis: verum
end;
suppose A12: ( k = m & k <> i & k <> j ) ; :: thesis: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)
then (Rotation (i,j,n,r)) * (m,k) = 1. F_Real by A1, A3, A7, Def3;
hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A2, A7, A9, A12, Def3; :: thesis: verum
end;
suppose A13: ( k <> m & k = i & m = j ) ; :: thesis: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)
then (Rotation (i,j,n,r)) * (m,k) = - (sin r) by A1, Def3;
hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A6, A9, A13, Def3; :: thesis: verum
end;
suppose A14: ( k <> m & k = i & m <> j ) ; :: thesis: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)
then not m in {i,j} by TARSKI:def 2;
then A15: {m,k} <> {i,j} by TARSKI:def 2;
then (Rotation (i,j,n,r)) * (m,k) = 0. F_Real by A1, A3, A8, A14, Def3;
hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A2, A7, A9, A14, A15, Def3; :: thesis: verum
end;
suppose A16: ( k <> m & k = j & m = i ) ; :: thesis: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)
then (Rotation (i,j,n,(- r))) * (k,m) = - (sin (- r)) by A1, Def3;
hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A6, A9, A16, Def3; :: thesis: verum
end;
suppose A17: ( k <> m & k = j & m <> i ) ; :: thesis: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)
then not m in {i,j} by TARSKI:def 2;
then A18: {m,k} <> {i,j} by TARSKI:def 2;
then (Rotation (i,j,n,r)) * (m,k) = 0. F_Real by A1, A3, A8, A17, Def3;
hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A2, A7, A9, A17, A18, Def3; :: thesis: verum
end;
suppose A19: ( k <> m & k <> j & k <> i ) ; :: thesis: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)
then not k in {i,j} by TARSKI:def 2;
then A20: {m,k} <> {i,j} by TARSKI:def 2;
then (Rotation (i,j,n,r)) * (m,k) = 0. F_Real by A1, A3, A8, A19, Def3;
hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A2, A7, A9, A19, A20, Def3; :: thesis: verum
end;
suppose A21: ( k <> m & m <> j & m <> i ) ; :: thesis: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)
then not m in {i,j} by TARSKI:def 2;
then A22: {m,k} <> {i,j} by TARSKI:def 2;
then (Rotation (i,j,n,r)) * (m,k) = 0. F_Real by A1, A3, A8, A21, Def3;
hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A2, A7, A9, A21, A22, Def3; :: thesis: verum
end;
end;
end;
hence (Rotation (i,j,n,r)) @ = Rotation (i,j,n,(- r)) by A4, MATRIX_0:27; :: thesis: verum