:: by Karol P\kak

::

:: Received May 30, 2011

:: Copyright (c) 2011-2021 Association of Mizar Users

theorem Th1: :: MATRTOP3:1

for n being Nat

for K being Field

for M being Matrix of n,K

for P being Permutation of (Seg n) holds

( Det ((((M * P) @) * P) @) = Det M & ( for i, j being Nat st [i,j] in Indices M holds

((((M * P) @) * P) @) * (i,j) = M * ((P . i),(P . j)) ) )

for K being Field

for M being Matrix of n,K

for P being Permutation of (Seg n) holds

( Det ((((M * P) @) * P) @) = Det M & ( for i, j being Nat st [i,j] in Indices M holds

((((M * P) @) * P) @) * (i,j) = M * ((P . i),(P . j)) ) )

proof end;

theorem Th3: :: MATRTOP3:3

for r being Real

for f being real-valued FinSequence

for i being Nat st i in dom f holds

Sum (sqr (f +* (i,r))) = ((Sum (sqr f)) - ((f . i) ^2)) + (r ^2)

for f being real-valued FinSequence

for i being Nat st i in dom f holds

Sum (sqr (f +* (i,r))) = ((Sum (sqr f)) - ((f . i) ^2)) + (r ^2)

proof end;

:: deftheorem Def1 defines -support-yielding MATRTOP3:def 1 :

for X being set

for F being Function-yielding Function holds

( F is X -support-yielding iff for f being Function

for x being set st f in dom F & (F . f) . x <> f . x holds

x in X );

for X being set

for F being Function-yielding Function holds

( F is X -support-yielding iff for f being Function

for x being set st f in dom F & (F . f) . x <> f . x holds

x in X );

registration

let X be set ;

existence

ex b_{1} being Function-yielding Function st b_{1} is X -support-yielding

end;
existence

ex b

proof end;

registration

let X be set ;

let Y be Subset of X;

for b_{1} being Function-yielding Function st b_{1} is Y -support-yielding holds

b_{1} is X -support-yielding

end;
let Y be Subset of X;

cluster Relation-like Function-like Function-yielding Y -support-yielding -> Function-yielding X -support-yielding for set ;

coherence for b

b

proof end;

registration

let X, Y be set ;

for b_{1} being Function-yielding Function st b_{1} is X -support-yielding & b_{1} is Y -support-yielding holds

b_{1} is X /\ Y -support-yielding

let g be Function-yielding Y -support-yielding Function;

coherence

f * g is X \/ Y -support-yielding

end;
cluster Relation-like Function-like Function-yielding X -support-yielding Y -support-yielding -> Function-yielding X /\ Y -support-yielding for set ;

coherence for b

b

proof end;

let f be Function-yielding X -support-yielding Function;let g be Function-yielding Y -support-yielding Function;

coherence

f * g is X \/ Y -support-yielding

proof end;

registration

let n be Nat;

ex b_{1} being Function of (TOP-REAL n),(TOP-REAL n) st b_{1} is homogeneous

end;
cluster Relation-like the carrier of (TOP-REAL n) -defined the carrier of (TOP-REAL n) -valued non empty Function-like total quasi_total homogeneous for Element of bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):];

existence ex b

proof end;

registration

let n, m be Nat;

for b_{1} being Function of (TOP-REAL n),(TOP-REAL m) holds b_{1} is FinSequence-yielding

end;
cluster Function-like quasi_total -> FinSequence-yielding for Element of bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL m):];

coherence for b

proof end;

registration
end;

registration
end;

registration

let n be Nat;

let f, g be homogeneous Function of (TOP-REAL n),(TOP-REAL n);

coherence

for b_{1} being Function of (TOP-REAL n),(TOP-REAL n) st b_{1} = f * g holds

b_{1} is homogeneous

end;
let f, g be homogeneous Function of (TOP-REAL n),(TOP-REAL n);

coherence

for b

b

proof end;

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 ) ) ) )

proof end;

definition

let n, i be Nat;

assume A1: i in Seg n ;

ex b_{1} being invertible Matrix of n,F_Real st

( b_{1} * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices b_{1} holds

( ( k = m & k <> i implies b_{1} * (k,k) = 1. F_Real ) & ( k <> m implies b_{1} * (k,m) = 0. F_Real ) ) ) )

