environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, PRE_TOPC, EUCLID, ARYTM_1, ARYTM_3, SUPINF_2, XBOOLE_0, RELAT_1, CARD_1, VALUED_0, FINSEQ_1, COMPLEX1, SQUARE_1, CARD_3, RVSUM_1, XXREAL_0, NAT_1, TARSKI, STRUCT_0, REAL_1, FUNCT_1, UNIALG_1, MSSUBFAM, FUNCOP_1, FINSEQ_2, ALGSTR_0, FUNCT_2, FVSUM_1, INCSP_1, MATRIX_1, MATRIX_3, MATRIX13, MATRLIN, MATRLIN2, MESFUNC1, ORDINAL4, PARTFUN1, PRVECT_1, QC_LANG1, RLVECT_2, RLVECT_3, TREES_1, VALUED_1, VECTSP_1, MATRIXJ1, ZFMISC_1, BINOP_1, GROUP_1, ABIAN, XXREAL_1, SIN_COS, FINSOP_1, FUNCT_4, MATRIX_6, PRE_POLY, TOPS_2, RFINSEQ, MONOID_0, MATRIXR2, MATRTOP3;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, NAT_D, FUNCOP_1, FINSEQ_1, PRE_POLY, RFINSEQ, FINSEQ_2, RVSUM_1, VALUED_0, SQUARE_1, STRUCT_0, PRE_TOPC, TOPS_2, RLVECT_1, EUCLID, TOPREAL9, CARD_1, VECTSP_1, MATRIX_0, MATRIX_1, MATRIX_3, MATRIX_6, GROUP_1, MATRIX11, MATRTOP1, SIN_COS, ALGSTR_0, MATRIX_7, BINOP_1, FVSUM_1, RCOMP_1, MONOID_0, GROUP_4, PRVECT_1, RLVECT_2, RLVECT_3, FUNCT_7, MATRIX13, MATRIXR2, FINSOP_1, MATRLIN, MATRLIN2, MOD_2, MATRIXJ1, TMAP_1;
definitions TARSKI, TOPREAL9, VECTSP_1;
theorems XREAL_0, TARSKI, FUNCT_2, EUCLID, XBOOLE_1, XBOOLE_0, SQUARE_1, XCMPLX_1, ABSVALUE, RVSUM_1, EUCLID_2, ENUMSET1, XREAL_1, XXREAL_0, RLVECT_1, ORDINAL1, VECTSP_1, CARD_1, CARD_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FUNCT_1, FVSUM_1, LAPLACE, MATRIX_0, MATRIX_1, MATRIX_6, MATRIX13, MATRIXR1, MATRLIN2, MATRTOP1, NAT_1, PARTFUN1, PRE_POLY, RELAT_1, RLSUB_1, RLVECT_2, RLVECT_3, ZFMISC_1, MATRIXJ1, STIRL2_1, TOPS_2, TOPREAL9, MATRIX_9, SIN_COS, MATRIX_7, MATRIXR2, MATRIX11, MATRIX_3, MATRIX15, RFINSEQ, FINSEQ_7, SIN_COS6, XXREAL_1, GROUP_4, MONOID_0, GROUP_1, FINSEQ_5, TMAP_1, RLVECT_4, FUNCT_7, TOPREALC, VALUED_1, INT_1, FINSOP_1, MOD_2, TOPREAL3;
schemes NAT_1, FINSEQ_4, MATRIX_0;
registrations XBOOLE_0, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, MEMBERED, STRUCT_0, MONOID_0, EUCLID, VALUED_0, FINSEQ_1, FUNCT_1, RELAT_1, TOPREAL9, CARD_1, FINSEQ_2, FINSET_1, FUNCT_2, MATRIX13, MATRIX_1, MATRTOP1, NUMBERS, PRVECT_1, RELSET_1, RLVECT_2, VECTSP_1, XCMPLX_0, SIN_COS, MATRIX11, MATRIXJ1, GRCAT_1, BORSUK_3, FUNCOP_1, MATRIX_0, INT_1, FUNCT_7, PRE_POLY, SUBSET_1, MATRIX_6, RVSUM_1, ORDINAL1, POLYNOM8;
constructors HIDDEN, REAL_1, SQUARE_1, BORSUK_1, MONOID_0, CONVEX1, TOPREAL9, BINARITH, FVSUM_1, LAPLACE, MATRIX_6, MATRIX11, TOPS_2, MATRIX13, MATRLIN2, MATRTOP1, REALSET1, RLVECT_3, MATRIXJ1, RCOMP_1, ABIAN, SIN_COS, MATRIX_7, SETWISEO, GROUP_4, TMAP_1, FINSOP_1, MATRIXR2, MATRIX_0, BINOP_2, VECTSP_2;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities SQUARE_1, EUCLID, XCMPLX_0, ALGSTR_0, STRUCT_0, FINSEQ_1, MATRTOP1, VECTSP_1, FVSUM_1;
expansions TARSKI, STRUCT_0, TOPREAL9, FINSEQ_1, VECTSP_1;
Lm1:
for i, n being Nat st i in Seg n holds
ex M being Matrix of n,F_Real st
( Det M = - (1. F_Real) & M * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices M holds
( ( k = m & k <> i implies M * (k,k) = 1. F_Real ) & ( k <> m implies M * (k,m) = 0. F_Real ) ) ) )
definition
let n,
i be
Nat;
assume A1:
i in Seg n
;
existence
ex b1 being invertible Matrix of n,F_Real st
( b1 * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices b1 holds
( ( k = m & k <> i implies b1 * (k,k) = 1. F_Real ) & ( k <> m implies b1 * (k,m) = 0. F_Real ) ) ) )
uniqueness
for b1, b2 being invertible Matrix of n,F_Real st b1 * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices b1 holds
( ( k = m & k <> i implies b1 * (k,k) = 1. F_Real ) & ( k <> m implies b1 * (k,m) = 0. F_Real ) ) ) & b2 * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices b2 holds
( ( k = m & k <> i implies b2 * (k,k) = 1. F_Real ) & ( k <> m implies b2 * (k,m) = 0. F_Real ) ) ) holds
b1 = b2
end;
Lm2:
for i, j, n being Nat st 1 <= i & i < j & j <= n holds
ex P being Permutation of (Seg n) st
( P . 1 = i & P . 2 = j & ( for k being Nat st k in Seg n & k > 2 holds
( ( k <= i + 1 implies P . k = k - 2 ) & ( i + 1 < k & k <= j implies P . k = k - 1 ) & ( k > j implies P . k = k ) ) ) )
Lm3:
for r being Real
for i, j, n being Nat st 1 <= i & i < j & j <= n holds
ex A being Matrix of n,F_Real st
( Det A = 1. F_Real & A * (i,i) = cos r & A * (j,j) = cos r & A * (i,j) = sin r & A * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices A holds
( ( k = m & k <> i & k <> j implies A * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies A * (k,m) = 0. F_Real ) ) ) )
definition
let n be
Nat;
let r be
Real;
let i,
j be
Nat;
assume A1:
( 1
<= i &
i < j &
j <= n )
;
func Rotation (
i,
j,
n,
r)
-> invertible Matrix of
n,
F_Real means :
Def3:
(
it * (
i,
i)
= cos r &
it * (
j,
j)
= cos r &
it * (
i,
j)
= sin r &
it * (
j,
i)
= - (sin r) & ( for
k,
m being
Nat st
[k,m] in Indices it holds
( (
k = m &
k <> i &
k <> j implies
it * (
k,
k)
= 1. F_Real ) & (
k <> m &
{k,m} <> {i,j} implies
it * (
k,
m)
= 0. F_Real ) ) ) );
existence
ex b1 being invertible Matrix of n,F_Real st
( b1 * (i,i) = cos r & b1 * (j,j) = cos r & b1 * (i,j) = sin r & b1 * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices b1 holds
( ( k = m & k <> i & k <> j implies b1 * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies b1 * (k,m) = 0. F_Real ) ) ) )
uniqueness
for b1, b2 being invertible Matrix of n,F_Real st b1 * (i,i) = cos r & b1 * (j,j) = cos r & b1 * (i,j) = sin r & b1 * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices b1 holds
( ( k = m & k <> i & k <> j implies b1 * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies b1 * (k,m) = 0. F_Real ) ) ) & b2 * (i,i) = cos r & b2 * (j,j) = cos r & b2 * (i,j) = sin r & b2 * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices b2 holds
( ( k = m & k <> i & k <> j implies b2 * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies b2 * (k,m) = 0. F_Real ) ) ) holds
b1 = b2
end;
::
deftheorem Def3 defines
Rotation MATRTOP3:def 3 :
for n being Nat
for r being Real
for i, j being Nat st 1 <= i & i < j & j <= n holds
for b5 being invertible Matrix of n,F_Real holds
( b5 = Rotation (i,j,n,r) iff ( b5 * (i,i) = cos r & b5 * (j,j) = cos r & b5 * (i,j) = sin r & b5 * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices b5 holds
( ( k = m & k <> i & k <> j implies b5 * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies b5 * (k,m) = 0. F_Real ) ) ) ) );
theorem Th17:
for
r1,
r2 being
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))
Lm4:
for r being Real
for i, j, n being Nat st 1 <= i & i < j & j <= n holds
(Rotation (i,j,n,r)) @ = Rotation (i,j,n,(- r))
Lm5:
for r being Real
for i, j, n being Nat st 1 <= i & i < j & j <= n holds
(Rotation (i,j,n,r)) ~ = Rotation (i,j,n,(- r))
theorem Th19:
for
r being
Real for
i,
j,
n being
Nat st 1
<= i &
i < j &
j <= n holds
(
Rotation (
i,
j,
n,
r) is
Orthogonal &
(Rotation (i,j,n,r)) ~ = Rotation (
i,
j,
n,
(- r)) )
Lm6:
for r being 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) . i) * (((Mx2Tran (Rotation (i,j,n,r))) . p) . i)) + ((((Mx2Tran (Rotation (i,j,n,r))) . p) . j) * (((Mx2Tran (Rotation (i,j,n,r))) . p) . j)) = ((p . i) * (p . i)) + ((p . j) * (p . j))
Lm7:
for r being Real
for i, j, n being Nat st 1 <= i & i < j & j <= n holds
Mx2Tran (Rotation (i,j,n,r)) is rotation
Lm8:
for n being Nat
for f, g being Function of (TOP-REAL n),(TOP-REAL n) st f is rotation & g is rotation holds
f * g is rotation
Lm9:
for X being set
for i, n being Nat
for f being additive homogeneous rotation Function of (TOP-REAL n),(TOP-REAL n) st f is X -support-yielding & not i in X holds
f . (Base_FinSeq (n,i)) = Base_FinSeq (n,i)
Lm10:
for n being Nat
for M being Matrix of n,F_Real st Mx2Tran M is base_rotation holds
Det M = 1. F_Real
Lm11:
for n being Nat
for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st f is base_rotation holds
AutMt f is Orthogonal