set TR = TOP-REAL n;
set cTR = the carrier of (TOP-REAL n);
set M = AutMt f;
per cases ( Det (AutMt f) = 1. F_Real or ( Det (AutMt f) = - (1. F_Real) & not f is base_rotation ) ) by Th37, Th38;
suppose Det (AutMt f) = 1. F_Real ; :: thesis: AutMt f is Orthogonal
then f is base_rotation by Th37;
hence AutMt f is Orthogonal by Lm11; :: thesis: verum
end;
suppose A1: ( Det (AutMt f) = - (1. F_Real) & not f is base_rotation ) ; :: thesis: AutMt f is Orthogonal
A2: n > 0
proof
A3: ( dom 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 n = 0 ;
then A4: the carrier of (TOP-REAL n) = {(0. (TOP-REAL n))} by EUCLID:22, EUCLID:77;
rng 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 f = the carrier of (TOP-REAL n) ) by A4, ZFMISC_1:33;
then f = id (TOP-REAL n) by A3, A4, FUNCT_1:7;
hence contradiction by A1; :: thesis: verum
end;
then A5: n in Seg n by FINSEQ_1:3;
set A = AxialSymmetry (n,n);
set MA = Mx2Tran (AxialSymmetry (n,n));
AutMt (Mx2Tran (AxialSymmetry (n,n))) = AxialSymmetry (n,n) by Def6;
then A6: f * (Mx2Tran (AxialSymmetry (n,n))) is base_rotation by A1, A5, Th39;
( AxialSymmetry (n,n) is V254( F_Real ) & (AxialSymmetry (n,n)) ~ = AxialSymmetry (n,n) ) by A5, Th7;
then (AxialSymmetry (n,n)) @ = (AxialSymmetry (n,n)) ~ by Th2;
then A7: ( AxialSymmetry (n,n) is Orthogonal & AutMt (f * (Mx2Tran (AxialSymmetry (n,n)))) is Orthogonal ) by A6, Lm11, MATRIX_6:def 7;
A8: AutMt (f * (Mx2Tran (AxialSymmetry (n,n)))) = (AutMt (Mx2Tran (AxialSymmetry (n,n)))) * (AutMt f) by Th29
.= (AxialSymmetry (n,n)) * (AutMt f) by Def6 ;
(AxialSymmetry (n,n)) ~ is_reverse_of AxialSymmetry (n,n) by MATRIX_6:def 4;
then A9: ((AxialSymmetry (n,n)) ~) * (AxialSymmetry (n,n)) = 1. (F_Real,n) by MATRIX_6:def 2;
( width ((AxialSymmetry (n,n)) ~) = n & len (AxialSymmetry (n,n)) = n & width (AxialSymmetry (n,n)) = n & len (AutMt f) = n ) by MATRIX_0:24;
then ((AxialSymmetry (n,n)) ~) * ((AxialSymmetry (n,n)) * (AutMt f)) = (((AxialSymmetry (n,n)) ~) * (AxialSymmetry (n,n))) * (AutMt f) by MATRIX_3:33
.= AutMt f by A9, MATRIX_3:18 ;
hence AutMt f is Orthogonal by A2, A7, A8, MATRIX_6:59; :: thesis: verum
end;
end;