set TR = TOP-REAL n;
set cTR = the carrier of ();
set M = AutMt f;
per cases ( Det () = 1. F_Real or ( Det () = - () & not f is base_rotation ) ) by ;
suppose Det () = 1. F_Real ; :: thesis:
end;
suppose A1: ( Det () = - () & not f is base_rotation ) ; :: thesis:
A2: n > 0
proof
A3: ( dom f = the carrier of () & dom (id the carrier of ()) = the carrier of () ) by FUNCT_2:52;
assume n <= 0 ; :: thesis: contradiction
then n = 0 ;
then A4: the carrier of () = {(0. ())} by ;
rng f c= the carrier of () by RELAT_1:def 19;
then ( rng (id the carrier of ()) = the carrier of () & rng f = the carrier of () ) by ;
then f = id () by ;
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 ;
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 ;
A8: AutMt (f * (Mx2Tran (AxialSymmetry (n,n)))) = (AutMt (Mx2Tran (AxialSymmetry (n,n)))) * () by Th29
.= (AxialSymmetry (n,n)) * () 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 () = n ) by MATRIX_0:24;
then ((AxialSymmetry (n,n)) ~) * ((AxialSymmetry (n,n)) * ()) = (((AxialSymmetry (n,n)) ~) * (AxialSymmetry (n,n))) * () by MATRIX_3:33
.= AutMt f by ;
hence AutMt f is Orthogonal by ; :: thesis: verum
end;
end;