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	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) = ( ⟨ 𝑌 , 𝑌 ⟩ ∙ 𝑌 ) )