let i, n be Nat; :: thesis: for f being homogeneous additive 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 homogeneous additive 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 set ; :: 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, TOPREAL7:17; :: 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

let p be Point of (TOP-REAL n); :: thesis: f . p = p

A7: now

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, FINSEQ_1:1;
then not j in {i} by TARSKI:def 1;
hence (f . p) . j = p . j by A2, A5, Def1; :: thesis: verum

end;

( len (f . p) = n & len p = n ) by CARD_1:def 7;
hence f . p = p by A7, FINSEQ_1:14; :: 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.| = abs 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
then A13: j in Seg n by FINSEQ_1:1;
A14: 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 A14, FUNCT_7:31; :: thesis: verum

end;

suppose A15: j <> i ; :: thesis: (f . B) . j = ((0* n) +* (i,((f . B) . i))) . j

then A16: not j in {i} by TARSKI:def 1;
thus ((0* n) +* (i,((f . B) . i))) . j = (0* n) . j by A15, FUNCT_7:32
.= 0 by A13, FINSEQ_2:57
.= B . j by A12, A15, MATRIXR2:76
.= (f . B) . j by A2, A5, A16, Def1 ; :: 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 A17: f . B = (0* n) +* (i,((f . B) . i)) by A10, A11, FINSEQ_1:14;
then A18: |.B.| = |.((0* n) +* (i,((f . B) . i))).| by A2, Def4
.= abs ((f . B) . i) by A8, TOPREALC:13 ;
A19: for h being homogeneous additive rotation Function of (TOP-REAL n),(TOP-REAL n) st h | S = id S holds
h = id (TOP-REAL n)

proof

let h be homogeneous additive rotation Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( h | S = id S implies h = id (TOP-REAL n) )
A20: dom (id (TOP-REAL n)) = the carrier of (TOP-REAL n) by FUNCT_2:def 1;
assume A21: h | S = id S ; :: thesis: h = id (TOP-REAL n)
A22: for x being set st x in dom (id (TOP-REAL n)) holds
(id (TOP-REAL n)) . x = h . x

proof

let x be set ; :: thesis: ( x in dom (id (TOP-REAL n)) implies (id (TOP-REAL n)) . x = h . x )
assume A23: 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) by FUNCT_2:def 1;
set hp = h . p;
A24: ( len p = n & len (h . p) = n ) by CARD_1:def 7;

A25: now

let j be Nat; :: thesis: ( 1 <= j & j <= n implies p . j = (h . p) . j )
assume A26: ( 1 <= j & j <= n ) ; :: thesis: p . j = (h . p) . j
then A27: j in Seg n by FINSEQ_1:1;
then Base_FinSeq (n,j) in S by A26;
then Base_FinSeq (n,j) in Lin S by RLVECT_3:15;
hence p . j = (h . p) . j by A21, A27, Th31; :: thesis: verum

end;

(id (TOP-REAL n)) . x = x by A20, A23, FUNCT_1:17;
hence (id (TOP-REAL n)) . x = h . x by A24, A25, FINSEQ_1:14; :: thesis: verum

end;

dom h = the carrier of (TOP-REAL n) by FUNCT_2:def 1;
hence h = id (TOP-REAL n) by A20, A22, FUNCT_1:2; :: thesis: verum

end;

per cases ( (f . B) . i >= 0 or (f . B) . i < 0 ) ;

suppose A28: (f . B) . i >= 0 ; :: thesis: ( AutMt f = AxialSymmetry (i,n) or AutMt f = 1. (F_Real,n) )

A29: dom (f | S) = S by A5, RELAT_1:62;
A30: (f . B) . i = 1 by A9, A18, A28, ABSVALUE:def 1;
A31: for x being set st x in S holds
(f | S) . x = (id S) . x

proof

let x be set ; :: thesis: ( x in S implies (f | S) . x = (id S) . x )
assume A32: x in S ; :: thesis: (f | S) . x = (id S) . x
then consider j being Element of NAT such that
A33: x = Base_FinSeq (n,j) and
1 <= j and
j <= n ;
A34: ( (f | S) . x = f . x & (id S) . x = x ) by A29, A32, 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 A17, A30, A33, A34, 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, A33, A34, Lm9; :: thesis: verum

end;

end;

end;

dom (id S) = S by FUNCT_2:52;
hence ( AutMt f = AxialSymmetry (i,n) or AutMt f = 1. (F_Real,n) ) by A2, A4, A19, A29, A31, FUNCT_1:2; :: thesis: verum

end;

