let Z be with_const_op Universal_Algebra; UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #), MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)) are_isomorphic
set A = UAStr(# the carrier of Z, the charact of Z #);
reconsider ff1 = (*--> 0) * (signature UAStr(# the carrier of Z, the charact of Z #)) as Function of (dom (signature UAStr(# the carrier of Z, the charact of Z #))),({0} *) by MSUALG_1:2;
A1:
MSSign UAStr(# the carrier of Z, the charact of Z #) = ManySortedSign(# {0},(dom (signature UAStr(# the carrier of Z, the charact of Z #))),ff1,((dom (signature UAStr(# the carrier of Z, the charact of Z #))) --> z) #)
by MSUALG_1:10;
defpred S1[ set , set ] means ex A1 being strict SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) st
( A1 = $1 & $2 = MSAlg A1 );
A2:
for x being Element of Sub UAStr(# the carrier of Z, the charact of Z #) ex y being Element of MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)) st S1[x,y]
consider f being Function of (Sub UAStr(# the carrier of Z, the charact of Z #)),(MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #))) such that
A3:
for x being Element of Sub UAStr(# the carrier of Z, the charact of Z #) holds S1[x,f . x]
from FUNCT_2:sch 3(A2);
reconsider f = f as Function of the carrier of (UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #)), the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) ;
f is Homomorphism of (UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #)),(MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))
proof
AA:
f is
"\/"-preserving
proof
let a1,
b1 be
Element of
(UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #));
LATTICE4:def 1 f . (a1 "\/" b1) = (f . a1) "\/" (f . b1)
reconsider a2 =
a1,
b2 =
b1 as
Element of
Sub UAStr(# the
carrier of
Z, the
charact of
Z #) ;
reconsider a3 =
a2,
b3 =
b2 as
strict non-empty SubAlgebra of
UAStr(# the
carrier of
Z, the
charact of
Z #)
by UNIALG_2:def 14;
reconsider s =
a3 "\/" b3 as
Element of
Sub UAStr(# the
carrier of
Z, the
charact of
Z #)
by UNIALG_2:def 14;
reconsider m =
a3 /\ b3 as
Element of
Sub UAStr(# the
carrier of
Z, the
charact of
Z #)
by UNIALG_2:def 14;
A4:
ex
A1 being
strict non-empty SubAlgebra of
UAStr(# the
carrier of
Z, the
charact of
Z #) st
(
A1 = s &
f . s = MSAlg A1 )
by A3;
MSSign b3 = MSSign UAStr(# the
carrier of
Z, the
charact of
Z #)
by Th7;
then reconsider g2 =
MSAlg b3 as
strict non-empty MSSubAlgebra of
MSAlg UAStr(# the
carrier of
Z, the
charact of
Z #)
by Th12;
consider A4 being
strict non-empty SubAlgebra of
UAStr(# the
carrier of
Z, the
charact of
Z #)
such that A5:
A4 = b3
and A6:
f . b3 = MSAlg A4
by A3;
MSSign A4 = MSSign UAStr(# the
carrier of
Z, the
charact of
Z #)
by Th7;
then reconsider g3 =
MSAlg A4 as
strict non-empty MSSubAlgebra of
MSAlg UAStr(# the
carrier of
Z, the
charact of
Z #)
by Th12;
MSSign a3 = MSSign UAStr(# the
carrier of
Z, the
charact of
Z #)
by Th7;
then reconsider g1 =
MSAlg a3 as
strict non-empty MSSubAlgebra of
MSAlg UAStr(# the
carrier of
Z, the
charact of
Z #)
by Th12;
consider A3 being
strict non-empty SubAlgebra of
UAStr(# the
carrier of
Z, the
charact of
Z #)
such that A7:
A3 = a3
and A8:
f . a3 = MSAlg A3
by A3;
MSSign A3 = MSSign UAStr(# the
carrier of
Z, the
charact of
Z #)
by Th7;
then reconsider g4 =
MSAlg A3 as
strict non-empty MSSubAlgebra of
MSAlg UAStr(# the
carrier of
Z, the
charact of
Z #)
by Th12;
thus f . (a1 "\/" b1) =
f . ((UniAlg_join UAStr(# the carrier of Z, the charact of Z #)) . (a2,b2))
by LATTICES:def 1
.=
MSAlg (a3 "\/" b3)
by A4, UNIALG_2:def 15
.=
g4 "\/" g3
by A7, A5, Th30
.=
the
L_join of
(MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) . (
(f . a1),
(f . b1))
by A8, A6, MSUALG_2:def 20
.=
(f . a1) "\/" (f . b1)
by LATTICES:def 1
;
verum
end;
f is
"/\"-preserving
proof
let a1,
b1 be
Element of
(UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #));
LATTICE4:def 2 f . (a1 "/\" b1) = (f . a1) "/\" (f . b1)
reconsider a2 =
a1,
b2 =
b1 as
Element of
Sub UAStr(# the
carrier of
Z, the
charact of
Z #) ;
reconsider a3 =
a2,
b3 =
b2 as
strict non-empty SubAlgebra of
UAStr(# the
carrier of
Z, the
charact of
Z #)
by UNIALG_2:def 14;
reconsider s =
a3 "\/" b3 as
Element of
Sub UAStr(# the
carrier of
Z, the
charact of
Z #)
by UNIALG_2:def 14;
reconsider m =
a3 /\ b3 as
Element of
Sub UAStr(# the
carrier of
Z, the
charact of
Z #)
by UNIALG_2:def 14;
MSSign b3 = MSSign UAStr(# the
carrier of
Z, the
charact of
Z #)
by Th7;
then reconsider g2 =
MSAlg b3 as
strict non-empty MSSubAlgebra of
MSAlg UAStr(# the
carrier of
Z, the
charact of
Z #)
by Th12;
consider A4 being
strict non-empty SubAlgebra of
UAStr(# the
carrier of
Z, the
charact of
Z #)
such that A5:
A4 = b3
and A6:
f . b3 = MSAlg A4
by A3;
MSSign A4 = MSSign UAStr(# the
carrier of
Z, the
charact of
Z #)
by Th7;
then reconsider g3 =
MSAlg A4 as
strict non-empty MSSubAlgebra of
MSAlg UAStr(# the
carrier of
Z, the
charact of
Z #)
by Th12;
MSSign a3 = MSSign UAStr(# the
carrier of
Z, the
charact of
Z #)
by Th7;
then reconsider g1 =
MSAlg a3 as
strict non-empty MSSubAlgebra of
MSAlg UAStr(# the
carrier of
Z, the
charact of
Z #)
by Th12;
consider A3 being
strict non-empty SubAlgebra of
UAStr(# the
carrier of
Z, the
charact of
Z #)
such that A7:
A3 = a3
and A8:
f . a3 = MSAlg A3
by A3;
MSSign A3 = MSSign UAStr(# the
carrier of
Z, the
charact of
Z #)
by Th7;
then reconsider g4 =
MSAlg A3 as
strict non-empty MSSubAlgebra of
MSAlg UAStr(# the
carrier of
Z, the
charact of
Z #)
by Th12;
A9:
ex
A1 being
strict non-empty SubAlgebra of
UAStr(# the
carrier of
Z, the
charact of
Z #) st
(
A1 = m &
f . m = MSAlg A1 )
by A3;
thus f . (a1 "/\" b1) =
f . ((UniAlg_meet UAStr(# the carrier of Z, the charact of Z #)) . (a2,b2))
by LATTICES:def 2
.=
MSAlg (a3 /\ b3)
by A9, UNIALG_2:def 16
.=
g1 /\ g2
by Th31
.=
the
L_meet of
(MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) . (
(f . a1),
(f . b1))
by A7, A8, A5, A6, MSUALG_2:def 21
.=
(f . a1) "/\" (f . b1)
by LATTICES:def 2
;
verum
end;
hence
f is
Homomorphism of
(UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #)),
(MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))
by AA;
verum
end;
then reconsider f = f as Homomorphism of (UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #)),(MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) ;
take
f
; LATTICE4:def 3 f is bijective
now for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2let x1,
x2 be
object ;
( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )assume that A11:
(
x1 in dom f &
x2 in dom f )
and A12:
f . x1 = f . x2
;
x1 = x2reconsider y1 =
x1,
y2 =
x2 as
Element of
Sub UAStr(# the
carrier of
Z, the
charact of
Z #)
by A11, FUNCT_2:def 1;
consider A1 being
strict SubAlgebra of
UAStr(# the
carrier of
Z, the
charact of
Z #)
such that A13:
A1 = y1
and A14:
f . y1 = MSAlg A1
by A3;
consider A2 being
strict SubAlgebra of
UAStr(# the
carrier of
Z, the
charact of
Z #)
such that A15:
(
A2 = y2 &
f . y2 = MSAlg A2 )
by A3;
A16:
MSSign A1 =
MSSign UAStr(# the
carrier of
Z, the
charact of
Z #)
by Th7
.=
MSSign A2
by Th7
;
thus x1 =
1-Alg (MSAlg A1)
by A13, MSUALG_1:9
.=
x2
by A12, A14, A15, A16, MSUALG_1:9
;
verum end;
hence
f is one-to-one
by FUNCT_1:def 4; FUNCT_2:def 4 f is onto
A17:
dom f = Sub UAStr(# the carrier of Z, the charact of Z #)
by FUNCT_2:def 1;
thus
rng f = the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))
FUNCT_2:def 3 verumproof
thus
rng f c= the
carrier of
(MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))
by RELAT_1:def 19;
XBOOLE_0:def 10 the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) c= rng f
let x be
object ;
TARSKI:def 3 ( not x in the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) or x in rng f )
assume
x in the
carrier of
(MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))
;
x in rng f
then reconsider y =
x as
strict MSSubAlgebra of
MSAlg UAStr(# the
carrier of
Z, the
charact of
Z #)
by MSUALG_2:def 19;
reconsider C =
Constants (MSAlg UAStr(# the carrier of Z, the charact of Z #)) as
MSSubset of
y by MSUALG_2:10;
C c= the
Sorts of
y
by PBOOLE:def 18;
then
the
Sorts of
y is
V2()
by PBOOLE:131;
then reconsider y =
y as
strict non-empty MSSubAlgebra of
MSAlg UAStr(# the
carrier of
Z, the
charact of
Z #)
by MSUALG_1:def 3;
1-Alg y is
SubAlgebra of
1-Alg (MSAlg UAStr(# the carrier of Z, the charact of Z #))
by Th20;
then
1-Alg y is
SubAlgebra of
UAStr(# the
carrier of
Z, the
charact of
Z #)
by MSUALG_1:9;
then reconsider y1 =
1-Alg y as
Element of
Sub UAStr(# the
carrier of
Z, the
charact of
Z #)
by UNIALG_2:def 14;
ex
A1 being
strict SubAlgebra of
UAStr(# the
carrier of
Z, the
charact of
Z #) st
(
A1 = y1 &
f . y1 = MSAlg A1 )
by A3;
then A18:
f . (1-Alg y) = x
by A1, Th26;
y1 in dom f
by A17;
hence
x in rng f
by A18, FUNCT_1:def 3;
verum
end;