for b_{1}, b_{2} being invertible Matrix of n,F_Real st b_{1} * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices b_{1} holds

( ( k = m & k <> i implies b_{1} * (k,k) = 1. F_Real ) & ( k <> m implies b_{1} * (k,m) = 0. F_Real ) ) ) & b_{2} * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices b_{2} holds

( ( k = m & k <> i implies b_{2} * (k,k) = 1. F_Real ) & ( k <> m implies b_{2} * (k,m) = 0. F_Real ) ) ) holds

b_{1} = b_{2}

end;
assume A1: i in Seg n ;

func AxialSymmetry (i,n) -> invertible Matrix of n,F_Real means :Def2: :: MATRTOP3:def 2

( it * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices it holds

( ( k = m & k <> i implies it * (k,k) = 1. F_Real ) & ( k <> m implies it * (k,m) = 0. F_Real ) ) ) );

existence ( it * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices it holds

( ( k = m & k <> i implies it * (k,k) = 1. F_Real ) & ( k <> m implies it * (k,m) = 0. F_Real ) ) ) );

ex b

( b

( ( k = m & k <> i implies b

proof end;

uniqueness for b

( ( k = m & k <> i implies b

( ( k = m & k <> i implies b

b

proof end;

:: deftheorem Def2 defines AxialSymmetry MATRTOP3:def 2 :

for n, i being Nat st i in Seg n holds

for b_{3} being invertible Matrix of n,F_Real holds

( b_{3} = AxialSymmetry (i,n) iff ( b_{3} * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices b_{3} holds

( ( k = m & k <> i implies b_{3} * (k,k) = 1. F_Real ) & ( k <> m implies b_{3} * (k,m) = 0. F_Real ) ) ) ) );

for n, i being Nat st i in Seg n holds

for b

( b

( ( k = m & k <> i implies b

theorem Th5: :: MATRTOP3:5

for i, j, n being Nat

for p being Point of (TOP-REAL n) st i in Seg n & j in Seg n & i <> j holds

(@ p) "*" (Col ((AxialSymmetry (i,n)),j)) = p . j

for p being Point of (TOP-REAL n) st i in Seg n & j in Seg n & i <> j holds

(@ p) "*" (Col ((AxialSymmetry (i,n)),j)) = p . j

proof end;

theorem Th6: :: MATRTOP3:6

for i, n being Nat

for p being Point of (TOP-REAL n) st i in Seg n holds

(@ p) "*" (Col ((AxialSymmetry (i,n)),i)) = - (p . i)

for p being Point of (TOP-REAL n) st i in Seg n holds

(@ p) "*" (Col ((AxialSymmetry (i,n)),i)) = - (p . i)

proof end;

theorem Th7: :: MATRTOP3:7

for i, n being Nat st i in Seg n holds

( AxialSymmetry (i,n) is V254( F_Real ) & (AxialSymmetry (i,n)) ~ = AxialSymmetry (i,n) )

( AxialSymmetry (i,n) is V254( F_Real ) & (AxialSymmetry (i,n)) ~ = AxialSymmetry (i,n) )

proof end;

theorem Th8: :: MATRTOP3:8

for i, j, n being Nat

for p being Point of (TOP-REAL n) st i in Seg n & i <> j holds

((Mx2Tran (AxialSymmetry (i,n))) . p) . j = p . j

for p being Point of (TOP-REAL n) st i in Seg n & i <> j holds

((Mx2Tran (AxialSymmetry (i,n))) . p) . j = p . j

proof end;

theorem Th9: :: MATRTOP3:9

for i, n being Nat

for p being Point of (TOP-REAL n) st i in Seg n holds

((Mx2Tran (AxialSymmetry (i,n))) . p) . i = - (p . i)

for p being Point of (TOP-REAL n) st i in Seg n holds

((Mx2Tran (AxialSymmetry (i,n))) . p) . i = - (p . i)

proof end;

theorem Th10: :: MATRTOP3:10

for i, n being Nat

for p being Point of (TOP-REAL n) st i in Seg n holds

(Mx2Tran (AxialSymmetry (i,n))) . p = p +* (i,(- (p . i)))

for p being Point of (TOP-REAL n) st i in Seg n holds

(Mx2Tran (AxialSymmetry (i,n))) . p = p +* (i,(- (p . i)))

proof end;

theorem Th12: :: MATRTOP3:12

for r being Real

for n being Nat

for a, b being Element of F_Real st a = cos r & b = sin r holds

Det (block_diagonal (<*((a,b) ][ ((- b),a)),(1. (F_Real,n))*>,(0. F_Real))) = 1. F_Real

for n being Nat

for a, b being Element of F_Real st a = cos r & b = sin r holds

Det (block_diagonal (<*((a,b) ][ ((- b),a)),(1. (F_Real,n))*>,(0. F_Real))) = 1. F_Real

proof 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 ) ) ) )

proof end;

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 ) ) ) )

proof end;

definition

let n be Nat;

let r be Real;

let i, j be Nat;

assume A1: ( 1 <= i & i < j & j <= n ) ;

ex b_{1} being invertible Matrix of n,F_Real st

( b_{1} * (i,i) = cos r & b_{1} * (j,j) = cos r & b_{1} * (i,j) = sin r & b_{1} * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices b_{1} holds

( ( k = m & k <> i & k <> j implies b_{1} * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies b_{1} * (k,m) = 0. F_Real ) ) ) )

