Metamath Proof Explorer


Theorem oppgoppcco

Description: The converted opposite monoid has the same composition as that of the opposite category. Example 3.6(2) of Adamek p. 25. (Contributed by Zhi Wang, 22-Sep-2025)

Ref Expression
Hypotheses mndtccat.c φ C = MndToCat M
mndtccat.m φ M Mnd
oppgoppchom.d φ D = MndToCat opp 𝑔 M
oppgoppchom.o O = oppCat C
oppgoppchom.x φ X Base D
oppgoppchom.y φ Y Base O
oppgoppcco.o φ · ˙ = comp D
oppgoppcco.x φ ˙ = comp O
Assertion oppgoppcco φ X X · ˙ X = Y Y ˙ Y

Proof

Step Hyp Ref Expression
1 mndtccat.c φ C = MndToCat M
2 mndtccat.m φ M Mnd
3 oppgoppchom.d φ D = MndToCat opp 𝑔 M
4 oppgoppchom.o O = oppCat C
5 oppgoppchom.x φ X Base D
6 oppgoppchom.y φ Y Base O
7 oppgoppcco.o φ · ˙ = comp D
8 oppgoppcco.x φ ˙ = comp O
9 eqid Base C = Base C
10 4 9 oppcbas Base C = Base O
11 10 eqcomi Base O = Base C
12 11 a1i φ Base O = Base C
13 eqidd φ comp C = comp C
14 1 2 12 6 6 6 13 mndtcco φ Y Y comp C Y = + M
15 14 tposeqd φ tpos Y Y comp C Y = tpos + M
16 eqid comp C = comp C
17 11 16 4 6 6 6 oppccofval φ Y Y comp O Y = tpos Y Y comp C Y
18 eqid opp 𝑔 M = opp 𝑔 M
19 18 oppgmnd M Mnd opp 𝑔 M Mnd
20 2 19 syl φ opp 𝑔 M Mnd
21 eqidd φ Base D = Base D
22 3 20 21 5 5 5 7 mndtcco φ X X · ˙ X = + opp 𝑔 M
23 eqid + M = + M
24 eqid + opp 𝑔 M = + opp 𝑔 M
25 23 18 24 oppgplusfval + opp 𝑔 M = tpos + M
26 22 25 eqtrdi φ X X · ˙ X = tpos + M
27 15 17 26 3eqtr4rd φ X X · ˙ X = Y Y comp O Y
28 8 oveqd φ Y Y ˙ Y = Y Y comp O Y
29 27 28 eqtr4d φ X X · ˙ X = Y Y ˙ Y