endmndlem

Description: A diagonal hom-set in a category equipped with the restriction of the composition has a structure of monoid. See also df-mndtc for converting a monoid to a category. Lemma for bj-endmnd . (Contributed by Zhi Wang, 25-Sep-2024)

	Ref	Expression
Hypotheses	endmndlem.b	$⊢ B = {Base}_{C}$
	endmndlem.h	$⊢ H = Hom (C)$
	endmndlem.o	$⊢ \underset{˙}{\cdot} = comp (C)$
	endmndlem.c	$⊢ φ \to C \in Cat$
	endmndlem.x	$⊢ φ \to X \in B$
	endmndlem.m	$⊢ φ \to X H X = {Base}_{M}$
	endmndlem.p	$⊢ φ \to ⟨X, X⟩ \underset{˙}{\cdot} X = +_{M}$
Assertion	endmndlem	$⊢ φ \to M \in Mnd$

Proof

Step	Hyp	Ref	Expression
1		endmndlem.b	$⊢ B = {Base}_{C}$
2		endmndlem.h	$⊢ H = Hom (C)$
3		endmndlem.o	$⊢ \underset{˙}{\cdot} = comp (C)$
4		endmndlem.c	$⊢ φ \to C \in Cat$
5		endmndlem.x	$⊢ φ \to X \in B$
6		endmndlem.m	$⊢ φ \to X H X = {Base}_{M}$
7		endmndlem.p	$⊢ φ \to ⟨X, X⟩ \underset{˙}{\cdot} X = +_{M}$
8	4	3ad2ant1	$⊢ (φ \land f \in (X H X) \land g \in (X H X)) \to C \in Cat$
9	5	3ad2ant1	$⊢ (φ \land f \in (X H X) \land g \in (X H X)) \to X \in B$
10		simp3	$⊢ (φ \land f \in (X H X) \land g \in (X H X)) \to g \in (X H X)$
11		simp2	$⊢ (φ \land f \in (X H X) \land g \in (X H X)) \to f \in (X H X)$
12	1 2 3 8 9 9 9 10 11	catcocl	$⊢ (φ \land f \in (X H X) \land g \in (X H X)) \to f (⟨X, X⟩ \underset{˙}{\cdot} X) g \in (X H X)$
13	4	adantr	$⊢ (φ \land (f \in (X H X) \land g \in (X H X) \land k \in (X H X))) \to C \in Cat$
14	5	adantr	$⊢ (φ \land (f \in (X H X) \land g \in (X H X) \land k \in (X H X))) \to X \in B$
15		simpr3	$⊢ (φ \land (f \in (X H X) \land g \in (X H X) \land k \in (X H X))) \to k \in (X H X)$
16		simpr2	$⊢ (φ \land (f \in (X H X) \land g \in (X H X) \land k \in (X H X))) \to g \in (X H X)$
17		simpr1	$⊢ (φ \land (f \in (X H X) \land g \in (X H X) \land k \in (X H X))) \to f \in (X H X)$
18	1 2 3 13 14 14 14 15 16 14 17	catass	$⊢ (φ \land (f \in (X H X) \land g \in (X H X) \land k \in (X H X))) \to (f (⟨X, X⟩ \underset{˙}{\cdot} X) g) (⟨X, X⟩ \underset{˙}{\cdot} X) k = f (⟨X, X⟩ \underset{˙}{\cdot} X) (g (⟨X, X⟩ \underset{˙}{\cdot} X) k)$
19		eqid	$⊢ Id (C) = Id (C)$
20	1 2 19 4 5	catidcl	$⊢ φ \to Id (C) (X) \in (X H X)$
21	4	adantr	$⊢ (φ \land f \in (X H X)) \to C \in Cat$
22	5	adantr	$⊢ (φ \land f \in (X H X)) \to X \in B$
23		simpr	$⊢ (φ \land f \in (X H X)) \to f \in (X H X)$
24	1 2 19 21 22 3 22 23	catlid	$⊢ (φ \land f \in (X H X)) \to Id (C) (X) (⟨X, X⟩ \underset{˙}{\cdot} X) f = f$
25	1 2 19 21 22 3 22 23	catrid	$⊢ (φ \land f \in (X H X)) \to f (⟨X, X⟩ \underset{˙}{\cdot} X) Id (C) (X) = f$
26	6 7 12 18 20 24 25	ismndd	$⊢ φ \to M \in Mnd$

Metamath Proof Explorer

Theorem endmndlem

Proof