let n be 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 )
let f be additive homogeneous Function of (TOP-REAL n),(TOP-REAL n); ( f is rotation implies ( Det (AutMt f) = 1. F_Real iff f is base_rotation ) )
set TR = TOP-REAL n;
set cTR = the carrier of (TOP-REAL n);
set M = AutMt f;
set MM = Mx2Tran (AutMt f);
A1:
( len (AutMt f) = n & width (AutMt f) = n )
by MATRIX_0:24;
A2:
( n = 0 implies n = 0 )
;
A3:
Mx2Tran (AutMt f) = f
by Def6;
assume A4:
f is rotation
; ( Det (AutMt f) = 1. F_Real iff f is base_rotation )
then consider h being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) such that
A5:
h is base_rotation
and
A6:
h * (Mx2Tran (AutMt f)) is {n} -support-yielding
by A3, Th36;
set R = AutMt h;
A7:
width (AutMt h) = n
by MATRIX_0:24;
A8:
h = Mx2Tran (AutMt h)
by Def6;
A9:
( AutMt (h * (Mx2Tran (AutMt f))) = 1. (F_Real,n) or AutMt (h * (Mx2Tran (AutMt f))) = AxialSymmetry (n,n) )
by A4, A3, A5, A6, Th35;
( Det (AutMt f) = 1. F_Real implies Mx2Tran (AutMt f) is base_rotation )
proof
assume A10:
Det (AutMt f) = 1. F_Real
;
Mx2Tran (AutMt f) is base_rotation
(
Det (AutMt h) = 1. F_Real &
n in NAT )
by A5, A8, Lm10, ORDINAL1:def 12;
then A11:
Det ((AutMt f) * (AutMt h)) =
(1. F_Real) * (1. F_Real)
by A10, MATRIXR2:45
.=
1
* (1. F_Real)
.=
1. F_Real
.=
1
;
A12:
rng (Mx2Tran (AutMt f)) c= the
carrier of
(TOP-REAL n)
by RELAT_1:def 19;
A13:
rng h = [#] (TOP-REAL n)
by A5, TOPS_2:def 5;
A14:
(
dom h = [#] (TOP-REAL n) &
h is
one-to-one )
by A5, TOPS_2:def 5;
A15:
dom (h ") = [#] (TOP-REAL n)
by A5, TOPS_2:def 5;
A16:
id (TOP-REAL n) = Mx2Tran (1. (F_Real,n))
by MATRTOP1:33;
h * (Mx2Tran (AutMt f)) = id the
carrier of
(TOP-REAL n)
proof
assume A17:
h * (Mx2Tran (AutMt f)) <> id the
carrier of
(TOP-REAL n)
;
contradiction
n <> 0
then A20:
n in Seg n
by FINSEQ_1:3;
Mx2Tran (AutMt (h * (Mx2Tran (AutMt f)))) = h * (Mx2Tran (AutMt f))
by Def6;
then
Mx2Tran (AxialSymmetry (n,n)) = Mx2Tran ((AutMt f) * (AutMt h))
by A1, A2, A9, A8, A7, A16, A17, MATRTOP1:32;
then
AxialSymmetry (
n,
n)
= (AutMt f) * (AutMt h)
by MATRTOP1:34;
then
Det (AxialSymmetry (n,n)) = Det ((AutMt f) * (AutMt h))
;
hence
contradiction
by A11, A20, Th4;
verum
end;
then
(h ") * (h * (Mx2Tran (AutMt f))) = h "
by A15, RELAT_1:52;
then h " =
((h ") * h) * (Mx2Tran (AutMt f))
by RELAT_1:36
.=
(id the carrier of (TOP-REAL n)) * (Mx2Tran (AutMt f))
by A14, A13, TOPS_2:52
.=
Mx2Tran (AutMt f)
by A12, RELAT_1:53
;
hence
Mx2Tran (AutMt f) is
base_rotation
by A5;
verum
end;
hence
( Det (AutMt f) = 1. F_Real iff f is base_rotation )
by A3, Lm10; verum