Theorem mndtcco2

Description: The composition of the category built from a monoid is the monoid operation. (Contributed by Zhi Wang, 22-Sep-2024)

	Ref	Expression
Hypotheses	mndtcbaseu.c	$$⊢\phi \to C=\mathrm{MndToCat}\left(M\right)$$
	mndtcbaseu.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
	mndtcbaseu.b	$$⊢\phi \to B={\mathrm{Base}}_C$$
	mndtchom.x	$$⊢\phi \to X\in B$$
	mndtchom.y	$$⊢\phi \to Y\in B$$
	mndtcco.z	$$⊢\phi \to Z\in B$$
	mndtcco.o	$$⊢\phi \to \underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
	mndtcco2.o2	No typesetting found for |- ( ph -> .o. = ( <. X , Y >. .x. Z ) ) with typecode |-
Assertion	mndtcco2	Could not format assertion : No typesetting found for |- ( ph -> ( G .o. F ) = ( G ( +g ` M ) F ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mndtcbaseu.c	$$⊢\phi \to C=\mathrm{MndToCat}\left(M\right)$$
2		mndtcbaseu.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
3		mndtcbaseu.b	$$⊢\phi \to B={\mathrm{Base}}_C$$
4		mndtchom.x	$$⊢\phi \to X\in B$$
5		mndtchom.y	$$⊢\phi \to Y\in B$$
6		mndtcco.z	$$⊢\phi \to Z\in B$$
7		mndtcco.o	$$⊢\phi \to \underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
8		mndtcco2.o2	Could not format ( ph -> .o. = ( <. X , Y >. .x. Z ) ) : No typesetting found for |- ( ph -> .o. = ( <. X , Y >. .x. Z ) ) with typecode |-
9	1 2 3 4 5 6 7	mndtcco	$$⊢\phi \to ⟨X,Y⟩\underset{\dot{}}{·}Z={+}_M$$
10	8 9	eqtrd	Could not format ( ph -> .o. = ( +g ` M ) ) : No typesetting found for |- ( ph -> .o. = ( +g ` M ) ) with typecode |-
11	10	oveqd	Could not format ( ph -> ( G .o. F ) = ( G ( +g ` M ) F ) ) : No typesetting found for |- ( ph -> ( G .o. F ) = ( G ( +g ` M ) F ) ) with typecode |-