let Z be with_const_op Universal_Algebra; :: thesis: 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:7;
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:16;
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
let a1,
b1 be
Element of
(UnSubAlLattice UAStr(# the carrier of Z,the charact of Z #));
:: according to LATTICE4:def 1 :: thesis: ( f . (a1 "\/" b1) = (f . a1) "\/" (f . b1) & 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 15;
reconsider s =
a3 "\/" b3 as
Element of
Sub UAStr(# the
carrier of
Z,the
charact of
Z #)
by UNIALG_2:def 15;
consider A1 being
strict non-empty SubAlgebra of
UAStr(# the
carrier of
Z,the
charact of
Z #)
such that A4:
(
A1 = s &
f . s = MSAlg A1 )
by A3;
consider A3 being
strict non-empty SubAlgebra of
UAStr(# the
carrier of
Z,the
charact of
Z #)
such that A5:
(
A3 = a3 &
f . a3 = MSAlg A3 )
by A3;
consider A4 being
strict non-empty SubAlgebra of
UAStr(# the
carrier of
Z,the
charact of
Z #)
such that A6:
(
A4 = b3 &
f . b3 = MSAlg A4 )
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;
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;
A7:
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 16
.=
g4 "\/" g3
by A5, A6, Th30
.=
the
L_join of
(MSSubAlLattice (MSAlg UAStr(# the carrier of Z,the charact of Z #))) . (f . a1),
(f . b1)
by A5, A6, MSUALG_2:def 21
.=
(f . a1) "\/" (f . b1)
by LATTICES:def 1
;
reconsider m =
a3 /\ b3 as
Element of
Sub UAStr(# the
carrier of
Z,the
charact of
Z #)
by UNIALG_2:def 15;
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;
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 A1 being
strict non-empty SubAlgebra of
UAStr(# the
carrier of
Z,the
charact of
Z #)
such that A8:
(
A1 = m &
f . m = MSAlg A1 )
by A3;
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 A8, UNIALG_2:def 17
.=
g1 /\ g2
by Th31
.=
the
L_meet of
(MSSubAlLattice (MSAlg UAStr(# the carrier of Z,the charact of Z #))) . (f . a1),
(f . b1)
by A5, A6, MSUALG_2:def 22
.=
(f . a1) "/\" (f . b1)
by LATTICES:def 2
;
hence
(
f . (a1 "\/" b1) = (f . a1) "\/" (f . b1) &
f . (a1 "/\" b1) = (f . a1) "/\" (f . b1) )
by A7;
:: thesis: 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
; :: according to LATTICE4:def 5 :: thesis: f is V15(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 #))))
A9:
dom f = Sub UAStr(# the carrier of Z,the charact of Z #)
by FUNCT_2:def 1;
thus
f is one-to-one
:: according to FUNCT_2:def 4 :: thesis: f is V14(the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z,the charact of Z #))))proof
now let x1,
x2 be
set ;
:: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )assume that A10:
x1 in dom f
and A11:
x2 in dom f
and A12:
f . x1 = f . x2
;
:: thesis: x1 = x2reconsider y1 =
x1,
y2 =
x2 as
Element of
Sub UAStr(# the
carrier of
Z,the
charact of
Z #)
by A10, 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 &
f . y1 = MSAlg A1 )
by A3;
consider A2 being
strict SubAlgebra of
UAStr(# the
carrier of
Z,the
charact of
Z #)
such that A14:
(
A2 = y2 &
f . y2 = MSAlg A2 )
by A3;
A15:
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:15
.=
x2
by A12, A13, A14, A15, MSUALG_1:15
;
:: thesis: verum end;
hence
f is
one-to-one
by FUNCT_1:def 8;
:: thesis: verum
end;
thus
rng f = the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z,the charact of Z #)))
:: according to FUNCT_2:def 3 :: thesis: verumproof
thus
rng f c= the
carrier of
(MSSubAlLattice (MSAlg UAStr(# the carrier of Z,the charact of Z #)))
by RELAT_1:def 19;
:: according to XBOOLE_0:def 10 :: thesis: the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z,the charact of Z #))) c= rng f
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( 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 #)))
;
:: thesis: 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 20;
reconsider C =
Constants (MSAlg UAStr(# the carrier of Z,the charact of Z #)) as
MSSubset of
y by MSUALG_2:11;
(
C c= the
Sorts of
y &
C is
non-empty )
by PBOOLE:def 23;
then
the
Sorts of
y is
non-empty
by PBOOLE:143;
then reconsider y =
y as
strict non-empty MSSubAlgebra of
MSAlg UAStr(# the
carrier of
Z,the
charact of
Z #)
by MSUALG_1:def 8;
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:15;
then reconsider y1 =
1-Alg y as
Element of
Sub UAStr(# the
carrier of
Z,the
charact of
Z #)
by UNIALG_2:def 15;
A16:
y1 in dom f
by A9;
consider A1 being
strict SubAlgebra of
UAStr(# the
carrier of
Z,the
charact of
Z #)
such that A17:
(
A1 = y1 &
f . y1 = MSAlg A1 )
by A3;
f . (1-Alg y) = x
by A1, A17, Th26;
hence
x in rng f
by A16, FUNCT_1:def 5;
:: thesis: verum
end;
thus
verum
; :: thesis: verum