let i, n be Nat; 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); ( 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)
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 )
; ( 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 A8:
i in Seg n
;
( 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
(
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)
per cases
( (f . B) . i >= 0 or (f . B) . i < 0 )
;
suppose A25:
(f . B) . i >= 0
;
( 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
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;
verum end; suppose A32:
(f . B) . i < 0
;
( 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 ;
( x in S implies (MAf | S) . x = (id S) . x )
assume A37:
x in S
;
(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
;
(MAf | S) . x = (id S) . xA41:
for
k being
Nat st 1
<= k &
k <= n holds
(MAf . B) . k = B . k
proof
let k be
Nat;
( 1 <= k & k <= n implies (MAf . B) . k = B . k )
assume A42:
( 1
<= k &
k <= n )
;
(MAf . B) . k = B . k
then A43:
k in Seg n
;
per cases
( k = i or k <> i )
;
suppose A44:
k = i
;
(MAf . B) . k = B . kthus (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
;
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;
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 ;
TARSKI:def 3 ( not x in the carrier of (TOP-REAL n) or x in rng f )
assume A52:
x in the
carrier of
(TOP-REAL n)
;
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;
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) )
;
verum end; end; end; end;