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	⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
	mndtcbas.m	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
	mndtcbas.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
	mndtchom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	mndtchom.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	mndtcco.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	mndtcco.o	⊢ ( 𝜑 → · = ( comp ‘ 𝐶 ) )
Assertion	mndtcco	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) = ( +_g ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		mndtcbas.c	⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
2		mndtcbas.m	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
3		mndtcbas.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
4		mndtchom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		mndtchom.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		mndtcco.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
7		mndtcco.o	⊢ ( 𝜑 → · = ( comp ‘ 𝐶 ) )
8	1 2	mndtcval	⊢ ( 𝜑 → 𝐶 = { ⟨ ( Base ‘ ndx ) , { 𝑀 } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ 𝑀 , 𝑀 , ( Base ‘ 𝑀 ) ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +_g ‘ 𝑀 ) ⟩ } ⟩ } )
9		catstr	⊢ { ⟨ ( Base ‘ ndx ) , { 𝑀 } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ 𝑀 , 𝑀 , ( Base ‘ 𝑀 ) ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +_g ‘ 𝑀 ) ⟩ } ⟩ } Struct ⟨ 1 , ; 1 5 ⟩
10		ccoid	⊢ comp = Slot ( comp ‘ ndx )
11		snsstp3	⊢ { ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +_g ‘ 𝑀 ) ⟩ } ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , { 𝑀 } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ 𝑀 , 𝑀 , ( Base ‘ 𝑀 ) ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +_g ‘ 𝑀 ) ⟩ } ⟩ }
12		snex	⊢ { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +_g ‘ 𝑀 ) ⟩ } ∈ V
13	12	a1i	⊢ ( 𝜑 → { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +_g ‘ 𝑀 ) ⟩ } ∈ V )
14		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
15	8 9 10 11 13 14	strfv3	⊢ ( 𝜑 → ( comp ‘ 𝐶 ) = { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +_g ‘ 𝑀 ) ⟩ } )
16	7 15	eqtrd	⊢ ( 𝜑 → · = { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +_g ‘ 𝑀 ) ⟩ } )
17	1 2 3 4	mndtcob	⊢ ( 𝜑 → 𝑋 = 𝑀 )
18	1 2 3 5	mndtcob	⊢ ( 𝜑 → 𝑌 = 𝑀 )
19	17 18	opeq12d	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑀 , 𝑀 ⟩ )
20	1 2 3 6	mndtcob	⊢ ( 𝜑 → 𝑍 = 𝑀 )
21	16 19 20	oveq123d	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) = ( ⟨ 𝑀 , 𝑀 ⟩ { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +_g ‘ 𝑀 ) ⟩ } 𝑀 ) )
22		df-ov	⊢ ( ⟨ 𝑀 , 𝑀 ⟩ { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +_g ‘ 𝑀 ) ⟩ } 𝑀 ) = ( { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +_g ‘ 𝑀 ) ⟩ } ‘ ⟨ ⟨ 𝑀 , 𝑀 ⟩ , 𝑀 ⟩ )
23		df-ot	⊢ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ = ⟨ ⟨ 𝑀 , 𝑀 ⟩ , 𝑀 ⟩
24	23	fveq2i	⊢ ( { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +_g ‘ 𝑀 ) ⟩ } ‘ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ ) = ( { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +_g ‘ 𝑀 ) ⟩ } ‘ ⟨ ⟨ 𝑀 , 𝑀 ⟩ , 𝑀 ⟩ )
25		otex	⊢ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ ∈ V
26		fvex	⊢ ( +_g ‘ 𝑀 ) ∈ V
27	25 26	fvsn	⊢ ( { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +_g ‘ 𝑀 ) ⟩ } ‘ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ ) = ( +_g ‘ 𝑀 )
28	22 24 27	3eqtr2i	⊢ ( ⟨ 𝑀 , 𝑀 ⟩ { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +_g ‘ 𝑀 ) ⟩ } 𝑀 ) = ( +_g ‘ 𝑀 )
29	21 28	eqtrdi	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) = ( +_g ‘ 𝑀 ) )

Metamath Proof Explorer

Theorem mndtcco

Proof