for b_{1}, b_{2} being invertible Matrix of n,F_Real st b_{1} * (i,i) = cos r & b_{1} * (j,j) = cos r & b_{1} * (i,j) = sin r & b_{1} * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices b_{1} holds

( ( k = m & k <> i & k <> j implies b_{1} * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies b_{1} * (k,m) = 0. F_Real ) ) ) & b_{2} * (i,i) = cos r & b_{2} * (j,j) = cos r & b_{2} * (i,j) = sin r & b_{2} * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices b_{2} holds

( ( k = m & k <> i & k <> j implies b_{2} * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies b_{2} * (k,m) = 0. F_Real ) ) ) holds

b_{1} = b_{2}

end;
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: :: MATRTOP3:def 3

( 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 ( 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 ) ) ) );

ex b

( b

( ( k = m & k <> i & k <> j implies b

proof end;

uniqueness for b

( ( k = m & k <> i & k <> j implies b

( ( k = m & k <> i & k <> j implies b

b

proof 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 b_{5} being invertible Matrix of n,F_Real holds

( b_{5} = Rotation (i,j,n,r) iff ( b_{5} * (i,i) = cos r & b_{5} * (j,j) = cos r & b_{5} * (i,j) = sin r & b_{5} * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices b_{5} holds

( ( k = m & k <> i & k <> j implies b_{5} * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies b_{5} * (k,m) = 0. F_Real ) ) ) ) );

for n being Nat

for r being Real

for i, j being Nat st 1 <= i & i < j & j <= n holds

for b

( b

( ( k = m & k <> i & k <> j implies b

theorem Th13: :: MATRTOP3:13

for r being Real

for i, j, n being Nat st 1 <= i & i < j & j <= n holds

Det (Rotation (i,j,n,r)) = 1. F_Real

for i, j, n being Nat st 1 <= i & i < j & j <= n holds

Det (Rotation (i,j,n,r)) = 1. F_Real

proof end;

theorem Th14: :: MATRTOP3:14

for r being Real

for i, j, k, n being Nat

for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & k in Seg n & k <> i & k <> j holds

(@ p) "*" (Col ((Rotation (i,j,n,r)),k)) = p . k

for i, j, k, n being Nat

for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & k in Seg n & k <> i & k <> j holds

(@ p) "*" (Col ((Rotation (i,j,n,r)),k)) = p . k

proof end;

theorem Th15: :: MATRTOP3:15

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

(@ p) "*" (Col ((Rotation (i,j,n,r)),i)) = ((p . i) * (cos r)) + ((p . j) * (- (sin r)))

for i, j, n being Nat

for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n holds

(@ p) "*" (Col ((Rotation (i,j,n,r)),i)) = ((p . i) * (cos r)) + ((p . j) * (- (sin r)))

proof end;

theorem Th16: :: MATRTOP3:16

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

(@ p) "*" (Col ((Rotation (i,j,n,r)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos r))

for i, j, n being Nat

for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n holds

(@ p) "*" (Col ((Rotation (i,j,n,r)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos r))

proof end;

theorem Th17: :: MATRTOP3:17

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))

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))

proof end;

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))

proof end;

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))

proof end;

theorem Th19: :: MATRTOP3:19

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)) )

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)) )

