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	$$⊢\phi \to C=\mathrm{MndToCat}\left(M\right)$$
	mndtccat.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
	oppgoppchom.d	$$⊢\phi \to D=\mathrm{MndToCat}\left({opp}_{𝑔}\left(M\right)\right)$$
	oppgoppchom.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	oppgoppchom.x	$$⊢\phi \to X\in {\mathrm{Base}}_D$$
	oppgoppchom.y	$$⊢\phi \to Y\in {\mathrm{Base}}_O$$
	oppgoppcco.o	$$⊢\phi \to \underset{\dot{}}{·}=\mathrm{comp}\left(D\right)$$
	oppgoppcco.x	$$⊢\phi \to \underset{\dot{}}{\bullet }=\mathrm{comp}\left(O\right)$$
Assertion	oppgoppcco	$$⊢\phi \to ⟨X,X⟩\underset{\dot{}}{·}X=⟨Y,Y⟩\underset{\dot{}}{\bullet }Y$$

Proof

Step	Hyp	Ref	Expression
1		mndtccat.c	$$⊢\phi \to C=\mathrm{MndToCat}\left(M\right)$$
2		mndtccat.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
3		oppgoppchom.d	$$⊢\phi \to D=\mathrm{MndToCat}\left({opp}_{𝑔}\left(M\right)\right)$$
4		oppgoppchom.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
5		oppgoppchom.x	$$⊢\phi \to X\in {\mathrm{Base}}_D$$
6		oppgoppchom.y	$$⊢\phi \to Y\in {\mathrm{Base}}_O$$
7		oppgoppcco.o	$$⊢\phi \to \underset{\dot{}}{·}=\mathrm{comp}\left(D\right)$$
8		oppgoppcco.x	$$⊢\phi \to \underset{\dot{}}{\bullet }=\mathrm{comp}\left(O\right)$$
9		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
10	4 9	oppcbas	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_O$$
11	10	eqcomi	$$⊢{\mathrm{Base}}_O={\mathrm{Base}}_C$$
12	11	a1i	$$⊢\phi \to {\mathrm{Base}}_O={\mathrm{Base}}_C$$
13		eqidd	$$⊢\phi \to \mathrm{comp}\left(C\right)=\mathrm{comp}\left(C\right)$$
14	1 2 12 6 6 6 13	mndtcco	$$⊢\phi \to ⟨Y,Y⟩\mathrm{comp}\left(C\right)Y={+}_M$$
15	14	tposeqd	$$⊢\phi \to tpos\left(⟨Y,Y⟩\mathrm{comp}\left(C\right)Y\right)=tpos{+}_M$$
16		eqid	$$⊢\mathrm{comp}\left(C\right)=\mathrm{comp}\left(C\right)$$
17	11 16 4 6 6 6	oppccofval	$$⊢\phi \to ⟨Y,Y⟩\mathrm{comp}\left(O\right)Y=tpos\left(⟨Y,Y⟩\mathrm{comp}\left(C\right)Y\right)$$
18		eqid	$$⊢{opp}_{𝑔}\left(M\right)={opp}_{𝑔}\left(M\right)$$
19	18	oppgmnd	$$⊢M\in \mathrm{Mnd}\to {opp}_{𝑔}\left(M\right)\in \mathrm{Mnd}$$
20	2 19	syl	$$⊢\phi \to {opp}_{𝑔}\left(M\right)\in \mathrm{Mnd}$$
21		eqidd	$$⊢\phi \to {\mathrm{Base}}_D={\mathrm{Base}}_D$$
22	3 20 21 5 5 5 7	mndtcco	$$⊢\phi \to ⟨X,X⟩\underset{\dot{}}{·}X={+}_{{opp}_{𝑔}\left(M\right)}$$
23		eqid	$$⊢{+}_M={+}_M$$
24		eqid	$$⊢{+}_{{opp}_{𝑔}\left(M\right)}={+}_{{opp}_{𝑔}\left(M\right)}$$
25	23 18 24	oppgplusfval	$$⊢{+}_{{opp}_{𝑔}\left(M\right)}=tpos{+}_M$$
26	22 25	eqtrdi	$$⊢\phi \to ⟨X,X⟩\underset{\dot{}}{·}X=tpos{+}_M$$
27	15 17 26	3eqtr4rd	$$⊢\phi \to ⟨X,X⟩\underset{\dot{}}{·}X=⟨Y,Y⟩\mathrm{comp}\left(O\right)Y$$
28	8	oveqd	$$⊢\phi \to ⟨Y,Y⟩\underset{\dot{}}{\bullet }Y=⟨Y,Y⟩\mathrm{comp}\left(O\right)Y$$
29	27 28	eqtr4d	$$⊢\phi \to ⟨X,X⟩\underset{\dot{}}{·}X=⟨Y,Y⟩\underset{\dot{}}{\bullet }Y$$