suppose A35: (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, Th25;
then reconsider MAf = (Mx2Tran (AxialSymmetry (i,n))) * f as homogeneous additive rotation Function of (TOP-REAL n),(TOP-REAL n) by A2;
A36: dom MAf = the carrier of (TOP-REAL n) by FUNCT_2:52;
then A37: dom (MAf | S) = S by RELAT_1:62;
A38: ( Mx2Tran (AxialSymmetry (i,n)) is {i} -support-yielding & {i} \/ {i} = {i} ) by A8, Th28;
A39: for x being set st x in S holds
(MAf | S) . x = (id S) . x

proof

let x be set ; :: thesis: ( x in S implies (MAf | S) . x = (id S) . x )
assume A40: x in S ; :: thesis: (MAf | S) . x = (id S) . x
then consider j being Element of NAT such that
A41: x = Base_FinSeq (n,j) and
( 1 <= j & j <= n ) ;
A42: ( (MAf | S) . x = MAf . x & (id S) . x = x ) by A37, A40, FUNCT_1:17, FUNCT_1:47;

per cases ( j = i or j <> i ) ;

suppose A43: j = i ; :: thesis: (MAf | S) . x = (id S) . x

A44: 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 A45: ( 1 <= k & k <= n ) ; :: thesis: (MAf . B) . k = B . k
then A46: k in Seg n by FINSEQ_1:1;

per cases ( k = i or k <> i ) ;

suppose A47: k = i ; :: thesis: (MAf . B) . k = B . k

thus (MAf . B) . k = ((Mx2Tran (AxialSymmetry (i,n))) . (f . B)) . k by A36, FUNCT_1:12
.= - ((f . B) . k) by A46, A47, Th17
.= - (- 1) by A9, A18, A35, A47, ABSVALUE:def 1
.= B . k by A45, A47, MATRIXR2:75 ; :: thesis: verum

end;

suppose A48: k <> i ; :: thesis: (MAf . B) . k = B . k

then A49: not k in {i} by TARSKI:def 1;
thus (MAf . B) . k = ((Mx2Tran (AxialSymmetry (i,n))) . (f . B)) . k by A36, FUNCT_1:12
.= (f . B) . k by A8, A48, Th16
.= B . k by A2, A5, A49, Def1 ; :: 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 A41, A42, A43, A44, 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, A38, A41, A42, Lm9; :: thesis: verum

end;

end;

end;

dom (id S) = S by FUNCT_2:52;
then A50: MAf = id (TOP-REAL n) by A19, A37, A39, FUNCT_1:2;
A51: dom (Mx2Tran (AxialSymmetry (i,n))) = [#] (TOP-REAL n) by TOPS_2:def 5;
set R = AutMt f;
A52: rng (Mx2Tran (AxialSymmetry (i,n))) = [#] (TOP-REAL n) by TOPS_2:def 5;
A53: Mx2Tran (AxialSymmetry (i,n)) is one-to-one by TOPS_2:def 5;
A54: the carrier of (TOP-REAL n) c= rng f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (TOP-REAL n) or x in rng f )
assume A55: x in the carrier of (TOP-REAL n) ; :: thesis: x in rng f
then A56: (Mx2Tran (AxialSymmetry (i,n))) . x in rng (Mx2Tran (AxialSymmetry (i,n))) by A51, FUNCT_1:def 3;
then A57: MAf . ((Mx2Tran (AxialSymmetry (i,n))) . x) = (Mx2Tran (AxialSymmetry (i,n))) . (f . ((Mx2Tran (AxialSymmetry (i,n))) . x)) by A36, A52, 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 A36, A50, A52, A56, FUNCT_1:11, FUNCT_1:18;
then x = f . ((Mx2Tran (AxialSymmetry (i,n))) . x) by A51, A53, A55, A57, FUNCT_1:def 4;
hence x in rng f by A5, A52, A56, 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 A54, XBOOLE_0:def 10;
then A58: f = (Mx2Tran (AxialSymmetry (i,n))) " by A50, A52, A51, A53, FUNCT_1:42;
( f = Mx2Tran (AutMt f) & Det (AxialSymmetry (i,n)) <> 0. F_Real ) by A8, Def6, Th12;
then AutMt f = (AxialSymmetry (i,n)) ~ by A58, MATRTOP1:43
.= AxialSymmetry (i,n) by A8, Th15 ;
hence ( AutMt f = AxialSymmetry (i,n) or AutMt f = 1. (F_Real,n) ) ; :: thesis: verum

end;

end;

end;

end;