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 ⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
mndtccat.m ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
oppgoppchom.d ⊢ ( 𝜑 → 𝐷 = ( MndToCat ‘ ( oppg ‘ 𝑀 ) ) )
oppgoppchom.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
oppgoppchom.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐷 ) )
oppgoppchom.y ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝑂 ) )
oppgoppcco.o ⊢ ( 𝜑 → · = ( comp ‘ 𝐷 ) )
oppgoppcco.x ⊢ ( 𝜑 → ∙ = ( comp ‘ 𝑂 ) )
Assertion oppgoppcco ( 𝜑 → ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) = ( ⟨ 𝑌 , 𝑌 ⟩ ∙ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 mndtccat.c ⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
2 mndtccat.m ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
3 oppgoppchom.d ⊢ ( 𝜑 → 𝐷 = ( MndToCat ‘ ( oppg ‘ 𝑀 ) ) )
4 oppgoppchom.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
5 oppgoppchom.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐷 ) )
6 oppgoppchom.y ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝑂 ) )
7 oppgoppcco.o ⊢ ( 𝜑 → · = ( comp ‘ 𝐷 ) )
8 oppgoppcco.x ⊢ ( 𝜑 → ∙ = ( comp ‘ 𝑂 ) )
9 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
10 4 9 oppcbas ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 )
11 10 eqcomi ⊢ ( Base ‘ 𝑂 ) = ( Base ‘ 𝐶 )
12 11 a1i ⊢ ( 𝜑 → ( Base ‘ 𝑂 ) = ( Base ‘ 𝐶 ) )
13 eqidd ⊢ ( 𝜑 → ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 ) )
14 1 2 12 6 6 6 13 mndtcco ⊢ ( 𝜑 → ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) = ( +g ‘ 𝑀 ) )
15 14 tposeqd ⊢ ( 𝜑 → tpos ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) = tpos ( +g ‘ 𝑀 ) )
16 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
17 11 16 4 6 6 6 oppccofval ⊢ ( 𝜑 → ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝑂 ) 𝑌 ) = tpos ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) )
18 eqid ⊢ ( oppg ‘ 𝑀 ) = ( oppg ‘ 𝑀 )
19 18 oppgmnd ⊢ ( 𝑀 ∈ Mnd → ( oppg ‘ 𝑀 ) ∈ Mnd )
20 2 19 syl ⊢ ( 𝜑 → ( oppg ‘ 𝑀 ) ∈ Mnd )
21 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 ) )
22 3 20 21 5 5 5 7 mndtcco ⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) = ( +g ‘ ( oppg ‘ 𝑀 ) ) )
23 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
24 eqid ⊢ ( +g ‘ ( oppg ‘ 𝑀 ) ) = ( +g ‘ ( oppg ‘ 𝑀 ) )
25 23 18 24 oppgplusfval ⊢ ( +g ‘ ( oppg ‘ 𝑀 ) ) = tpos ( +g ‘ 𝑀 )
26 22 25 eqtrdi ⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) = tpos ( +g ‘ 𝑀 ) )
27 15 17 26 3eqtr4rd ⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) = ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝑂 ) 𝑌 ) )
28 8 oveqd ⊢ ( 𝜑 → ( ⟨ 𝑌 , 𝑌 ⟩ ∙ 𝑌 ) = ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝑂 ) 𝑌 ) )
29 27 28 eqtr4d ⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) = ( ⟨ 𝑌 , 𝑌 ⟩ ∙ 𝑌 ) )