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