let i, n be Nat; :: thesis: for f being additive homogeneous Function of (),() 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 (),(); :: 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 ()
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 () )
assume x in { (Base_FinSeq (n,j)) where j is Element of NAT : ( 1 <= j & j <= n ) } ; :: thesis: x in the carrier of ()
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 () by ; :: thesis: verum
end;
then reconsider S = { (Base_FinSeq (n,j)) where j is Element of NAT : ( 1 <= j & j <= n ) } as Subset of () ;
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 () = Mx2Tran (1. (F_Real,n)) by MATRTOP1:33;
then A4: AutMt (id ()) = 1. (F_Real,n) by Def6;
A5: dom f = the carrier of () 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 () holds f . p = p
let p be Point of (); :: 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 () by FUNCT_2:124;
hence ( AutMt f = AxialSymmetry (i,n) or AutMt f = 1. (F_Real,n) ) by ; :: 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 () ;
B = (0* n) +* (i,1) by MATRIXR2:def 4;
then A9: |.B.| = |.1.| by
.= 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 ;
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 ; :: 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
.= 0
.= B . j by
.= (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 ;
then A16: f . B = (0* n) +* (i,((f . B) . i)) by ;
then A17: |.B.| = |.((0* n) +* (i,((f . B) . i))).| by A2
.= |.((f . B) . i).| by ;
A18: for h being additive homogeneous rotation Function of (),() st h | S = id S holds
h = id ()
proof
let h be additive homogeneous rotation Function of (),(); :: thesis: ( h | S = id S implies h = id () )
assume A19: h | S = id S ; :: thesis: h = id ()
A20: for x being object st x in dom (id ()) holds
(id ()) . x = h . x
proof
let x be object ; :: thesis: ( x in dom (id ()) implies (id ()) . x = h . x )
assume x in dom (id ()) ; :: thesis: (id ()) . x = h . x
then reconsider p = x as Point of () ;
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 ; :: thesis: verum
end;
thus (id ()) . x = h . x by ; :: thesis: verum
end;
dom h = the carrier of () by FUNCT_2:def 1;
hence h = id () by ; :: thesis: verum
end;
per cases ) . 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 ;
A27: (f . B) . i = 1 by ;
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 ;
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 ; :: 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 ; :: 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 ;
then reconsider MAf = (Mx2Tran (AxialSymmetry (i,n))) * f as additive homogeneous rotation Function of (),() by A2;
A33: dom MAf = the carrier of () 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 ;
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 ;
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
.= - ((f . B) . k) by
.= - (- 1) by
.= B . k by ; :: 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
.= (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 ; :: 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 () by ;
A48: dom (Mx2Tran (AxialSymmetry (i,n))) = [#] () by TOPS_2:def 5;
set R = AutMt f;
A49: rng (Mx2Tran (AxialSymmetry (i,n))) = [#] () by TOPS_2:def 5;
A50: Mx2Tran (AxialSymmetry (i,n)) is one-to-one by TOPS_2:def 5;
A51: the carrier of () c= rng f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of () or x in rng f )
assume A52: x in the carrier of () ; :: thesis: x in rng f
then A53: (Mx2Tran (AxialSymmetry (i,n))) . x in rng (Mx2Tran (AxialSymmetry (i,n))) by ;
then A54: MAf . ((Mx2Tran (AxialSymmetry (i,n))) . x) = (Mx2Tran (AxialSymmetry (i,n))) . (f . ((Mx2Tran (AxialSymmetry (i,n))) . x)) by ;
( f . ((Mx2Tran (AxialSymmetry (i,n))) . x) in dom (Mx2Tran (AxialSymmetry (i,n))) & MAf . ((Mx2Tran (AxialSymmetry (i,n))) . x) = (Mx2Tran (AxialSymmetry (i,n))) . x ) by ;
then x = f . ((Mx2Tran (AxialSymmetry (i,n))) . x) by ;
hence x in rng f by ; :: thesis: verum
end;
rng f c= the carrier of () by RELAT_1:def 19;
then rng f = the carrier of () by ;
then A55: f = (Mx2Tran (AxialSymmetry (i,n))) " by ;
Det (AxialSymmetry (i,n)) = - () by ;
then ( f = Mx2Tran () & Det (AxialSymmetry (i,n)) <> 0. F_Real ) by Def6;
then AutMt f = (AxialSymmetry (i,n)) ~ by
.= AxialSymmetry (i,n) by ;
hence ( AutMt f = AxialSymmetry (i,n) or AutMt f = 1. (F_Real,n) ) ; :: thesis: verum
end;
end;
end;
end;