let i, n be Nat; :: thesis: for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st f is {i} -support-yielding & f is rotation & not AutMt f = AxialSymmetry (i,n) holds
AutMt f = 1. (F_Real,n)
let f be additive homogeneous Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( f is {i} -support-yielding & f is rotation & not AutMt f = AxialSymmetry (i,n) implies AutMt f = 1. (F_Real,n) )
set TR = TOP-REAL n;
set S = { (Base_FinSeq (n,j)) where j is Element of NAT : ( 1 <= j & j <= n ) } ;
{ (Base_FinSeq (n,j)) where j is Element of NAT : ( 1 <= j & j <= n ) } c= the carrier of (TOP-REAL n)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Base_FinSeq (n,j)) where j is Element of NAT : ( 1 <= j & j <= n ) } or x in the carrier of (TOP-REAL n) )
assume x in { (Base_FinSeq (n,j)) where j is Element of NAT : ( 1 <= j & j <= n ) } ; :: thesis: x in the carrier of (TOP-REAL n)
then consider j being Element of NAT such that
A1: x = Base_FinSeq (n,j) and
( 1 <= j & j <= n ) ;
len (Base_FinSeq (n,j)) = n by MATRIXR2:74;
hence x in the carrier of (TOP-REAL n) by A1, TOPREAL3:46; :: thesis: verum
end;
then reconsider S = { (Base_FinSeq (n,j)) where j is Element of NAT : ( 1 <= j & j <= n ) } as Subset of (TOP-REAL n) ;
set M = Mx2Tran (AxialSymmetry (n,i));
assume A2: ( f is {i} -support-yielding & f is rotation ) ; :: thesis: ( AutMt f = AxialSymmetry (i,n) or AutMt f = 1. (F_Real,n) )
A3: id (TOP-REAL n) = Mx2Tran (1. (F_Real,n)) by MATRTOP1:33;
then A4: AutMt (id (TOP-REAL n)) = 1. (F_Real,n) by Def6;
A5: dom f = the carrier of (TOP-REAL n) by FUNCT_2:52;
per cases ( not i in Seg n or i in Seg n ) ;
suppose A6: not i in Seg n ; :: thesis: ( AutMt f = AxialSymmetry (i,n) or AutMt f = 1. (F_Real,n) )
now :: thesis: for p being Point of (TOP-REAL n) holds f . p = p
let p be Point of (TOP-REAL n); :: thesis: f . p = p
A7: now :: thesis: for j being Nat st 1 <= j & j <= n holds
(f . p) . j = p . j
let j be Nat; :: thesis: ( 1 <= j & j <= n implies (f . p) . j = p . j )
assume ( 1 <= j & j <= n ) ; :: thesis: (f . p) . j = p . j
then j <> i by A6;
then not j in {i} by TARSKI:def 1;
hence (f . p) . j = p . j by A2, A5; :: thesis: verum
end;
( len (f . p) = n & len p = n ) by CARD_1:def 7;
hence f . p = p by A7; :: thesis: verum
end;
then f = id (TOP-REAL n) by FUNCT_2:124;
hence ( AutMt f = AxialSymmetry (i,n) or AutMt f = 1. (F_Real,n) ) by A3, Def6; :: thesis: verum
end;
suppose A8: i in Seg n ; :: thesis: ( AutMt f = AxialSymmetry (i,n) or AutMt f = 1. (F_Real,n) )
then ( 1 <= i & i <= n ) by FINSEQ_1:1;
then Base_FinSeq (n,i) in S by A8;
then reconsider B = Base_FinSeq (n,i) as Point of (TOP-REAL n) ;
B = (0* n) +* (i,1) by MATRIXR2:def 4;
then A9: |.B.| = |.1.| by A8, TOPREALC:13
.= 1 by ABSVALUE:def 1 ;
set B0 = (0* n) +* (i,((f . B) . i));
A10: len (0* n) = n by CARD_1:def 7;
A11: for j being Nat st 1 <= j & j <= n holds
(f . B) . j = ((0* n) +* (i,((f . B) . i))) . j
proof
let j be Nat; :: thesis: ( 1 <= j & j <= n implies (f . B) . j = ((0* n) +* (i,((f . B) . i))) . j )
assume A12: ( 1 <= j & j <= n ) ; :: thesis: (f . B) . j = ((0* n) +* (i,((f . B) . i))) . j
A13: j in dom (0* n) by A10, A12, FINSEQ_3:25;
per cases ( j = i or j <> i ) ;
suppose j = i ; :: thesis: (f . B) . j = ((0* n) +* (i,((f . B) . i))) . j
hence ((0* n) +* (i,((f . B) . i))) . j = (f . B) . j by A13, FUNCT_7:31; :: thesis: verum
end;
suppose A14: j <> i ; :: thesis: (f . B) . j = ((0* n) +* (i,((f . B) . i))) . j
then A15: not j in {i} by TARSKI:def 1;
thus ((0* n) +* (i,((f . B) . i))) . j = (0* n) . j by A14, FUNCT_7:32
.= 0
.= B . j by A12, A14, MATRIXR2:76
.= (f . B) . j by A2, A5, A15 ; :: thesis: verum
end;
end;
end;
( len ((0* n) +* (i,((f . B) . i))) = len (0* n) & len (f . B) = n ) by CARD_1:def 7, FUNCT_7:97;
then A16: f . B = (0* n) +* (i,((f . B) . i)) by A10, A11;
then A17: |.B.| = |.((0* n) +* (i,((f . B) . i))).| by A2
.= |.((f . B) . i).| by A8, TOPREALC:13 ;
A18: for h being additive homogeneous rotation Function of (TOP-REAL n),(TOP-REAL n) st h | S = id S holds
h = id (TOP-REAL n)
proof
let h be additive homogeneous rotation Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( h | S = id S implies h = id (TOP-REAL n) )
assume A19: h | S = id S ; :: thesis: h = id (TOP-REAL n)
A20: for x being object st x in dom (id (TOP-REAL n)) holds
(id (TOP-REAL n)) . x = h . x
proof
let x be object ; :: thesis: ( x in dom (id (TOP-REAL n)) implies (id (TOP-REAL n)) . x = h . x )
assume x in dom (id (TOP-REAL n)) ; :: thesis: (id (TOP-REAL n)) . x = h . x
then reconsider p = x as Point of (TOP-REAL n) ;
set hp = h . p;
A21: ( len p = n & len (h . p) = n ) by CARD_1:def 7;
A22: now :: thesis: for j being Nat st 1 <= j & j <= n holds
p . j = (h . p) . j
let j be Nat; :: thesis: ( 1 <= j & j <= n implies p . j = (h . p) . j )
assume A23: ( 1 <= j & j <= n ) ; :: thesis: p . j = (h . p) . j
then A24: j in Seg n ;
then Base_FinSeq (n,j) in S by A23;
then Base_FinSeq (n,j) in Lin S by RLVECT_3:15;
hence p . j = (h . p) . j by A19, A24, Th32; :: thesis: verum
end;
thus (id (TOP-REAL n)) . x = h . x by A21, A22; :: thesis: verum
end;
dom h = the carrier of (TOP-REAL n) by FUNCT_2:def 1;
hence h = id (TOP-REAL n) by A20, FUNCT_1:2; :: thesis: verum
end;
per cases ( (f . B) . i >= 0 or (f . B) . i < 0 ) ;
suppose A25: (f . B) . i >= 0 ; :: thesis: ( AutMt f = AxialSymmetry (i,n) or AutMt f = 1. (F_Real,n) )
A26: dom (f | S) = S by A5, RELAT_1:62;
A27: (f . B) . i = 1 by A9, A17, A25, ABSVALUE:def 1;
A28: for x being object st x in S holds
(f | S) . x = (id S) . x
proof
let x be object ; :: thesis: ( x in S implies (f | S) . x = (id S) . x )
assume A29: x in S ; :: thesis: (f | S) . x = (id S) . x
then consider j being Element of NAT such that
A30: x = Base_FinSeq (n,j) and
1 <= j and
j <= n ;
A31: ( (f | S) . x = f . x & (id S) . x = x ) by A26, A29, FUNCT_1:17, FUNCT_1:47;
per cases ( j = i or j <> i ) ;
suppose j = i ; :: thesis: (f | S) . x = (id S) . x
hence (f | S) . x = (id S) . x by A16, A27, A30, A31, MATRIXR2:def 4; :: thesis: verum
end;
suppose j <> i ; :: thesis: (f | S) . x = (id S) . x
then not j in {i} by TARSKI:def 1;
hence (f | S) . x = (id S) . x by A2, A30, A31, Lm9; :: thesis: verum
end;
end;
end;
dom (id S) = S ;
hence ( AutMt f = AxialSymmetry (i,n) or AutMt f = 1. (F_Real,n) ) by A2, A4, A18, A26, A28, FUNCT_1:2; :: thesis: verum
end;
suppose A32: (f . B) . i < 0 ; :: thesis: ( AutMt f = AxialSymmetry (i,n) or AutMt f = 1. (F_Real,n) )
set MA = Mx2Tran (AxialSymmetry (i,n));
Mx2Tran (AxialSymmetry (i,n)) is rotation by A8, Th27;
then reconsider MAf = (Mx2Tran (AxialSymmetry (i,n))) * f as additive homogeneous rotation Function of (TOP-REAL n),(TOP-REAL n) by A2;
A33: dom MAf = the carrier of (TOP-REAL n) by FUNCT_2:52;
then A34: dom (MAf | S) = S by RELAT_1:62;
A35: ( Mx2Tran (AxialSymmetry (i,n)) is {i} -support-yielding & {i} \/ {i} = {i} ) by A8, Th11;
A36: for x being object st x in S holds
(MAf | S) . x = (id S) . x
proof
let x be object ; :: thesis: ( x in S implies (MAf | S) . x = (id S) . x )
assume A37: x in S ; :: thesis: (MAf | S) . x = (id S) . x
then consider j being Element of NAT such that
A38: x = Base_FinSeq (n,j) and
( 1 <= j & j <= n ) ;
A39: ( (MAf | S) . x = MAf . x & (id S) . x = x ) by A34, A37, FUNCT_1:17, FUNCT_1:47;
per cases ( j = i or j <> i ) ;
suppose A40: j = i ; :: thesis: (MAf | S) . x = (id S) . x
A41: for k being Nat st 1 <= k & k <= n holds
(MAf . B) . k = B . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= n implies (MAf . B) . k = B . k )
assume A42: ( 1 <= k & k <= n ) ; :: thesis: (MAf . B) . k = B . k
then A43: k in Seg n ;
per cases ( k = i or k <> i ) ;
suppose A44: k = i ; :: thesis: (MAf . B) . k = B . k
thus (MAf . B) . k = ((Mx2Tran (AxialSymmetry (i,n))) . (f . B)) . k by A33, FUNCT_1:12
.= - ((f . B) . k) by A43, A44, Th9
.= - (- 1) by A9, A17, A32, A44, ABSVALUE:def 1
.= B . k by A42, A44, MATRIXR2:75 ; :: thesis: verum
end;
suppose A45: k <> i ; :: thesis: (MAf . B) . k = B . k
then A46: not k in {i} by TARSKI:def 1;
thus (MAf . B) . k = ((Mx2Tran (AxialSymmetry (i,n))) . (f . B)) . k by A33, FUNCT_1:12
.= (f . B) . k by A8, A45, Th8
.= B . k by A2, A5, A46 ; :: thesis: verum
end;
end;
end;
( len (MAf . B) = n & len B = n ) by CARD_1:def 7;
hence (MAf | S) . x = (id S) . x by A38, A39, A40, A41, FINSEQ_1:14; :: thesis: verum
end;
suppose j <> i ; :: thesis: (MAf | S) . x = (id S) . x
then not j in {i} by TARSKI:def 1;
hence (MAf | S) . x = (id S) . x by A2, A35, A38, A39, Lm9; :: thesis: verum
end;
end;
end;
dom (id S) = S ;
then A47: MAf = id (TOP-REAL n) by A18, A34, A36, FUNCT_1:2;
A48: dom (Mx2Tran (AxialSymmetry (i,n))) = [#] (TOP-REAL n) by TOPS_2:def 5;
set R = AutMt f;
A49: rng (Mx2Tran (AxialSymmetry (i,n))) = [#] (TOP-REAL n) by TOPS_2:def 5;
A50: Mx2Tran (AxialSymmetry (i,n)) is one-to-one by TOPS_2:def 5;
A51: the carrier of (TOP-REAL n) c= rng f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (TOP-REAL n) or x in rng f )
assume A52: x in the carrier of (TOP-REAL n) ; :: thesis: x in rng f
then A53: (Mx2Tran (AxialSymmetry (i,n))) . x in rng (Mx2Tran (AxialSymmetry (i,n))) by A48, FUNCT_1:def 3;
then A54: MAf . ((Mx2Tran (AxialSymmetry (i,n))) . x) = (Mx2Tran (AxialSymmetry (i,n))) . (f . ((Mx2Tran (AxialSymmetry (i,n))) . x)) by A33, A49, FUNCT_1:12;
( f . ((Mx2Tran (AxialSymmetry (i,n))) . x) in dom (Mx2Tran (AxialSymmetry (i,n))) & MAf . ((Mx2Tran (AxialSymmetry (i,n))) . x) = (Mx2Tran (AxialSymmetry (i,n))) . x ) by A33, A47, A49, A53, FUNCT_1:11, FUNCT_1:18;
then x = f . ((Mx2Tran (AxialSymmetry (i,n))) . x) by A48, A50, A52, A54, FUNCT_1:def 4;
hence x in rng f by A5, A49, A53, FUNCT_1:def 3; :: thesis: verum
end;
rng f c= the carrier of (TOP-REAL n) by RELAT_1:def 19;
then rng f = the carrier of (TOP-REAL n) by A51, XBOOLE_0:def 10;
then A55: f = (Mx2Tran (AxialSymmetry (i,n))) " by A47, A49, A48, A50, FUNCT_1:42;
Det (AxialSymmetry (i,n)) = - (1. F_Real) by A8, Th4;
then ( f = Mx2Tran (AutMt f) & Det (AxialSymmetry (i,n)) <> 0. F_Real ) by Def6;
then AutMt f = (AxialSymmetry (i,n)) ~ by A55, MATRTOP1:43
.= AxialSymmetry (i,n) by A8, Th7 ;
hence ( AutMt f = AxialSymmetry (i,n) or AutMt f = 1. (F_Real,n) ) ; :: thesis: verum
end;
end;
end;
end;