grptcmon

Description: All morphisms in a category converted from a group are monomorphisms. (Contributed by Zhi Wang, 23-Sep-2024)

	Ref	Expression
Hypotheses	grptcmon.c	No typesetting found for \|- ( ph -> C = ( MndToCat ` G ) ) with typecode \|-
	grptcmon.g	$⊢ φ \to G \in Grp$
	grptcmon.b	$⊢ φ \to B = {Base}_{C}$
	grptcmon.x	$⊢ φ \to X \in B$
	grptcmon.y	$⊢ φ \to Y \in B$
	grptcmon.h	$⊢ φ \to H = Hom (C)$
	grptcmon.m	$⊢ φ \to M = Mono (C)$
Assertion	grptcmon	$⊢ φ \to X M Y = X H Y$

Proof

Step	Hyp	Ref	Expression
1		grptcmon.c	Could not format ( ph -> C = ( MndToCat ` G ) ) : No typesetting found for \|- ( ph -> C = ( MndToCat ` G ) ) with typecode \|-
2		grptcmon.g	$⊢ φ \to G \in Grp$
3		grptcmon.b	$⊢ φ \to B = {Base}_{C}$
4		grptcmon.x	$⊢ φ \to X \in B$
5		grptcmon.y	$⊢ φ \to Y \in B$
6		grptcmon.h	$⊢ φ \to H = Hom (C)$
7		grptcmon.m	$⊢ φ \to M = Mono (C)$
8		eqid	$⊢ {Base}_{C} = {Base}_{C}$
9		eqid	$⊢ Hom (C) = Hom (C)$
10		eqid	$⊢ comp (C) = comp (C)$
11		eqid	$⊢ Mono (C) = Mono (C)$
12	2	grpmndd	$⊢ φ \to G \in Mnd$
13	1 12	mndtccat	$⊢ φ \to C \in Cat$
14	4 3	eleqtrd	$⊢ φ \to X \in {Base}_{C}$
15	5 3	eleqtrd	$⊢ φ \to Y \in {Base}_{C}$
16	8 9 10 11 13 14 15	ismon2	$⊢ φ \to (f \in (X Mono (C) Y) \leftrightarrow (f \in (X Hom (C) Y) \land \forall z \in {Base}_{C} \forall g \in (z Hom (C) X) \forall h \in (z Hom (C) X) (f (⟨z, X⟩ comp (C) Y) g = f (⟨z, X⟩ comp (C) Y) h \to g = h)))$
17	1	ad2antrr	Could not format ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( z ( Hom ` C ) X ) /\ h e. ( z ( Hom ` C ) X ) ) ) -> C = ( MndToCat ` G ) ) : No typesetting found for \|- ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( z ( Hom ` C ) X ) /\ h e. ( z ( Hom ` C ) X ) ) ) -> C = ( MndToCat ` G ) ) with typecode \|-
18	12	ad2antrr	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to G \in Mnd$
19	3	ad2antrr	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to B = {Base}_{C}$
20		simpr1	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to z \in {Base}_{C}$
21	20 19	eleqtrrd	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to z \in B$
22	4	ad2antrr	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to X \in B$
23	5	ad2antrr	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to Y \in B$
24		eqidd	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to comp (C) = comp (C)$
25		eqidd	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to ⟨z, X⟩ comp (C) Y = ⟨z, X⟩ comp (C) Y$
26	17 18 19 21 22 23 24 25	mndtcco2	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to f (⟨z, X⟩ comp (C) Y) g = f +_{G} g$
27	17 18 19 21 22 23 24 25	mndtcco2	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to f (⟨z, X⟩ comp (C) Y) h = f +_{G} h$
28	26 27	eqeq12d	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to (f (⟨z, X⟩ comp (C) Y) g = f (⟨z, X⟩ comp (C) Y) h \leftrightarrow f +_{G} g = f +_{G} h)$
29	2	ad2antrr	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to G \in Grp$
30		simpr2	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to g \in (z Hom (C) X)$
31		eqidd	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to Hom (C) = Hom (C)$
32	17 18 19 21 22 31	mndtchom	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to z Hom (C) X = {Base}_{G}$
33	30 32	eleqtrd	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to g \in {Base}_{G}$
34		simpr3	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to h \in (z Hom (C) X)$
35	34 32	eleqtrd	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to h \in {Base}_{G}$
36		simplr	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to f \in (X Hom (C) Y)$
37	17 18 19 22 23 31	mndtchom	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to X Hom (C) Y = {Base}_{G}$
38	36 37	eleqtrd	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to f \in {Base}_{G}$
39		eqid	$⊢ {Base}_{G} = {Base}_{G}$
40		eqid	$⊢ +_{G} = +_{G}$
41	39 40	grplcan	$⊢ (G \in Grp \land (g \in {Base}_{G} \land h \in {Base}_{G} \land f \in {Base}_{G})) \to (f +_{G} g = f +_{G} h \leftrightarrow g = h)$
42	29 33 35 38 41	syl13anc	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to (f +_{G} g = f +_{G} h \leftrightarrow g = h)$
43	28 42	bitrd	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to (f (⟨z, X⟩ comp (C) Y) g = f (⟨z, X⟩ comp (C) Y) h \leftrightarrow g = h)$
44	43	biimpd	$⊢ ((φ \land f \in (X Hom (C) Y)) \land (z \in {Base}_{C} \land g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to (f (⟨z, X⟩ comp (C) Y) g = f (⟨z, X⟩ comp (C) Y) h \to g = h)$
45	44	ralrimivvva	$⊢ (φ \land f \in (X Hom (C) Y)) \to \forall z \in {Base}_{C} \forall g \in (z Hom (C) X) \forall h \in (z Hom (C) X) (f (⟨z, X⟩ comp (C) Y) g = f (⟨z, X⟩ comp (C) Y) h \to g = h)$
46	16 45	mpbiran3d	$⊢ φ \to (f \in (X Mono (C) Y) \leftrightarrow f \in (X Hom (C) Y))$
47	46	eqrdv	$⊢ φ \to X Mono (C) Y = X Hom (C) Y$
48	7	oveqd	$⊢ φ \to X M Y = X Mono (C) Y$
49	6	oveqd	$⊢ φ \to X H Y = X Hom (C) Y$
50	47 48 49	3eqtr4d	$⊢ φ \to X M Y = X H Y$

Metamath Proof Explorer

Theorem grptcmon

Proof