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	$⊢ φ \to C = MndToCat (M)$
	mndtcbas.m	$⊢ φ \to M \in Mnd$
	mndtcbas.b	$⊢ φ \to B = {Base}_{C}$
	mndtchom.x	$⊢ φ \to X \in B$
	mndtchom.y	$⊢ φ \to Y \in B$
	mndtcco.z	$⊢ φ \to Z \in B$
	mndtcco.o	$⊢ φ \to \underset{˙}{\cdot} = comp (C)$
	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 \|-

Step	Hyp	Ref	Expression
1		mndtcbas.c	$⊢ φ \to C = MndToCat (M)$
2		mndtcbas.m	$⊢ φ \to M \in Mnd$
3		mndtcbas.b	$⊢ φ \to B = {Base}_{C}$
4		mndtchom.x	$⊢ φ \to X \in B$
5		mndtchom.y	$⊢ φ \to Y \in B$
6		mndtcco.z	$⊢ φ \to Z \in B$
7		mndtcco.o	$⊢ φ \to \underset{˙}{\cdot} = comp (C)$
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	$⊢ φ \to ⟨X, Y⟩ \underset{˙}{\cdot} 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 \|-

Metamath Proof Explorer