let n be Nat; :: thesis: 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); :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: 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) ; :: thesis: contradiction
n <> 0

proof

A18: ( dom (h * (Mx2Tran (AutMt f))) = the carrier of (TOP-REAL n) & dom (id the carrier of (TOP-REAL n)) = the carrier of (TOP-REAL n) ) by FUNCT_2:52;
assume n = 0 ; :: thesis: contradiction
then A19: the carrier of (TOP-REAL n) = {(0. (TOP-REAL n))} by EUCLID:22, EUCLID:77;
rng (h * (Mx2Tran (AutMt f))) c= the carrier of (TOP-REAL n) by RELAT_1:def 19;
then ( rng (id the carrier of (TOP-REAL n)) = the carrier of (TOP-REAL n) & rng (h * (Mx2Tran (AutMt f))) = the carrier of (TOP-REAL n) ) by A19, ZFMISC_1:33;
hence contradiction by A17, A18, A19, FUNCT_1:7; :: thesis: verum

end;

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; :: thesis: 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; :: thesis: verum

end;

hence ( Det (AutMt f) = 1. F_Real iff f is base_rotation ) by A3, Lm10; :: thesis: verum