let A, B be non empty transitive AltCatStr ; ( A,B are_opposite & A is associative implies B is associative )
assume that
A1:
A,B are_opposite
and
A2:
A is associative
; B is associative
deffunc H1( set , set , set , set , set ) -> set = ( the Comp of A . ($3,$2,$1)) . ($4,$5);
A3:
now for a, b, c being Object of B st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = H1(a,b,c,f,g)let a,
b,
c be
Object of
B;
( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c holds g * f = H1(a,b,c,f,g) )assume that A4:
<^a,b^> <> {}
and A5:
<^b,c^> <> {}
;
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = H1(a,b,c,f,g)let f be
Morphism of
a,
b;
for g being Morphism of b,c holds g * f = H1(a,b,c,f,g)let g be
Morphism of
b,
c;
g * f = H1(a,b,c,f,g)reconsider a9 =
a,
b9 =
b,
c9 =
c as
Object of
A by A1;
A6:
<^a,b^> = <^b9,a9^>
by A1, Th7;
A7:
<^b,c^> = <^c9,b9^>
by A1, Th7;
reconsider f9 =
f as
Morphism of
b9,
a9 by A1, Th7;
reconsider g9 =
g as
Morphism of
c9,
b9 by A1, Th7;
thus g * f =
f9 * g9
by A1, A4, A5, Th9
.=
H1(
a,
b,
c,
f,
g)
by A4, A5, A6, A7, ALTCAT_1:def 8
;
verum end;
A8:
now for a, b, c, d being Object of B
for f, g, h being set st f in <^a,b^> & g in <^b,c^> & h in <^c,d^> holds
H1(a,c,d,H1(a,b,c,f,g),h) = H1(a,b,d,f,H1(b,c,d,g,h))let a,
b,
c,
d be
Object of
B;
for f, g, h being set st f in <^a,b^> & g in <^b,c^> & h in <^c,d^> holds
H1(a,c,d,H1(a,b,c,f,g),h) = H1(a,b,d,f,H1(b,c,d,g,h))let f,
g,
h be
set ;
( f in <^a,b^> & g in <^b,c^> & h in <^c,d^> implies H1(a,c,d,H1(a,b,c,f,g),h) = H1(a,b,d,f,H1(b,c,d,g,h)) )reconsider a9 =
a,
b9 =
b,
c9 =
c,
d9 =
d as
Object of
A by A1;
assume A9:
f in <^a,b^>
;
( g in <^b,c^> & h in <^c,d^> implies H1(a,c,d,H1(a,b,c,f,g),h) = H1(a,b,d,f,H1(b,c,d,g,h)) )then A10:
f in <^b9,a9^>
by A1, Th9;
reconsider f9 =
f as
Morphism of
b9,
a9 by A1, A9, Th9;
assume A11:
g in <^b,c^>
;
( h in <^c,d^> implies H1(a,c,d,H1(a,b,c,f,g),h) = H1(a,b,d,f,H1(b,c,d,g,h)) )then A12:
g in <^c9,b9^>
by A1, Th9;
reconsider g9 =
g as
Morphism of
c9,
b9 by A1, A11, Th9;
assume A13:
h in <^c,d^>
;
H1(a,c,d,H1(a,b,c,f,g),h) = H1(a,b,d,f,H1(b,c,d,g,h))then A14:
h in <^d9,c9^>
by A1, Th9;
reconsider h9 =
h as
Morphism of
d9,
c9 by A1, A13, Th9;
A15:
<^c9,a9^> <> {}
by A10, A12, ALTCAT_1:def 2;
A16:
<^d9,b9^> <> {}
by A12, A14, ALTCAT_1:def 2;
thus H1(
a,
c,
d,
H1(
a,
b,
c,
f,
g),
h) =
H1(
a,
c,
d,
f9 * g9,
h)
by A10, A12, ALTCAT_1:def 8
.=
(f9 * g9) * h9
by A14, A15, ALTCAT_1:def 8
.=
f9 * (g9 * h9)
by A2, A10, A12, A14
.=
H1(
a,
b,
d,
f,
g9 * h9)
by A10, A16, ALTCAT_1:def 8
.=
H1(
a,
b,
d,
f,
H1(
b,
c,
d,
g,
h))
by A12, A14, ALTCAT_1:def 8
;
verum end;
thus
B is associative
from YELLOW18:sch 2(A3, A8); verum