let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra of S holds MSAlg_join U0 is associative
let U0 be non-empty MSAlgebra of S; :: thesis: MSAlg_join U0 is associative
set o = MSAlg_join U0;
for x, y, z being Element of MSSub U0 holds (MSAlg_join U0) . x,((MSAlg_join U0) . y,z) = (MSAlg_join U0) . ((MSAlg_join U0) . x,y),z
proof
let x,
y,
z be
Element of
MSSub U0;
:: thesis: (MSAlg_join U0) . x,((MSAlg_join U0) . y,z) = (MSAlg_join U0) . ((MSAlg_join U0) . x,y),z
reconsider U1 =
x,
U2 =
y,
U3 =
z as
strict MSSubAlgebra of
U0 by Def20;
(
(MSAlg_join U0) . y,
z = U2 "\/" U3 &
(MSAlg_join U0) . x,
y = U1 "\/" U2 )
by Def21;
then A1:
(
(MSAlg_join U0) . x,
((MSAlg_join U0) . y,z) = U1 "\/" (U2 "\/" U3) &
(MSAlg_join U0) . ((MSAlg_join U0) . x,y),
z = (U1 "\/" U2) "\/" U3 )
by Def21;
set B = the
Sorts of
U1 \/ (the Sorts of U2 \/ the Sorts of U3);
( the
Sorts of
U1 is
MSSubset of
U0 & the
Sorts of
U2 is
MSSubset of
U0 & the
Sorts of
U3 is
MSSubset of
U0 )
by Def10;
then A2:
( the
Sorts of
U1 c= the
Sorts of
U0 & the
Sorts of
U2 c= the
Sorts of
U0 & the
Sorts of
U3 c= the
Sorts of
U0 )
by PBOOLE:def 23;
then A3:
the
Sorts of
U2 \/ the
Sorts of
U3 c= the
Sorts of
U0
by PBOOLE:18;
A4:
the
Sorts of
U1 \/ the
Sorts of
U2 c= the
Sorts of
U0
by A2, PBOOLE:18;
reconsider C = the
Sorts of
U2 \/ the
Sorts of
U3 as
MSSubset of
U0 by A3, PBOOLE:def 23;
reconsider D = the
Sorts of
U1 \/ the
Sorts of
U2 as
MSSubset of
U0 by A4, PBOOLE:def 23;
the
Sorts of
U1 \/ (the Sorts of U2 \/ the Sorts of U3) c= the
Sorts of
U0
by A2, A3, PBOOLE:18;
then reconsider B = the
Sorts of
U1 \/ (the Sorts of U2 \/ the Sorts of U3) as
MSSubset of
U0 by PBOOLE:def 23;
A5:
U1 "\/" (U2 "\/" U3) =
U1 "\/" (GenMSAlg C)
by Def19
.=
(GenMSAlg C) "\/" U1
by Th27
.=
GenMSAlg B
by Th25
;
A6:
B = D \/ the
Sorts of
U3
by PBOOLE:34;
(U1 "\/" U2) "\/" U3 =
(GenMSAlg D) "\/" U3
by Def19
.=
GenMSAlg B
by A6, Th25
;
hence
(MSAlg_join U0) . x,
((MSAlg_join U0) . y,z) = (MSAlg_join U0) . ((MSAlg_join U0) . x,y),
z
by A1, A5;
:: thesis: verum
end;
hence
MSAlg_join U0 is associative
by BINOP_1:def 3; :: thesis: verum