:: UNIALG_2 semantic presentation

theorem Th1: :: UNIALG_2:1

for b₁ being Nat
for b₂ being non empty set
for b₃ being non empty Subset of b₂ holds (b₁ -tuples_on b₂) /\ (b₁ -tuples_on b₃) = b₁ -tuples_on b₃

proof end;

theorem Th2: :: UNIALG_2:2

for b₁ being non empty set
for b₂ being non empty homogeneous quasi_total PartFunc of b₁ * ,b₁ holds dom b₂ = (arity b₂) -tuples_on b₁

proof end;

definition

let c₁ be non empty set ;
mode PFuncsDomHQN of c₁ -> non empty set means :Def1: :: UNIALG_2:def 1
for b₁ being Element of a₂ holds b₁ is non empty homogeneous quasi_total PartFunc of a₁ * ,a₁;
existence

proof end;

end;

:: deftheorem Def1 defines PFuncsDomHQN UNIALG_2:def 1 :

definition

let c₁ be non empty set ;
let c₂ be PFuncsDomHQN of c₁;
redefine mode Element as Element of c₂ -> non empty homogeneous quasi_total PartFunc of a₁ * ,a₁;
coherence by Def1;

end;

definition

let c₁ be Universal_Algebra;
mode PFuncsDomHQN of a₁ is PFuncsDomHQN of the carrier of a₁;

end;

definition

let c₁ be UAStr ;
mode PartFunc of a₁ is PartFunc of the carrier of a₁ * ,the carrier of a₁;

end;

definition

let c₁, c₂ be Universal_Algebra;
pred c₁,c₂ are_similar means :Def2: :: UNIALG_2:def 2
signature a₁ = signature a₂;
symmetry ;
reflexivity ;

end;

:: deftheorem Def2 defines are_similar UNIALG_2:def 2 :

theorem Th3: :: UNIALG_2:3

for b₁, b₂ being Universal_Algebra st b₁,b₂ are_similar holds
len the charact of b₁ = len the charact of b₂

proof end;

theorem Th4: :: UNIALG_2:4

for b₁, b₂, b₃ being Universal_Algebra st b₁,b₂ are_similar & b₂,b₃ are_similar holds
b₁,b₃ are_similar

proof end;

theorem Th5: :: UNIALG_2:5

for b₁ being Universal_Algebra holds rng the charact of b₁ is non empty Subset of (PFuncs (the carrier of b₁ * ),the carrier of b₁) by FINSEQ_1:27, FINSEQ_1:def 4;

definition

let c₁ be Universal_Algebra;
func Operations c₁ -> PFuncsDomHQN of a₁ equals :: UNIALG_2:def 3
rng the charact of a₁;
coherence

proof end;

end;

:: deftheorem Def3 defines Operations UNIALG_2:def 3 :

definition

let c₁ be Universal_Algebra;
mode operation of a₁ is Element of Operations a₁;

end;

theorem Th6: :: UNIALG_2:6

for b₁ being Universal_Algebra
for b₂ being set st b₂ in dom the charact of b₁ holds
the charact of b₁ . b₂ is operation of b₁ by FUNCT_1:def 5;

definition

let c₁ be Universal_Algebra;
let c₂ be Subset of c₁;
let c₃ be operation of c₁;
pred c₂ is_closed_on c₃ means :Def4: :: UNIALG_2:def 4
for b₁ being FinSequence of a₂ st len b₁ = arity a₃ holds
a₃ . b₁ in a₂;

end;

:: deftheorem Def4 defines is_closed_on UNIALG_2:def 4 :

definition

let c₁ be Universal_Algebra;
let c₂ be Subset of c₁;
attr a₂ is opers_closed means :Def5: :: UNIALG_2:def 5
for b₁ being operation of a₁ holds a₂ is_closed_on b₁;

end;

:: deftheorem Def5 defines opers_closed UNIALG_2:def 5 :

definition

