This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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