proof end;

theorem Th20: :: MATRTOP3:20

for r being Real

for i, j, k, n being Nat

for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & k <> i & k <> j holds

((Mx2Tran (Rotation (i,j,n,r))) . p) . k = p . k

for i, j, k, n being Nat

for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & k <> i & k <> j holds

((Mx2Tran (Rotation (i,j,n,r))) . p) . k = p . k

proof end;

theorem Th21: :: MATRTOP3:21

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 = ((p . i) * (cos r)) + ((p . j) * (- (sin r)))

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 = ((p . i) * (cos r)) + ((p . j) * (- (sin r)))

proof end;

theorem Th22: :: MATRTOP3:22

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) . j = ((p . i) * (sin r)) + ((p . j) * (cos r))

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) . j = ((p . i) * (sin r)) + ((p . j) * (cos r))

proof end;

theorem Th23: :: MATRTOP3:23

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 = ((((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)

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)

proof end;

theorem Th24: :: MATRTOP3:24

for s being Real

for i, j, n being Nat

for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & s ^2 <= ((p . i) ^2) + ((p . j) ^2) holds

ex r being Real st ((Mx2Tran (Rotation (i,j,n,r))) . p) . i = s

for i, j, n being Nat

for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & s ^2 <= ((p . i) ^2) + ((p . j) ^2) holds

ex r being Real st ((Mx2Tran (Rotation (i,j,n,r))) . p) . i = s

proof end;

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))

proof end;

theorem Th25: :: MATRTOP3:25

for s being Real

for i, j, n being Nat

for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & s ^2 <= ((p . i) ^2) + ((p . j) ^2) holds

ex r being Real st ((Mx2Tran (Rotation (i,j,n,r))) . p) . j = s

for i, j, n being Nat

for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & s ^2 <= ((p . i) ^2) + ((p . j) ^2) holds

ex r being Real st ((Mx2Tran (Rotation (i,j,n,r))) . p) . j = s

proof end;

theorem Th26: :: MATRTOP3:26

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 {i,j} -support-yielding

for i, j, n being Nat st 1 <= i & i < j & j <= n holds

Mx2Tran (Rotation (i,j,n,r)) is {i,j} -support-yielding

proof end;

:: deftheorem Def4 defines rotation MATRTOP3:def 4 :

for n being Nat

for f being Function of (TOP-REAL n),(TOP-REAL n) holds

( f is rotation iff for p being Point of (TOP-REAL n) holds |.p.| = |.(f . p).| );

for n being Nat

for f being Function of (TOP-REAL n),(TOP-REAL n) holds

( f is rotation iff for p being Point of (TOP-REAL n) holds |.p.| = |.(f . p).| );

:: deftheorem Def5 defines base_rotation MATRTOP3:def 5 :

for n being Nat

for f being Function of (TOP-REAL n),(TOP-REAL n) holds

( f is base_rotation iff ex F being FinSequence of (GFuncs the carrier of (TOP-REAL n)) st

( f = Product F & ( for k being Nat st k in dom F holds

ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) ) ) ) );

for n being Nat

for f being Function of (TOP-REAL n),(TOP-REAL n) holds

( f is base_rotation iff ex F being FinSequence of (GFuncs the carrier of (TOP-REAL n)) st

( f = Product F & ( for k being Nat st k in dom F holds

ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) ) ) ) );

registration

let n be Nat;

ex b_{1} being Function of (TOP-REAL n),(TOP-REAL n) st b_{1} is base_rotation

end;
cluster Relation-like the carrier of (TOP-REAL n) -defined the carrier of (TOP-REAL n) -valued non empty Function-like total quasi_total Function-yielding V196() FinSequence-yielding base_rotation for Element of bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):];

existence ex b

proof end;

registration

let n be Nat;

let f, g be base_rotation Function of (TOP-REAL n),(TOP-REAL n);

coherence

for b_{1} being Function of (TOP-REAL n),(TOP-REAL n) st b_{1} = f * g holds

b_{1} is base_rotation

end;
let f, g be base_rotation Function of (TOP-REAL n),(TOP-REAL n);

coherence

for b

