let A, B be non empty transitive AltCatStr ; :: thesis: ( A,B are_opposite & A is associative implies B is associative )
assume that
A1:
A,B are_opposite
and
A2:
A is associative
; :: thesis: B is associative
deffunc H1( set , set , set , set , set ) -> set = (the Comp of A . $3,$2,$1) . $4,$5;
A3:
now let a,
b,
c be
object of
B;
:: thesis: ( <^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 A4:
(
<^a,b^> <> {} &
<^b,c^> <> {} )
;
:: thesis: 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;
:: thesis: for g being Morphism of b,c holds g * f = H1(a,b,c,f,g)let g be
Morphism of
b,
c;
:: thesis: g * f = H1(a,b,c,f,g)reconsider a' =
a,
b' =
b,
c' =
c as
object of
A by A1, Th6;
A5:
(
<^a,b^> = <^b',a'^> &
<^b,c^> = <^c',b'^> )
by A1, Th7;
reconsider f' =
f as
Morphism of
b',
a' by A1, Th7;
reconsider g' =
g as
Morphism of
c',
b' by A1, Th7;
thus g * f =
f' * g'
by A1, A4, Th9
.=
H1(
a,
b,
c,
f,
g)
by A4, A5, ALTCAT_1:def 10
;
:: thesis: verum end;
A6:
now let a,
b,
c,
d be
object of
B;
:: thesis: 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 ;
:: thesis: ( 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 a' =
a,
b' =
b,
c' =
c,
d' =
d as
object of
A by A1, Def3;
assume A7:
f in <^a,b^>
;
:: thesis: ( 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 A8:
f in <^b',a'^>
by A1, Th9;
reconsider f' =
f as
Morphism of
b',
a' by A1, A7, Th9;
assume A9:
g in <^b,c^>
;
:: thesis: ( 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:
g in <^c',b'^>
by A1, Th9;
reconsider g' =
g as
Morphism of
c',
b' by A1, A9, Th9;
assume A11:
h in <^c,d^>
;
:: thesis: H1(a,c,d,H1(a,b,c,f,g),h) = H1(a,b,d,f,H1(b,c,d,g,h))then A12:
h in <^d',c'^>
by A1, Th9;
reconsider h' =
h as
Morphism of
d',
c' by A1, A11, Th9;
A13:
(
<^c',a'^> <> {} &
<^d',b'^> <> {} )
by A8, A10, A12, ALTCAT_1:def 4;
thus H1(
a,
c,
d,
H1(
a,
b,
c,
f,
g),
h) =
H1(
a,
c,
d,
f' * g',
h)
by A8, A10, ALTCAT_1:def 10
.=
(f' * g') * h'
by A12, A13, ALTCAT_1:def 10
.=
f' * (g' * h')
by A2, A8, A10, A12, ALTCAT_1:25
.=
H1(
a,
b,
d,
f,
g' * h')
by A8, A13, ALTCAT_1:def 10
.=
H1(
a,
b,
d,
f,
H1(
b,
c,
d,
g,
h))
by A10, A12, ALTCAT_1:def 10
;
:: thesis: verum end;
thus
B is associative
from YELLOW18:sch 2(A3, A6); :: thesis: verum