let i, n be Nat; :: thesis: for f1, f2 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st f1 is rotation & Det (AutMt f1) = - (1. F_Real) & i in Seg n & AutMt f2 = AxialSymmetry (i,n) holds
f1 * f2 is base_rotation
let f1, f2 be additive homogeneous Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( f1 is rotation & Det (AutMt f1) = - (1. F_Real) & i in Seg n & AutMt f2 = AxialSymmetry (i,n) implies f1 * f2 is base_rotation )
set M = AutMt f1;
set A = AutMt f2;
assume that
A1: f1 is rotation and
A2: Det (AutMt f1) = - (1. F_Real) and
A3: i in Seg n and
A4: AutMt f2 = AxialSymmetry (i,n) ; :: thesis: f1 * f2 is base_rotation
A5: f2 = Mx2Tran (AxialSymmetry (i,n)) by A4, Def6;
reconsider MF = (Mx2Tran (AutMt f1)) * f2 as additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) ;
set A = AxialSymmetry (i,n);
set R = AutMt MF;
A6: ( n = 0 implies n = 0 ) ;
A7: ( MF = Mx2Tran (AutMt MF) & width (AutMt f1) = n ) by Def6, MATRIX_0:24;
( len (AxialSymmetry (i,n)) = n & width (AxialSymmetry (i,n)) = n ) by MATRIX_0:24;
then Mx2Tran (AutMt MF) = Mx2Tran ((AxialSymmetry (i,n)) * (AutMt f1)) by A5, A6, A7, MATRTOP1:32;
then A8: AutMt MF = (AxialSymmetry (i,n)) * (AutMt f1) by MATRTOP1:34;
( n in NAT & Det (AxialSymmetry (i,n)) = - (1. F_Real) ) by A3, Th4, ORDINAL1:def 12;
then A9: Det (AutMt MF) = (- (1. F_Real)) * (- (1. F_Real)) by A2, A8, MATRIXR2:45
.= (- (1. F_Real)) * (- 1)
.= 1. F_Real ;
A10: Mx2Tran (AutMt f1) = f1 by Def6;
f2 is rotation by A3, A5, Th27;
hence f1 * f2 is base_rotation by A10, A1, A9, Th37; :: thesis: verum