let c₁ be Universal_Algebra;
let c₂ be non empty Subset of c₁;
let c₃ be operation of c₁;
assume E8: c₂ is_closed_on c₃ ;
func c₃ /. c₂ -> non empty homogeneous quasi_total PartFunc of a₂ * ,a₂ equals :Def6: :: UNIALG_2:def 6
a₃ | ((arity a₃) -tuples_on a₂);
coherence

proof end;

end;

:: deftheorem Def6 defines /. UNIALG_2:def 6 :

definition

let c₁ be Universal_Algebra;
let c₂ be non empty Subset of c₁;
func Opers c₁,c₂ -> PFuncFinSequence of a₂ means :Def7: :: UNIALG_2:def 7
( dom a₃ = dom the charact of a₁ & ( for b₁ being set
for b₂ being operation of a₁ st b₁ in dom a₃ & b₂ = the charact of a₁ . b₁ holds
a₃ . b₁ = b₂ /. a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines Opers UNIALG_2:def 7 :

theorem Th7: :: UNIALG_2:7

for b₁ being Universal_Algebra
for b₂ being non empty Subset of b₁ st b₂ = the carrier of b₁ holds
( b₂ is opers_closed & ( for b₃ being operation of b₁ holds b₃ /. b₂ = b₃ ) )

proof end;

theorem Th8: :: UNIALG_2:8

for b₁ being Universal_Algebra
for b₂ being non empty Subset of b₁
for b₃ being operation of b₁ st b₂ is_closed_on b₃ holds
arity (b₃ /. b₂) = arity b₃

proof end;

definition

let c₁ be Universal_Algebra;
mode SubAlgebra of c₁ -> Universal_Algebra means :Def8: :: UNIALG_2:def 8
( the carrier of a₂ is Subset of a₁ & ( for b₁ being non empty Subset of a₁ st b₁ = the carrier of a₂ holds
( the charact of a₂ = Opers a₁,b₁ & b₁ is opers_closed ) ) );
existence

proof end;

end;

:: deftheorem Def8 defines SubAlgebra UNIALG_2:def 8 :

registration

let c₁ be Universal_Algebra;
cluster strict SubAlgebra of a₁;
existence

proof end;

end;

theorem Th9: :: UNIALG_2:9

for b₁, b₂ being Universal_Algebra
for b₃ being operation of b₁
for b₄ being operation of b₂
for b₅ being Nat st b₁ is SubAlgebra of b₂ & b₅ in dom the charact of b₁ & b₃ = the charact of b₁ . b₅ & b₄ = the charact of b₂ . b₅ holds
arity b₃ = arity b₄

proof end;

theorem Th10: :: UNIALG_2:10

for b₁, b₂ being Universal_Algebra st b₁ is SubAlgebra of b₂ holds
dom the charact of b₁ = dom the charact of b₂

proof end;

theorem Th11: :: UNIALG_2:11

for b₁ being Universal_Algebra holds b₁ is SubAlgebra of b₁

proof end;

theorem Th12: :: UNIALG_2:12

for b₁, b₂, b₃ being Universal_Algebra st b₁ is SubAlgebra of b₂ & b₂ is SubAlgebra of b₃ holds
b₁ is SubAlgebra of b₃

proof end;

theorem Th13: :: UNIALG_2:13

for b₁, b₂ being Universal_Algebra st b₁ is strict SubAlgebra of b₂ & b₂ is strict SubAlgebra of b₁ holds
b₁ = b₂

proof end;

theorem Th14: :: UNIALG_2:14

for b₁ being Universal_Algebra
for b₂, b₃ being SubAlgebra of b₁ st the carrier of b₂ c= the carrier of b₃ holds
b₂ is SubAlgebra of b₃

proof end;

theorem Th15: :: UNIALG_2:15

for b₁ being Universal_Algebra
for b₂, b₃ being strict SubAlgebra of b₁ st the carrier of b₂ = the carrier of b₃ holds
b₂ = b₃

proof end;

theorem Th16: :: UNIALG_2:16

for b₁, b₂ being Universal_Algebra st b₁ is SubAlgebra of b₂ holds
b₁,b₂ are_similar

proof end;

theorem Th17: :: UNIALG_2:17

for b₁ being Universal_Algebra
for b₂ being non empty Subset of b₁ holds UAStr(# b₂,(Opers b₁,b₂) #) is strict Universal_Algebra

proof end;

definition

let c₁ be Universal_Algebra;
let c₂ be non empty Subset of c₁;
assume E18: c₂ is opers_closed ;
func UniAlgSetClosed c₂ -> strict SubAlgebra of a₁ equals :Def9: :: UNIALG_2:def 9
UAStr(# a₂,(Opers a₁,a₂) #);
coherence

proof end;

end;

:: deftheorem Def9 defines UniAlgSetClosed UNIALG_2:def 9 :

definition

let c₁ be Universal_Algebra;
let c₂, c₃ be SubAlgebra of c₁;
assume E19: the carrier of c₂ meets the carrier of c₃ ;
func c₂ /\ c₃ -> strict SubAlgebra of a₁ means :Def10: :: UNIALG_2:def 10
( the carrier of a₄ = the carrier of a₂ /\ the carrier of a₃ & ( for b₁ being non empty Subset of a₁ st b₁ = the carrier of a₄ holds
( the charact of a₄ = Opers a₁,b₁ & b₁ is opers_closed ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines /\ UNIALG_2:def 10 :

definition

let c₁ be Universal_Algebra;
func Constants c₁ -> Subset of a₁ equals :: UNIALG_2:def 11
{ b₁ where B is Element of a₁ : ex b₁ being operation of a₁ st
( arity b₂ = 0 & b₁ in rng b₂ ) } ;
coherence

proof end;

end;

:: deftheorem Def11 defines Constants UNIALG_2:def 11 :

definition

let c₁ be Universal_Algebra;
attr a₁ is with_const_op means :Def12: :: UNIALG_2:def 12
ex b₁ being operation of a₁ st arity b₁ = 0;

end;

:: deftheorem Def12 defines with_const_op UNIALG_2:def 12 :

registration

cluster strict with_const_op UAStr ;
existence

proof end;

end;

registration

let c₁ be with_const_op Universal_Algebra;
cluster Constants a₁ -> non empty ;
coherence

proof end;

end;

theorem Th18: :: UNIALG_2:18

for b₁ being Universal_Algebra
for b₂ being SubAlgebra of b₁ holds Constants b₁ is Subset of b₂

proof end;

theorem Th19: :: UNIALG_2:19

for b₁ being with_const_op Universal_Algebra
for b₂ being SubAlgebra of b₁ holds Constants b₁ is non empty Subset of b₂ by Th18;

theorem Th20: :: UNIALG_2:20

for b₁ being with_const_op Universal_Algebra
for b₂, b₃ being SubAlgebra of b₁ holds the carrier of b₂ meets the carrier of b₃

proof end;

definition

let c₁ be Universal_Algebra;
let c₂ be Subset of c₁;
assume E23: ( Constants c₁ <> {} or c₂ <> {} ) ;
func GenUnivAlg c₂ -> strict SubAlgebra of a₁ means :Def13: :: UNIALG_2:def 13
( a₂ c= the carrier of a₃ & ( for b₁ being SubAlgebra of a₁ st a₂ c= the carrier of b₁ holds
a₃ is SubAlgebra of b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines GenUnivAlg UNIALG_2:def 13 :

theorem Th21: :: UNIALG_2:21

for b₁ being strict Universal_Algebra holds GenUnivAlg ([#] the carrier of b₁) = b₁

proof end;

theorem Th22: :: UNIALG_2:22

for b₁ being Universal_Algebra
for b₂ being strict SubAlgebra of b₁
for b₃ being non empty Subset of b₁ st b₃ = the carrier of b₂ holds
GenUnivAlg b₃ = b₂

proof end;

definition

let c₁ be Universal_Algebra;
let c₂, c₃ be SubAlgebra of c₁;
func c₂ "\/" c₃ -> strict SubAlgebra of a₁ means :Def14: :: UNIALG_2:def 14
for b₁ being non empty Subset of a₁ st b₁ = the carrier of a₂ \/ the carrier of a₃ holds
a₄ = GenUnivAlg b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines "\/" UNIALG_2:def 14 :

theorem Th23: :: UNIALG_2:23

for b₁ being Universal_Algebra
for b₂ being SubAlgebra of b₁
for b₃, b₄ being Subset of b₁ st ( b₃ <> {} or Constants b₁ <> {} ) & b₄ = b₃ \/ the carrier of b₂ holds
(GenUnivAlg b₃) "\/" b₂ = GenUnivAlg b₄

proof end;

theorem Th24: :: UNIALG_2:24

for b₁ being Universal_Algebra
for b₂, b₃ being SubAlgebra of b₁ holds b₂ "\/" b₃ = b₃ "\/" b₂

proof end;

theorem Th25: :: UNIALG_2:25

for b₁ being with_const_op Universal_Algebra
for b₂, b₃ being strict SubAlgebra of b₁ holds b₂ /\ (b₂ "\/" b₃) = b₂

proof end;

theorem Th26: :: UNIALG_2:26

for b₁ being with_const_op Universal_Algebra
for b₂, b₃ being strict SubAlgebra of b₁ holds (b₂ /\ b₃) "\/" b₃ = b₃

proof end;

definition

let c₁ be Universal_Algebra;
func Sub c₁ -> set means :Def15: :: UNIALG_2:def 15
for b₁ being set holds
( b₁ in a₂ iff b₁ is strict SubAlgebra of a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines Sub UNIALG_2:def 15 :

registration

let c₁ be Universal_Algebra;
cluster Sub a₁ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be Universal_Algebra;
func UniAlg_join c₁ -> BinOp of Sub a₁ means :Def16: :: UNIALG_2:def 16
for b₁, b₂ being Element of Sub a₁
for b₃, b₄ being strict SubAlgebra of a₁ st b₁ = b₃ & b₂ = b₄ holds
a₂ . b₁,b₂ = b₃ "\/" b₄;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines UniAlg_join UNIALG_2:def 16 :

definition

let c₁ be Universal_Algebra;
func UniAlg_meet c₁ -> BinOp of Sub a₁ means :Def17: :: UNIALG_2:def 17
for b₁, b₂ being Element of Sub a₁
for b₃, b₄ being strict SubAlgebra of a₁ st b₁ = b₃ & b₂ = b₄ holds
a₂ . b₁,b₂ = b₃ /\ b₄;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines UniAlg_meet UNIALG_2:def 17 :

theorem Th27: :: UNIALG_2:27

for b₁ being Universal_Algebra holds UniAlg_join b₁ is commutative

proof end;

theorem Th28: :: UNIALG_2:28

for b₁ being Universal_Algebra holds UniAlg_join b₁ is associative

proof end;

theorem Th29: :: UNIALG_2:29

for b₁ being with_const_op Universal_Algebra holds UniAlg_meet b₁ is commutative

proof end;

theorem Th30: :: UNIALG_2:30

for b₁ being with_const_op Universal_Algebra holds UniAlg_meet b₁ is associative

proof end;

definition

let c₁ be with_const_op Universal_Algebra;
func UnSubAlLattice c₁ -> strict Lattice equals :: UNIALG_2:def 18
LattStr(# (Sub a₁),(UniAlg_join a₁),(UniAlg_meet a₁) #);
coherence

proof end;

end;

:: deftheorem Def18 defines UnSubAlLattice UNIALG_2:def 18 :