let A be strict Universal_Algebra; :: thesis: 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
let a1, b1 be strict non-empty SubAlgebra of A; :: thesis: for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
MSAlg (a1 "\/" b1) = a2 "\/" b2
let a2, b2 be strict non-empty MSSubAlgebra of MSAlg A; :: thesis: ( a2 = MSAlg a1 & b2 = MSAlg b1 implies MSAlg (a1 "\/" b1) = a2 "\/" b2 )
assume A1:
( a2 = MSAlg a1 & b2 = MSAlg b1 )
; :: thesis: MSAlg (a1 "\/" b1) = a2 "\/" b2
reconsider MSA = MSAlg (a1 "\/" b1) as MSSubAlgebra of MSAlg A by Th12;
MSSign (a1 "\/" b1) = MSSign A
by Th7;
then reconsider MSA = MSA as strict non-empty MSSubAlgebra of MSAlg A ;
for B being MSSubset of (MSAlg A) st B = the Sorts of a2 \/ the Sorts of b2 holds
MSA = GenMSAlg B
proof
let B be
MSSubset of
(MSAlg A);
:: thesis: ( B = the Sorts of a2 \/ the Sorts of b2 implies MSA = GenMSAlg B )
assume A2:
B = the
Sorts of
a2 \/ the
Sorts of
b2
;
:: thesis: MSA = GenMSAlg B
set X =
MSA;
MSA = MSAlgebra(#
(MSSorts (a1 "\/" b1)),
(MSCharact (a1 "\/" b1)) #)
by MSUALG_1:def 16;
then A3:
the
Sorts of
MSA = 0 .--> the
carrier of
(a1 "\/" b1)
by MSUALG_1:def 14;
reconsider ff1 =
(*--> 0 ) * (signature A) as
Function of
(dom (signature A)),
({0 } * ) by MSUALG_1:7;
A4:
MSSign A = ManySortedSign(#
{0 },
(dom (signature A)),
ff1,
((dom (signature A)) --> z) #)
by MSUALG_1:16;
A5:
the
carrier of
a1 is
Subset of
A
by UNIALG_2:def 8;
the
carrier of
b1 is
Subset of
A
by UNIALG_2:def 8;
then reconsider K = the
carrier of
a1 \/ the
carrier of
b1 as non
empty Subset of
A by A5, XBOOLE_1:8;
reconsider M1 = the
Sorts of
MSA as
ManySortedSet of ;
reconsider x =
0 as
Element of
(MSSign A) by A4;
A6:
B is
MSSubset of
MSA
for
U1 being
MSSubAlgebra of
MSAlg A st
B is
MSSubset of
U1 holds
MSA is
MSSubAlgebra of
U1
proof
let U1 be
MSSubAlgebra of
MSAlg A;
:: thesis: ( B is MSSubset of U1 implies MSA is MSSubAlgebra of U1 )
assume A10:
B is
MSSubset of
U1
;
:: thesis: MSA is MSSubAlgebra of U1
per cases
( U1 is non-empty or not U1 is non-empty )
;
suppose
U1 is
non-empty
;
:: thesis: MSA is MSSubAlgebra of U1then reconsider U11 =
U1 as
non-empty MSSubAlgebra of
MSAlg A ;
A11:
1-Alg U11 is
SubAlgebra of
1-Alg (MSAlg A)
by Th20;
then
1-Alg U11 is
SubAlgebra of
A
by MSUALG_1:15;
then A12:
MSSign A = MSSign (1-Alg U11)
by Th7;
B c= the
Sorts of
U11
by A10, PBOOLE:def 23;
then A13:
B . x c= the
Sorts of
U11 . x
by PBOOLE:def 5;
A14:
MSAlgebra(# the
Sorts of
U11,the
Charact of
U11 #)
= MSAlg (1-Alg U11)
by A4, Th26;
MSAlg (1-Alg U11) = MSAlgebra(#
(MSSorts (1-Alg U11)),
(MSCharact (1-Alg U11)) #)
by MSUALG_1:def 16;
then A15:
the
Sorts of
U11 . 0 = (0 .--> the carrier of (1-Alg U11)) . 0
by A14, MSUALG_1:def 14;
A16:
B . 0 =
(0 .--> K) . 0
by A1, A2, Th28
.=
K
by FUNCOP_1:87
;
reconsider A1 =
1-Alg U11 as
strict SubAlgebra of
A by A11, MSUALG_1:15;
the
carrier of
a1 \/ the
carrier of
b1 c= the
carrier of
A1
by A13, A15, A16, FUNCOP_1:87;
then
GenUnivAlg K is
SubAlgebra of
1-Alg U11
by UNIALG_2:def 13;
then
a1 "\/" b1 is
SubAlgebra of
1-Alg U11
by UNIALG_2:def 14;
then
MSA is
MSSubAlgebra of
MSAlg (1-Alg U11)
by Th12;
then
MSA is
MSSubAlgebra of
MSAlgebra(# the
Sorts of
U11,the
Charact of
U11 #)
by A4, A12, Th26;
hence
MSA is
MSSubAlgebra of
U1
by Th21;
:: thesis: verum end; suppose
not
U1 is
non-empty
;
:: thesis: MSA is MSSubAlgebra of U1then
not the
Sorts of
U1 is
non-empty
by MSUALG_1:def 8;
then consider i being
set such that A17:
i in the
carrier of
(MSSign A)
and A18:
the
Sorts of
U1 . i is
empty
by PBOOLE:def 16;
B c= the
Sorts of
U1
by A10, PBOOLE:def 23;
then A19:
B . x c= the
Sorts of
U1 . x
by PBOOLE:def 5;
consider e being
Element of
a1;
dom ({0 } --> the carrier of a1) = {0 }
by FUNCOP_1:19;
then reconsider 0a1 =
0 .--> the
carrier of
a1 as
ManySortedSet of
by A4, PARTFUN1:def 4;
a2 = MSAlgebra(#
(MSSorts a1),
(MSCharact a1) #)
by A1, MSUALG_1:def 16;
then
B = 0a1 \/ the
Sorts of
b2
by A2, MSUALG_1:def 14;
then A20:
B . x = (0a1 . x) \/ (the Sorts of b2 . x)
by PBOOLE:def 7;
x in {0 }
by TARSKI:def 1;
then
0a1 . x = the
carrier of
a1
by FUNCOP_1:13;
then
e in B . x
by A20, XBOOLE_0:def 3;
hence
MSA is
MSSubAlgebra of
U1
by A4, A17, A18, A19, TARSKI:def 1;
:: thesis: verum end;
end;
hence
MSA = GenMSAlg B
by A6, MSUALG_2:def 18;
:: thesis: verum
end;
hence
MSAlg (a1 "\/" b1) = a2 "\/" b2
by MSUALG_2:def 19; :: thesis: verum