:: AUTALG_1 semantic presentation

theorem Th1: :: AUTALG_1:1

for b₁ being Universal_Algebra holds id the carrier of b₁ is_isomorphism b₁,b₁

proof end;

definition

let c₁ be Universal_Algebra;
func UAAut c₁ -> FUNCTION_DOMAIN of the carrier of a₁,the carrier of a₁ means :Def1: :: AUTALG_1:def 1
( ( for b₁ being Element of a₂ holds b₁ is Function of a₁,a₁ ) & ( for b₁ being Function of a₁,a₁ holds
( b₁ in a₂ iff b₁ is_isomorphism a₁,a₁ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines UAAut AUTALG_1:def 1 :

theorem Th2: :: AUTALG_1:2

for b₁ being Universal_Algebra holds UAAut b₁ c= Funcs the carrier of b₁,the carrier of b₁

proof end;

theorem Th3: :: AUTALG_1:3

canceled;

theorem Th4: :: AUTALG_1:4

for b₁ being Universal_Algebra holds id the carrier of b₁ in UAAut b₁

proof end;

theorem Th5: :: AUTALG_1:5

for b₁ being Universal_Algebra
for b₂, b₃ being Function of b₁,b₁ st b₂ is Element of UAAut b₁ & b₃ = b₂ " holds
b₃ is_isomorphism b₁,b₁

proof end;

Lemma4: for b₁ being Universal_Algebra
for b₂ being Function of b₁,b₁ st b₂ is_isomorphism b₁,b₁ holds
b₂ " is Function of b₁,b₁

proof end;

theorem Th6: :: AUTALG_1:6

for b₁ being Universal_Algebra
for b₂ being Element of UAAut b₁ holds b₂ " in UAAut b₁

proof end;

theorem Th7: :: AUTALG_1:7

for b₁ being Universal_Algebra
for b₂, b₃ being Element of UAAut b₁ holds b₂ * b₃ in UAAut b₁

proof end;

definition

let c₁ be Universal_Algebra;
func UAAutComp c₁ -> BinOp of UAAut a₁ means :Def2: :: AUTALG_1:def 2
for b₁, b₂ being Element of UAAut a₁ holds a₂ . b₁,b₂ = b₂ * b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines UAAutComp AUTALG_1:def 2 :

definition

let c₁ be Universal_Algebra;
func UAAutGroup c₁ -> Group equals :: AUTALG_1:def 3
HGrStr(# (UAAut a₁),(UAAutComp a₁) #);
coherence

proof end;

end;

:: deftheorem Def3 defines UAAutGroup AUTALG_1:def 3 :

registration

let c₁ be Universal_Algebra;
cluster UAAutGroup a₁ -> strict ;
coherence ;

end;

Lemma8: for b₁ being Universal_Algebra
for b₂ being Element of UAAut b₁ holds
( dom b₂ = rng b₂ & dom b₂ = the carrier of b₁ )

proof end;

theorem Th8: :: AUTALG_1:8

for b₁ being Universal_Algebra
for b₂, b₃ being Element of (UAAutGroup b₁)
for b₄, b₅ being Element of UAAut b₁ st b₂ = b₄ & b₃ = b₅ holds
b₂ * b₃ = b₅ * b₄ by Def2;

theorem Th9: :: AUTALG_1:9

for b₁ being Universal_Algebra holds id the carrier of b₁ = 1. (UAAutGroup b₁)

proof end;

theorem Th10: :: AUTALG_1:10

for b₁ being Universal_Algebra
for b₂ being Element of UAAut b₁
for b₃ being Element of (UAAutGroup b₁) st b₂ = b₃ holds
b₂ " = b₃ "

proof end;

theorem Th11: :: AUTALG_1:11

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st b₂ is_transformable_to b₃ & b₃ is_transformable_to b₄ holds
b₂ is_transformable_to b₄

proof end;

theorem Th12: :: AUTALG_1:12

for b₁ being set
for b₂ being ManySortedSet of {b₁} holds b₂ = b₁ .--> (b₂ . b₁)

proof end;

theorem Th13: :: AUTALG_1:13

for b₁, b₂, b₃ being Function-yielding Function holds (b₃ ** b₂) ** b₁ = b₃ ** (b₂ ** b₁)

proof end;

theorem Th14: :: AUTALG_1:14

for b₁ being set
for b₂, b₃ being V2 ManySortedSet of b₁
for b₄ being ManySortedFunction of b₂,b₃ st b₄ is "1-1" & b₄ is "onto" holds
( b₄ "" is "1-1" & b₄ "" is "onto" )

proof end;

theorem Th15: :: AUTALG_1:15

for b₁ being set
for b₂, b₃ being V2 ManySortedSet of b₁
for b₄ being ManySortedFunction of b₂,b₃ st b₄ is "1-1" & b₄ is "onto" holds
(b₄ "" ) "" = b₄

proof end;

theorem Th16: :: AUTALG_1:16

for b₁, b₂ being Function-yielding Function st b₁ is "1-1" & b₂ is "1-1" holds
b₂ ** b₁ is "1-1"

proof end;

theorem Th17: :: AUTALG_1:17

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃, b₄ being V2 ManySortedSet of b₁
for b₅ being ManySortedFunction of b₂,b₃
for b₆ being ManySortedFunction of b₃,b₄ st b₅ is "onto" & b₆ is "onto" holds
b₆ ** b₅ is "onto"

proof end;

theorem Th18: :: AUTALG_1:18

for b₁ being set
for b₂, b₃, b₄ being V2 ManySortedSet of b₁
for b₅ being ManySortedFunction of b₂,b₃
for b₆ being ManySortedFunction of b₃,b₄ st b₅ is "1-1" & b₅ is "onto" & b₆ is "1-1" & b₆ is "onto" holds
(b₆ ** b₅) "" = (b₅ "" ) ** (b₆ "" )

proof end;

theorem Th19: :: AUTALG_1:19

for b₁ being set
for b₂, b₃ being V2 ManySortedSet of b₁
for b₄ being ManySortedFunction of b₂,b₃
for b₅ being ManySortedFunction of b₃,b₂ st b₄ is "1-1" & b₄ is "onto" & b₅ ** b₄ = id b₂ holds
b₅ = b₄ ""

proof end;

theorem Th20: :: AUTALG_1:20

canceled;

theorem Th21: :: AUTALG_1:21

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ is_transformable_to b₃ holds
for b₄ being set st b₄ in product (MSFuncs b₂,b₃) holds
b₄ is ManySortedFunction of b₂,b₃

proof end;

theorem Th22: :: AUTALG_1:22

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ is_transformable_to b₃ holds
for b₄ being ManySortedFunction of b₂,b₃ holds b₄ in product (MSFuncs b₂,b₃)

proof end;

theorem Th23: :: AUTALG_1:23

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ is_transformable_to b₃ holds
MSFuncs b₂,b₃ is non-empty

proof end;

definition

let c₁ be set ;
let c₂, c₃ be ManySortedSet of c₁;
assume E20: c₂ is_transformable_to c₃ ;
canceled;
canceled;
mode MSFunctionSet of c₂,c₃ -> non empty set means :Def6: :: AUTALG_1:def 6
for b₁ being set st b₁ in a₄ holds
b₁ is ManySortedFunction of a₂,a₃;
existence

proof end;

end;

:: deftheorem Def4 AUTALG_1:def 4 :

:: deftheorem Def5 AUTALG_1:def 5 :

:: deftheorem Def6 defines MSFunctionSet AUTALG_1:def 6 :

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
cluster MSFuncs a₂,a₂ -> V2 ;
coherence

proof end;

end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂, c₃ be non-empty MSAlgebra of c₁;
mode MSFunctionSet of a₂,a₃ is MSFunctionSet of the Sorts of a₂,the Sorts of a₃;

end;

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
cluster non empty MSFunctionSet of a₂,a₂;
existence

proof end;

end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃ be non empty MSFunctionSet of c₂,c₂;
redefine mode Element as Element of c₃ -> ManySortedFunction of a₂,a₂;
coherence by Def6;

end;

theorem Th24: :: AUTALG_1:24

for b₁ being set
for b₂ being ManySortedSet of b₁ holds id b₂ is "onto"

proof end;

theorem Th25: :: AUTALG_1:25

for b₁ being set
for b₂ being ManySortedSet of b₁ holds id b₂ is "1-1"

proof end;

theorem Th26: :: AUTALG_1:26

canceled;

theorem Th27: :: AUTALG_1:27

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds id the Sorts of b₂ in product (MSFuncs the Sorts of b₂,the Sorts of b₂) by Th22;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
func MSAAut c₂ -> MSFunctionSet of the Sorts of a₂,the Sorts of a₂ means :Def7: :: AUTALG_1:def 7
( ( for b₁ being Element of a₃ holds b₁ is ManySortedFunction of a₂,a₂ ) & ( for b₁ being ManySortedFunction of a₂,a₂ holds
( b₁ in a₃ iff b₁ is_isomorphism a₂,a₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines MSAAut AUTALG_1:def 7 :

theorem Th28: :: AUTALG_1:28

canceled;

theorem Th29: :: AUTALG_1:29

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being Element of MSAAut b₂ holds b₃ in product (MSFuncs the Sorts of b₂,the Sorts of b₂) by Th22;

theorem Th30: :: AUTALG_1:30

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds MSAAut b₂ c= product (MSFuncs the Sorts of b₂,the Sorts of b₂)

proof end;

Lemma22: for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being Element of MSAAut b₂ holds
( b₃ is "1-1" & b₃ is "onto" )

proof end;

theorem Th31: :: AUTALG_1:31

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds id the Sorts of b₂ in MSAAut b₂

proof end;

theorem Th32: :: AUTALG_1:32

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being Element of MSAAut b₂ holds b₃ "" in MSAAut b₂

proof end;

theorem Th33: :: AUTALG_1:33

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃, b₄ being Element of MSAAut b₂ holds b₃ ** b₄ in MSAAut b₂

proof end;

theorem Th34: :: AUTALG_1:34

for b₁ being Universal_Algebra
for b₂ being ManySortedFunction of (MSAlg b₁),(MSAlg b₁)
for b₃ being Element of UAAut b₁ st b₂ = 0 .--> b₃ holds
b₂ in MSAAut (MSAlg b₁)

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
func MSAAutComp c₂ -> BinOp of MSAAut a₂ means :Def8: :: AUTALG_1:def 8
for b₁, b₂ being Element of MSAAut a₂ holds a₃ . b₁,b₂ = b₂ ** b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines MSAAutComp AUTALG_1:def 8 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
func MSAAutGroup c₂ -> Group equals :: AUTALG_1:def 9
HGrStr(# (MSAAut a₂),(MSAAutComp a₂) #);
coherence

proof end;

end;

:: deftheorem Def9 defines MSAAutGroup AUTALG_1:def 9 :

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
cluster MSAAutGroup a₂ -> strict ;
coherence ;

end;

theorem Th35: :: AUTALG_1:35

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃, b₄ being Element of (MSAAutGroup b₂)
for b₅, b₆ being Element of MSAAut b₂ st b₃ = b₅ & b₄ = b₆ holds
b₃ * b₄ = b₆ ** b₅ by Def8;

theorem Th36: :: AUTALG_1:36

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds id the Sorts of b₂ = 1. (MSAAutGroup b₂)

proof end;

theorem Th37: :: AUTALG_1:37

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being Element of MSAAut b₂
for b₄ being Element of (MSAAutGroup b₂) st b₃ = b₄ holds
b₃ "" = b₄ "

proof end;

theorem Th38: :: AUTALG_1:38

for b₁, b₂ being Universal_Algebra st b₁,b₂ are_similar holds
for b₃ being ManySortedFunction of (MSAlg b₁),((MSAlg b₂) Over (MSSign b₁)) holds b₃ . 0 is Function of b₁,b₂

proof end;

theorem Th39: :: AUTALG_1:39

for b₁ being Universal_Algebra
for b₂ being Element of UAAut b₁ holds 0 .--> b₂ is ManySortedFunction of (MSAlg b₁),(MSAlg b₁)

proof end;

Lemma32: for b₁ being Universal_Algebra
for b₂ being Function st dom b₂ = UAAut b₁ & ( for b₃ being set st b₃ in UAAut b₁ holds
b₂ . b₃ = 0 .--> b₃ ) holds
rng b₂ = MSAAut (MSAlg b₁)

proof end;

theorem Th40: :: AUTALG_1:40

for b₁ being Universal_Algebra
for b₂ being Function st dom b₂ = UAAut b₁ & ( for b₃ being set st b₃ in UAAut b₁ holds
b₂ . b₃ = 0 .--> b₃ ) holds
b₂ is Homomorphism of (UAAutGroup b₁),(MSAAutGroup (MSAlg b₁))

proof end;

theorem Th41: :: AUTALG_1:41

for b₁ being Universal_Algebra
for b₂ being Homomorphism of (UAAutGroup b₁),(MSAAutGroup (MSAlg b₁)) st ( for b₃ being set st b₃ in UAAut b₁ holds
b₂ . b₃ = 0 .--> b₃ ) holds
b₂ is_isomorphism

proof end;

theorem Th42: :: AUTALG_1:42

for b₁ being Universal_Algebra holds UAAutGroup b₁, MSAAutGroup (MSAlg b₁) are_isomorphic

proof end;