let S1 be OrderSortedSign; for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is associative
let U0 be non-empty OSAlgebra of S1; OSAlg_join U0 is associative
set o = OSAlg_join U0;
for x, y, z being Element of OSSub U0 holds (OSAlg_join U0) . (x,((OSAlg_join U0) . (y,z))) = (OSAlg_join U0) . (((OSAlg_join U0) . (x,y)),z)
proof
let x,
y,
z be
Element of
OSSub U0;
(OSAlg_join U0) . (x,((OSAlg_join U0) . (y,z))) = (OSAlg_join U0) . (((OSAlg_join U0) . (x,y)),z)
reconsider U1 =
x,
U2 =
y,
U3 =
z as
strict OSSubAlgebra of
U0 by Def14;
set B = the
Sorts of
U1 (\/) ( the Sorts of U2 (\/) the Sorts of U3);
A1:
the
Sorts of
U2 is
OrderSortedSet of
S1
by OSALG_1:17;
the
Sorts of
U2 is
MSSubset of
U0
by MSUALG_2:def 9;
then A2:
the
Sorts of
U2 c= the
Sorts of
U0
by PBOOLE:def 18;
the
Sorts of
U3 is
MSSubset of
U0
by MSUALG_2:def 9;
then
the
Sorts of
U3 c= the
Sorts of
U0
by PBOOLE:def 18;
then A3:
the
Sorts of
U2 (\/) the
Sorts of
U3 c= the
Sorts of
U0
by A2, PBOOLE:16;
then reconsider C1 = the
Sorts of
U2 (\/) the
Sorts of
U3 as
MSSubset of
U0 by PBOOLE:def 18;
the
Sorts of
U3 is
OrderSortedSet of
S1
by OSALG_1:17;
then A4:
the
Sorts of
U2 (\/) the
Sorts of
U3 is
OrderSortedSet of
S1
by A1, Th2;
then reconsider C =
C1 as
OSSubset of
U0 by Def2;
A5:
the
Sorts of
U1 is
OrderSortedSet of
S1
by OSALG_1:17;
then A6:
the
Sorts of
U1 (\/) ( the Sorts of U2 (\/) the Sorts of U3) is
OrderSortedSet of
S1
by A4, Th2;
the
Sorts of
U1 is
MSSubset of
U0
by MSUALG_2:def 9;
then A7:
the
Sorts of
U1 c= the
Sorts of
U0
by PBOOLE:def 18;
then
the
Sorts of
U1 (\/) the
Sorts of
U2 c= the
Sorts of
U0
by A2, PBOOLE:16;
then reconsider D1 = the
Sorts of
U1 (\/) the
Sorts of
U2 as
MSSubset of
U0 by PBOOLE:def 18;
(OSAlg_join U0) . (
y,
z)
= U2 "\/"_os U3
by Def15;
then A8:
(OSAlg_join U0) . (
x,
((OSAlg_join U0) . (y,z)))
= U1 "\/"_os (U2 "\/"_os U3)
by Def15;
the
Sorts of
U1 (\/) the
Sorts of
U2 is
OrderSortedSet of
S1
by A5, A1, Th2;
then reconsider D =
D1 as
OSSubset of
U0 by Def2;
A9:
(OSAlg_join U0) . (
x,
y)
= U1 "\/"_os U2
by Def15;
the
Sorts of
U1 (\/) ( the Sorts of U2 (\/) the Sorts of U3) c= the
Sorts of
U0
by A7, A3, PBOOLE:16;
then
the
Sorts of
U1 (\/) ( the Sorts of U2 (\/) the Sorts of U3) is
MSSubset of
U0
by PBOOLE:def 18;
then reconsider B = the
Sorts of
U1 (\/) ( the Sorts of U2 (\/) the Sorts of U3) as
OSSubset of
U0 by A6, Def2;
A10:
B = D (\/) the
Sorts of
U3
by PBOOLE:28;
A11:
(U1 "\/"_os U2) "\/"_os U3 =
(GenOSAlg D) "\/"_os U3
by Def13
.=
GenOSAlg B
by A10, Th37
;
U1 "\/"_os (U2 "\/"_os U3) =
U1 "\/"_os (GenOSAlg C)
by Def13
.=
(GenOSAlg C) "\/"_os U1
by Th39
.=
GenOSAlg B
by Th37
;
hence
(OSAlg_join U0) . (
x,
((OSAlg_join U0) . (y,z)))
= (OSAlg_join U0) . (
((OSAlg_join U0) . (x,y)),
z)
by A9, A8, A11, Def15;
verum
end;
hence
OSAlg_join U0 is associative
by BINOP_1:def 3; verum