:: by Adam Naumowicz and Agnieszka Julia Marasik

::

:: Received September 22, 1998

:: Copyright (c) 1998-2019 Association of Mizar Users

reconsider z = 0 as Element of {0} by TARSKI:def 1;

theorem Th8: :: MSSUBLAT:8

for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds

for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds

for o being OperSymbol of (MSSign U2)

for a being OperSymbol of (MSSign U1) st a = o holds

Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1)))

for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds

for o being OperSymbol of (MSSign U2)

for a being OperSymbol of (MSSign U1) st a = o holds

Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1)))

proof end;

theorem Th9: :: MSSUBLAT:9

for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds

the Sorts of (MSAlg U1) is MSSubset of (MSAlg U2)

the Sorts of (MSAlg U1) is MSSubset of (MSAlg U2)

proof end;

theorem Th10: :: MSSUBLAT:10

for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds

for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds

B is opers_closed

for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds

B is opers_closed

proof end;

theorem Th11: :: MSSUBLAT:11

for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds

for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds

the Charact of (MSAlg U1) = Opers ((MSAlg U2),B)

for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds

the Charact of (MSAlg U1) = Opers ((MSAlg U2),B)

proof end;

theorem Th12: :: MSSUBLAT:12

for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds

MSAlg U1 is MSSubAlgebra of MSAlg U2

MSAlg U1 is MSSubAlgebra of MSAlg U2

proof end;

theorem Th13: :: MSSUBLAT:13

for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds

the carrier of U1 is Subset of U2

the carrier of U1 is Subset of U2

proof end;

theorem Th14: :: MSSUBLAT:14

for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds

for B being non empty Subset of U2 st B = the carrier of U1 holds

B is opers_closed

for B being non empty Subset of U2 st B = the carrier of U1 holds

B is opers_closed

proof end;

theorem Th15: :: MSSUBLAT:15

for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds

for B being non empty Subset of U2 st B = the carrier of U1 holds

the charact of U1 = Opers (U2,B)

for B being non empty Subset of U2 st B = the carrier of U1 holds

the charact of U1 = Opers (U2,B)

proof end;

theorem Th16: :: MSSUBLAT:16

for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds

U1 is SubAlgebra of U2

U1 is SubAlgebra of U2

proof end;

theorem Th17: :: MSSUBLAT:17

for MS being non void 1 -element segmental ManySortedSign

for A being non-empty MSAlgebra over MS

for B being non-empty MSSubAlgebra of A holds the carrier of (1-Alg B) is Subset of (1-Alg A)

for A being non-empty MSAlgebra over MS

for B being non-empty MSSubAlgebra of A holds the carrier of (1-Alg B) is Subset of (1-Alg A)

proof end;

theorem Th18: :: MSSUBLAT:18

for MS being non void 1 -element segmental ManySortedSign

for A being non-empty MSAlgebra over MS

for B being non-empty MSSubAlgebra of A

for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds

S is opers_closed

for A being non-empty MSAlgebra over MS

for B being non-empty MSSubAlgebra of A

for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds

S is opers_closed

proof end;

theorem Th19: :: MSSUBLAT:19

for MS being non void 1 -element segmental ManySortedSign

for A being non-empty MSAlgebra over MS

for B being non-empty MSSubAlgebra of A

for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds

the charact of (1-Alg B) = Opers ((1-Alg A),S)

for A being non-empty MSAlgebra over MS

for B being non-empty MSSubAlgebra of A

for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds

the charact of (1-Alg B) = Opers ((1-Alg A),S)

proof end;

theorem Th20: :: MSSUBLAT:20

for MS being non void 1 -element segmental ManySortedSign

for A being non-empty MSAlgebra over MS

for B being non-empty MSSubAlgebra of A holds 1-Alg B is SubAlgebra of 1-Alg A

for A being non-empty MSAlgebra over MS

for B being non-empty MSSubAlgebra of A holds 1-Alg B is SubAlgebra of 1-Alg A

proof end;

theorem Th21: :: MSSUBLAT:21

for S being non empty non void ManySortedSign

for A, B being MSAlgebra over S holds

( A is MSSubAlgebra of B iff A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) )

for A, B being MSAlgebra over S holds

( A is MSSubAlgebra of B iff A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) )

proof end;

theorem Th23: :: MSSUBLAT:23

for MS being non void 1 -element segmental ManySortedSign

for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds

