let n be Nat; for f being homogeneous additive 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 homogeneous additive 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_1:24;
A2:
( n = 0 implies n = 0 )
;
A3:
n in NAT
by ORDINAL1:def 12;
( n = 0 or n >= 1 )
by NAT_1:14;
then A4:
( ( Det (1. (F_Real,n)) = 1_ F_Real & n >= 1 ) or ( Det (1. (F_Real,n)) = 1. F_Real & n = 0 ) )
by A3, MATRIXR2:41, MATRIX_7:16;
assume
f is rotation
; ( Det (AutMt f) = 1. F_Real or Det (AutMt f) = - (1. F_Real) )
then A5:
Mx2Tran (AutMt f) is rotation
by Def6;
then consider h being homogeneous additive Function of (TOP-REAL n),(TOP-REAL n) such that
A6:
h is base_rotation
and
A7:
h * (Mx2Tran (AutMt f)) is {n} -support-yielding
by Th35;
set R = AutMt h;
A8:
h = Mx2Tran (AutMt h)
by Def6;
then
( n in NAT & Det (AutMt h) = 1. F_Real )
by A6, Lm10, ORDINAL1:def 12;
then A9: Det ((AutMt f) * (AutMt h)) =
(Det (AutMt f)) * (1. F_Real)
by MATRIXR2:45
.=
Det (AutMt f)
;
width (AutMt h) = n
by MATRIX_1:24;
then A10:
h * (Mx2Tran (AutMt f)) = Mx2Tran ((AutMt f) * (AutMt h))
by A1, A2, A8, MATRTOP1:32;