b

proof end;

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

proof end;

theorem Th28: :: MATRTOP3:28

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 base_rotation

for i, j, n being Nat st 1 <= i & i < j & j <= n holds

Mx2Tran (Rotation (i,j,n,r)) is base_rotation

proof end;

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

proof end;

registration

let n be Nat;

for b_{1} being Function of (TOP-REAL n),(TOP-REAL n) st b_{1} is base_rotation holds

( b_{1} is homogeneous & b_{1} is additive & b_{1} is rotation & b_{1} is being_homeomorphism )

end;
cluster Function-like quasi_total base_rotation -> additive homogeneous being_homeomorphism rotation for Element of bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):];

coherence for b

( b

proof end;

registration

let n be Nat;

let f be base_rotation Function of (TOP-REAL n),(TOP-REAL n);

coherence

f " is base_rotation

end;
let f be base_rotation Function of (TOP-REAL n),(TOP-REAL n);

coherence

f " is base_rotation

proof end;

registration

let n be Nat;

let f, g be rotation Function of (TOP-REAL n),(TOP-REAL n);

coherence

for b_{1} being Function of (TOP-REAL n),(TOP-REAL n) st b_{1} = f * g holds

b_{1} is rotation
by Lm8;

end;
let f, g be rotation Function of (TOP-REAL n),(TOP-REAL n);

coherence

for b

b

definition

let n be Nat;

let f be additive homogeneous Function of (TOP-REAL n),(TOP-REAL n);

existence

ex b_{1} being Matrix of n,F_Real st f = Mx2Tran b_{1}

for b_{1}, b_{2} being Matrix of n,F_Real st f = Mx2Tran b_{1} & f = Mx2Tran b_{2} holds

b_{1} = b_{2}
by MATRTOP1:34;

end;
let f be additive homogeneous Function of (TOP-REAL n),(TOP-REAL n);

existence

ex b

proof end;

uniqueness for b

b

:: deftheorem Def6 defines AutMt MATRTOP3:def 6 :

for n being Nat

for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n)

for b_{3} being Matrix of n,F_Real holds

( b_{3} = AutMt f iff f = Mx2Tran b_{3} );

for n being Nat

for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n)

for b

( b

theorem Th29: :: MATRTOP3:29

for n being Nat

for f1, f2 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) holds AutMt (f1 * f2) = (AutMt f2) * (AutMt f1)

for f1, f2 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) holds AutMt (f1 * f2) = (AutMt f2) * (AutMt f1)

proof end;

theorem Th30: :: MATRTOP3:30

for X being set

for k, n being Nat

for p being Point of (TOP-REAL n) st k in X & k in Seg n holds

ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st

( f is X -support-yielding & f is base_rotation & ( card (X /\ (Seg n)) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg n) & i <> k holds

(f . p) . i = 0 ) )

for k, n being Nat

for p being Point of (TOP-REAL n) st k in X & k in Seg n holds

ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st

( f is X -support-yielding & f is base_rotation & ( card (X /\ (Seg n)) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg n) & i <> k holds

(f . p) . i = 0 ) )

proof end;

theorem Th31: :: MATRTOP3:31

for n being Nat

for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n)

for A being Subset of (TOP-REAL n) st f | A = id A holds

f | (Lin A) = id (Lin A)

for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n)

for A being Subset of (TOP-REAL n) st f | A = id A holds

f | (Lin A) = id (Lin A)

proof end;

theorem Th32: :: MATRTOP3:32

for n being Nat

for p being Point of (TOP-REAL n)

for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n)

for A being Subset of (TOP-REAL n) st f is rotation & f | A = id A holds

for i being Nat st i in Seg n & Base_FinSeq (n,i) in Lin A holds

(f . p) . i = p . i

for p being Point of (TOP-REAL n)

for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n)

for A being Subset of (TOP-REAL n) st f is rotation & f | A = id A holds

for i being Nat st i in Seg n & Base_FinSeq (n,i) in Lin A holds

(f . p) . i = p . i

proof end;

theorem Th33: :: MATRTOP3:33

for X being set

for n being Nat

for p being Point of (TOP-REAL n)

for f being rotation Function of (TOP-REAL n),(TOP-REAL n) st f is X -support-yielding & ( for i being Nat st i in X /\ (Seg n) holds

p . i = 0 ) holds

