let S1 be OrderSortedSign; :: thesis: for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is associative
let U0 be non-empty OSAlgebra of S1; :: thesis: 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;
:: thesis: (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 Def15;
(
(OSAlg_join U0) . y,
z = U2 "\/"_os U3 &
(OSAlg_join U0) . x,
y = U1 "\/"_os U2 )
by Def16;
then A1:
(
(OSAlg_join U0) . x,
((OSAlg_join U0) . y,z) = U1 "\/"_os (U2 "\/"_os U3) &
(OSAlg_join U0) . ((OSAlg_join U0) . x,y),
z = (U1 "\/"_os U2) "\/"_os U3 )
by Def16;
set B = the
Sorts of
U1 \/ (the Sorts of U2 \/ the Sorts of U3);
A2:
( the
Sorts of
U1 is
OrderSortedSet of & the
Sorts of
U2 is
OrderSortedSet of & the
Sorts of
U3 is
OrderSortedSet of )
by OSALG_1:17;
then A3:
( the
Sorts of
U1 \/ the
Sorts of
U2 is
OrderSortedSet of & the
Sorts of
U2 \/ the
Sorts of
U3 is
OrderSortedSet of )
by Th2;
then A4:
the
Sorts of
U1 \/ (the Sorts of U2 \/ the Sorts of U3) is
OrderSortedSet of
by A2, Th2;
( 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 MSUALG_2:def 10;
then A5:
( 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 A6:
the
Sorts of
U2 \/ the
Sorts of
U3 c= the
Sorts of
U0
by PBOOLE:18;
A7:
the
Sorts of
U1 \/ the
Sorts of
U2 c= the
Sorts of
U0
by A5, PBOOLE:18;
reconsider C1 = the
Sorts of
U2 \/ the
Sorts of
U3 as
MSSubset of
U0 by A6, PBOOLE:def 23;
reconsider C =
C1 as
OSSubset of
U0 by A3, Def2;
reconsider D1 = the
Sorts of
U1 \/ the
Sorts of
U2 as
MSSubset of
U0 by A7, PBOOLE:def 23;
reconsider D =
D1 as
OSSubset of
U0 by A3, Def2;
the
Sorts of
U1 \/ (the Sorts of U2 \/ the Sorts of U3) c= the
Sorts of
U0
by A5, A6, PBOOLE:18;
then
the
Sorts of
U1 \/ (the Sorts of U2 \/ the Sorts of U3) is
MSSubset of
U0
by PBOOLE:def 23;
then reconsider B = the
Sorts of
U1 \/ (the Sorts of U2 \/ the Sorts of U3) as
OSSubset of
U0 by A4, Def2;
A8:
U1 "\/"_os (U2 "\/"_os U3) =
U1 "\/"_os (GenOSAlg C)
by Def14
.=
(GenOSAlg C) "\/"_os U1
by Th44
.=
GenOSAlg B
by Th42
;
A9:
B = D \/ the
Sorts of
U3
by PBOOLE:34;
(U1 "\/"_os U2) "\/"_os U3 =
(GenOSAlg D) "\/"_os U3
by Def14
.=
GenOSAlg B
by A9, Th42
;
hence
(OSAlg_join U0) . x,
((OSAlg_join U0) . y,z) = (OSAlg_join U0) . ((OSAlg_join U0) . x,y),
z
by A1, A8;
:: thesis: verum
end;
hence
OSAlg_join U0 is associative
by BINOP_1:def 3; :: thesis: verum