MSSign (1-Alg A) = ManySortedSign(# the carrier of MS, the carrier' of MS, the Arity of MS, the ResultSort of MS #)

for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds

MSSign (1-Alg A) = ManySortedSign(# the carrier of MS, the carrier' of MS, the Arity of MS, the ResultSort of MS #)

proof end;

theorem Th24: :: MSSUBLAT:24

for MS being non void 1 -element segmental ManySortedSign

for A, B being non-empty MSAlgebra over MS st 1-Alg A = 1-Alg B holds

MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)

for A, B being non-empty MSAlgebra over MS st 1-Alg A = 1-Alg B holds

MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)

proof end;

theorem :: MSSUBLAT:25

for MS being non void 1 -element segmental ManySortedSign

for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds

the Sorts of A = the Sorts of (MSAlg (1-Alg A))

for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds

the Sorts of A = the Sorts of (MSAlg (1-Alg A))

proof end;

theorem Th26: :: MSSUBLAT:26

for MS being non void 1 -element segmental ManySortedSign

for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds

MSAlg (1-Alg A) = MSAlgebra(# the Sorts of A, the Charact of A #)

for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds

MSAlg (1-Alg A) = MSAlgebra(# the Sorts of A, the Charact of A #)

proof end;

theorem :: MSSUBLAT:27

for A being Universal_Algebra

for B being strict non-empty MSSubAlgebra of MSAlg A st the carrier of (MSSign A) = {0} holds

1-Alg B is SubAlgebra of A

for B being strict non-empty MSSubAlgebra of MSAlg A st the carrier of (MSSign A) = {0} holds

1-Alg B is SubAlgebra of A

proof end;

theorem Th28: :: MSSUBLAT:28

for A being Universal_Algebra

for a1, b1 being strict SubAlgebra of A

for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds

the Sorts of a2 (\/) the Sorts of b2 = 0 .--> ( the carrier of a1 \/ the carrier of b1)

for a1, b1 being strict SubAlgebra of A

for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds

the Sorts of a2 (\/) the Sorts of b2 = 0 .--> ( the carrier of a1 \/ the carrier of b1)

proof end;

theorem Th29: :: MSSUBLAT:29

for A being Universal_Algebra

for a1, b1 being strict non-empty SubAlgebra of A

for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds

the Sorts of a2 (/\) the Sorts of b2 = 0 .--> ( the carrier of a1 /\ the carrier of b1)

for a1, b1 being strict non-empty SubAlgebra of A

for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds

the Sorts of a2 (/\) the Sorts of b2 = 0 .--> ( the carrier of a1 /\ the carrier of b1)

proof end;

theorem Th30: :: MSSUBLAT:30

for A being strict Universal_Algebra

for a1, b1 being strict non-empty SubAlgebra of A

for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds

MSAlg (a1 "\/" b1) = a2 "\/" b2

for a1, b1 being strict non-empty SubAlgebra of A

for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds

MSAlg (a1 "\/" b1) = a2 "\/" b2

proof end;

registration

let A be with_const_op Universal_Algebra;

coherence

( not MSSign A is void & MSSign A is strict & MSSign A is segmental & MSSign A is trivial & MSSign A is all-with_const_op )

end;
coherence

( not MSSign A is void & MSSign A is strict & MSSign A is segmental & MSSign A is trivial & MSSign A is all-with_const_op )

proof end;

theorem Th31: :: MSSUBLAT:31

for A being with_const_op Universal_Algebra

for a1, b1 being strict non-empty SubAlgebra of A

for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds

MSAlg (a1 /\ b1) = a2 /\ b2

for a1, b1 being strict non-empty SubAlgebra of A

for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds

MSAlg (a1 /\ b1) = a2 /\ b2

proof end;

registration

let A be quasi_total UAStr ;

coherence

UAStr(# the carrier of A, the charact of A #) is quasi_total ;

end;
coherence

UAStr(# the carrier of A, the charact of A #) is quasi_total ;

registration
end;

registration
end;

registration

let A be with_const_op Universal_Algebra;

coherence

UAStr(# the carrier of A, the charact of A #) is with_const_op

end;
coherence

UAStr(# the carrier of A, the charact of A #) is with_const_op

proof end;

theorem :: MSSUBLAT:32

for A being with_const_op Universal_Algebra holds UnSubAlLattice UAStr(# the carrier of A, the charact of A #), MSSubAlLattice (MSAlg UAStr(# the carrier of A, the charact of A #)) are_isomorphic

proof end;

:: Universal and Many Sorted Algebras