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

let f be additive homogeneous Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( not f is rotation or Det (AutMt f) = 1. F_Real or Det (AutMt f) = - (1. F_Real) )

set M = AutMt f;

set MM = Mx2Tran (AutMt f);

set TR = TOP-REAL n;

A1: ( len (AutMt f) = n & width (AutMt f) = n ) by MATRIX_0:24;

A2: ( n = 0 implies n = 0 ) ;

( n = 0 or n >= 1 ) by NAT_1:14;

then A3: ( ( Det (1. (F_Real,n)) = 1_ F_Real & n >= 1 ) or ( Det (1. (F_Real,n)) = 1. F_Real & n = 0 ) ) by MATRIXR2:41, MATRIX_7:16;

assume f is rotation ; :: thesis: ( Det (AutMt f) = 1. F_Real or Det (AutMt f) = - (1. F_Real) )

then A4: Mx2Tran (AutMt f) is rotation by Def6;

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 Th36;

set R = AutMt h;

A7: h = Mx2Tran (AutMt h) by Def6;

then ( n in NAT & Det (AutMt h) = 1. F_Real ) by A5, Lm10, ORDINAL1:def 12;

then A8: Det ((AutMt f) * (AutMt h)) = (Det (AutMt f)) * (1. F_Real) by MATRIXR2:45

.= (Det (AutMt f)) * 1

.= Det (AutMt f) ;

width (AutMt h) = n by MATRIX_0:24;

then A9: h * (Mx2Tran (AutMt f)) = Mx2Tran ((AutMt f) * (AutMt h)) by A1, A2, A7, MATRTOP1:32;

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

let f be additive homogeneous Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( not f is rotation or Det (AutMt f) = 1. F_Real or Det (AutMt f) = - (1. F_Real) )

set M = AutMt f;

set MM = Mx2Tran (AutMt f);

set TR = TOP-REAL n;

A1: ( len (AutMt f) = n & width (AutMt f) = n ) by MATRIX_0:24;

A2: ( n = 0 implies n = 0 ) ;

( n = 0 or n >= 1 ) by NAT_1:14;

then A3: ( ( Det (1. (F_Real,n)) = 1_ F_Real & n >= 1 ) or ( Det (1. (F_Real,n)) = 1. F_Real & n = 0 ) ) by MATRIXR2:41, MATRIX_7:16;

assume f is rotation ; :: thesis: ( Det (AutMt f) = 1. F_Real or Det (AutMt f) = - (1. F_Real) )

then A4: Mx2Tran (AutMt f) is rotation by Def6;

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 Th36;

set R = AutMt h;

A7: h = Mx2Tran (AutMt h) by Def6;

then ( n in NAT & Det (AutMt h) = 1. F_Real ) by A5, Lm10, ORDINAL1:def 12;

then A8: Det ((AutMt f) * (AutMt h)) = (Det (AutMt f)) * (1. F_Real) by MATRIXR2:45

.= (Det (AutMt f)) * 1

.= Det (AutMt f) ;

width (AutMt h) = n by MATRIX_0:24;

then A9: h * (Mx2Tran (AutMt f)) = Mx2Tran ((AutMt f) * (AutMt h)) by A1, A2, A7, MATRTOP1:32;

per cases
( AutMt (h * (Mx2Tran (AutMt f))) = 1. (F_Real,n) or ( AutMt (h * (Mx2Tran (AutMt f))) <> 1. (F_Real,n) & AutMt (h * (Mx2Tran (AutMt f))) = AxialSymmetry (n,n) ) )
by A4, A5, A6, Th35;

end;

suppose
AutMt (h * (Mx2Tran (AutMt f))) = 1. (F_Real,n)
; :: thesis: ( Det (AutMt f) = 1. F_Real or Det (AutMt f) = - (1. F_Real) )

hence
( Det (AutMt f) = 1. F_Real or Det (AutMt f) = - (1. F_Real) )
by A3, A8, A9, Def6; :: thesis: verum

end;suppose A10:
( AutMt (h * (Mx2Tran (AutMt f))) <> 1. (F_Real,n) & AutMt (h * (Mx2Tran (AutMt f))) = AxialSymmetry (n,n) )
; :: thesis: ( Det (AutMt f) = 1. F_Real or Det (AutMt f) = - (1. F_Real) )

set cTR = the carrier of (TOP-REAL n);

n <> 0

then Det (AxialSymmetry (n,n)) = - (1. F_Real) by Th4;

hence ( Det (AutMt f) = 1. F_Real or Det (AutMt f) = - (1. F_Real) ) by A8, A9, A10, Def6; :: thesis: verum

end;n <> 0

proof

then
n in Seg n
by FINSEQ_1:3;
A11:
( 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 A12: 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 A12, ZFMISC_1:33;

then h * (Mx2Tran (AutMt f)) = id (TOP-REAL n) by A11, A12, FUNCT_1:7

.= Mx2Tran (1. (F_Real,n)) by MATRTOP1:33 ;

hence contradiction by A10, Def6; :: thesis: verum

end;assume n = 0 ; :: thesis: contradiction

then A12: 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 A12, ZFMISC_1:33;

then h * (Mx2Tran (AutMt f)) = id (TOP-REAL n) by A11, A12, FUNCT_1:7

.= Mx2Tran (1. (F_Real,n)) by MATRTOP1:33 ;

hence contradiction by A10, Def6; :: thesis: verum

then Det (AxialSymmetry (n,n)) = - (1. F_Real) by Th4;

hence ( Det (AutMt f) = 1. F_Real or Det (AutMt f) = - (1. F_Real) ) by A8, A9, A10, Def6; :: thesis: verum