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)

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;

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

then reconsider S = { (Base_FinSeq (n,j)) where j is Element of NAT : ( 1 <= j & j <= n ) } as Subset of (TOP-REAL n) ;
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;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

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 )
;

end;

suppose A6:
not i in Seg n
; :: thesis: ( AutMt f = AxialSymmetry (i,n) or AutMt f = 1. (F_Real,n) )

hence ( AutMt f = AxialSymmetry (i,n) or AutMt f = 1. (F_Real,n) ) by A3, Def6; :: thesis: verum

end;

now :: thesis: for p being Point of (TOP-REAL n) holds f . p = p

then
f = id (TOP-REAL n)
by FUNCT_2:124;let p be Point of (TOP-REAL n); :: thesis: f . p = p

hence f . p = p by A7; :: thesis: verum

end;A7: now :: thesis: for j being Nat st 1 <= j & j <= n holds

(f . p) . j = p . j

( len (f . p) = n & len p = n )
by CARD_1:def 7;(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;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

hence f . p = p by A7; :: thesis: verum

hence ( AutMt f = AxialSymmetry (i,n) or AutMt f = 1. (F_Real,n) ) by A3, Def6; :: thesis: verum

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

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)

end;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

( len ((0* n) +* (i,((f . B) . i))) = len (0* n) & len (f . B) = n )
by CARD_1:def 7, FUNCT_7:97;
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;

end;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;

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

hence h = id (TOP-REAL n) by A20, FUNCT_1:2; :: thesis: verum

end;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

dom h = the carrier of (TOP-REAL n)
by FUNCT_2:def 1;
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;

end;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

thus
(id (TOP-REAL n)) . x = h . x
by A21, A22; :: thesis: verump . 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;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

hence h = id (TOP-REAL n) by A20, FUNCT_1:2; :: thesis: verum

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

end;

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

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;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

dom (id S) = S
;
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;

end;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;

hence ( AutMt f = AxialSymmetry (i,n) or AutMt f = 1. (F_Real,n) ) by A2, A4, A18, A26, A28, FUNCT_1:2; :: thesis: verum

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

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

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;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

dom (id S) = S
;
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;

end;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 )
;

end;

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

hence (MAf | S) . x = (id S) . x by A38, A39, A40, A41, FINSEQ_1:14; :: thesis: verum

end;(MAf . B) . k = B . k

proof

( len (MAf . B) = n & len B = n )
by CARD_1:def 7;
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 ;

end;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 )
;

end;

hence (MAf | S) . x = (id S) . x by A38, A39, A40, A41, FINSEQ_1:14; :: thesis: verum

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

rng f c= the carrier of (TOP-REAL n)
by RELAT_1:def 19;
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;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

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