Theorem mndtcco

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)$$
Assertion	mndtcco	$$⊢\phi \to ⟨X,Y⟩\underset{\dot{}}{·}Z={+}_M$$

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	1 2	mndtcval	$$⊢\phi \to C=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{M\right\}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}⟩\right\}$$
9		catstr	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{M\right\}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}⟩\right\}\mathrm{Struct}⟨1,15⟩$$
10		ccoid	$$⊢\mathrm{comp}=\mathrm{Slot}\mathrm{comp}\left(\mathrm{ndx}\right)$$
11		snsstp3	$$⊢\left\{⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{M\right\}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}⟩\right\}$$
12		snex	$$⊢\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}\in \mathrm{V}$$
13	12	a1i	$$⊢\phi \to \left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}\in \mathrm{V}$$
14		eqid	$$⊢\mathrm{comp}\left(C\right)=\mathrm{comp}\left(C\right)$$
15	8 9 10 11 13 14	strfv3	$$⊢\phi \to \mathrm{comp}\left(C\right)=\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}$$
16	7 15	eqtrd	$$⊢\phi \to \underset{\dot{}}{·}=\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}$$
17	1 2 3 4	mndtcob	$$⊢\phi \to X=M$$
18	1 2 3 5	mndtcob	$$⊢\phi \to Y=M$$
19	17 18	opeq12d	$$⊢\phi \to ⟨X,Y⟩=⟨M,M⟩$$
20	1 2 3 6	mndtcob	$$⊢\phi \to Z=M$$
21	16 19 20	oveq123d	$$⊢\phi \to ⟨X,Y⟩\underset{\dot{}}{·}Z=⟨M,M⟩\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}M$$
22		df-ov	$$⊢⟨M,M⟩\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}M=\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}\left(⟨⟨M,M⟩,M⟩\right)$$
23		df-ot	$$⊢⟨M,M,M⟩=⟨⟨M,M⟩,M⟩$$
24	23	fveq2i	$$⊢\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}\left(⟨M,M,M⟩\right)=\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}\left(⟨⟨M,M⟩,M⟩\right)$$
25		otex	$$⊢⟨M,M,M⟩\in \mathrm{V}$$
26		fvex	$$⊢{+}_M\in \mathrm{V}$$
27	25 26	fvsn	$$⊢\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}\left(⟨M,M,M⟩\right)={+}_M$$
28	22 24 27	3eqtr2i	$$⊢⟨M,M⟩\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}M={+}_M$$
29	21 28	eqtrdi	$$⊢\phi \to ⟨X,Y⟩\underset{\dot{}}{·}Z={+}_M$$