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	mndtcbas.c	No typesetting found for |- ( ph -> C = ( MndToCat ` M ) ) with typecode |-
	mndtcbas.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
	mndtcbas.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		mndtcbas.c	Could not format ( ph -> C = ( MndToCat ` M ) ) : No typesetting found for |- ( ph -> C = ( MndToCat ` M ) ) with typecode |-
2		mndtcbas.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
3		mndtcbas.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 |-