f . p = p

for n being Nat

for p being Point of (TOP-REAL n)

for f being rotation Function of (TOP-REAL n),(TOP-REAL n) st f is X -support-yielding & ( for i being Nat st i in X /\ (Seg n) holds

p . i = 0 ) holds

f . p = p

proof end;

theorem Th34: :: MATRTOP3:34

for i, n being Nat

for p being Point of (TOP-REAL n) st i in Seg n & n >= 2 holds

ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st

( f is base_rotation & f . p = p +* (i,(- (p . i))) )

for p being Point of (TOP-REAL n) st i in Seg n & n >= 2 holds

ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st

( f is base_rotation & f . p = p +* (i,(- (p . i))) )

proof end;

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)

proof end;

theorem Th35: :: MATRTOP3:35

for i, n being Nat

for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st f is {i} -support-yielding & f is rotation & not AutMt f = AxialSymmetry (i,n) holds

AutMt f = 1. (F_Real,n)

for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st f is {i} -support-yielding & f is rotation & not AutMt f = AxialSymmetry (i,n) holds

AutMt f = 1. (F_Real,n)

proof end;

theorem Th36: :: MATRTOP3:36

for n being Nat

for f1 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st f1 is rotation holds

ex f2 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st

( f2 is base_rotation & f2 * f1 is {n} -support-yielding )

for f1 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st f1 is rotation holds

ex f2 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st

( f2 is base_rotation & f2 * f1 is {n} -support-yielding )

proof end;

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

proof end;

theorem Th37: :: MATRTOP3:37

for n being Nat

for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st f is rotation holds

( Det (AutMt f) = 1. F_Real iff f is base_rotation )

for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st f is rotation holds

( Det (AutMt f) = 1. F_Real iff f is base_rotation )

proof end;

theorem Th38: :: MATRTOP3:38

for n being Nat

for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) holds

( not f is rotation or Det (AutMt f) = 1. F_Real or Det (AutMt f) = - (1. F_Real) )

for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) holds

( not f is rotation or Det (AutMt f) = 1. F_Real or Det (AutMt f) = - (1. F_Real) )

proof end;

theorem Th39: :: MATRTOP3:39

for i, n being Nat

for f1, f2 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st f1 is rotation & Det (AutMt f1) = - (1. F_Real) & i in Seg n & AutMt f2 = AxialSymmetry (i,n) holds

f1 * f2 is base_rotation

for f1, f2 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st f1 is rotation & Det (AutMt f1) = - (1. F_Real) & i in Seg n & AutMt f2 = AxialSymmetry (i,n) holds

f1 * f2 is base_rotation

proof end;

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

proof end;

registration

let n be Nat;

let f be additive homogeneous rotation Function of (TOP-REAL n),(TOP-REAL n);

coherence

AutMt f is Orthogonal

end;
let f be additive homogeneous rotation Function of (TOP-REAL n),(TOP-REAL n);

coherence

AutMt f is Orthogonal

proof end;

registration

let n be Nat;

for b_{1} being Function of (TOP-REAL n),(TOP-REAL n) st b_{1} is homogeneous & b_{1} is additive & b_{1} is rotation holds

b_{1} is being_homeomorphism

end;
cluster Function-like quasi_total additive homogeneous rotation -> being_homeomorphism for Element of bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):];

coherence for b

b

proof end;

theorem :: MATRTOP3:40

for n being Nat

for p, q being Point of (TOP-REAL n) st n = 1 & |.p.| = |.q.| holds

ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st

( f is rotation & f . p = q & ( AutMt f = AxialSymmetry (n,n) or AutMt f = 1. (F_Real,n) ) )

for p, q being Point of (TOP-REAL n) st n = 1 & |.p.| = |.q.| holds

ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st

( f is rotation & f . p = q & ( AutMt f = AxialSymmetry (n,n) or AutMt f = 1. (F_Real,n) ) )

proof end;

theorem :: MATRTOP3:41

for n being Nat

for p, q being Point of (TOP-REAL n) st n <> 1 & |.p.| = |.q.| holds

ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st

( f is base_rotation & f . p = q )

for p, q being Point of (TOP-REAL n) st n <> 1 & |.p.| = |.q.| holds

ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st

( f is base_rotation & f . p = q )

proof end;