Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝐺 ) )
grptcmon.g ⊢ ( 𝜑 → 𝐺 ∈ Grp )
grptcmon.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
grptcmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
grptcmon.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
grptcmon.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
grptcmon.m ⊢ ( 𝜑 → 𝑀 = ( Mono ‘ 𝐶 ) )
Assertion grptcmon ( 𝜑 → ( 𝑋 𝑀 𝑌 ) = ( 𝑋 𝐻 𝑌 ) )

Proof

Step Hyp Ref Expression
1 grptcmon.c ⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝐺 ) )
2 grptcmon.g ⊢ ( 𝜑 → 𝐺 ∈ Grp )
3 grptcmon.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
4 grptcmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 grptcmon.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 grptcmon.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
7 grptcmon.m ⊢ ( 𝜑 → 𝑀 = ( Mono ‘ 𝐶 ) )
8 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
9 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
10 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
11 eqid ⊢ ( Mono ‘ 𝐶 ) = ( Mono ‘ 𝐶 )
12 2 grpmndd ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
13 1 12 mndtccat ⊢ ( 𝜑 → 𝐶 ∈ Cat )
14 4 3 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
15 5 3 eleqtrd ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
16 8 9 10 11 13 14 15 ismon2 ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑋 ( Mono ‘ 𝐶 ) 𝑌 ) ↔ ( 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∀ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ( ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) → 𝑔 = ℎ ) ) ) )
17 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝐶 = ( MndToCat ‘ 𝐺 ) )
18 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝐺 ∈ Mnd )
19 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝐵 = ( Base ‘ 𝐶 ) )
20 simpr1 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
21 20 19 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝑧 ∈ 𝐵 )
22 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝑋 ∈ 𝐵 )
23 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝑌 ∈ 𝐵 )
24 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 ) )
25 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) = ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) )
26 17 18 19 21 22 23 24 25 mndtcco2 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝑓 ( +g ‘ 𝐺 ) 𝑔 ) )
27 17 18 19 21 22 23 24 25 mndtcco2 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) = ( 𝑓 ( +g ‘ 𝐺 ) ℎ ) )
28 26 27 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) ↔ ( 𝑓 ( +g ‘ 𝐺 ) 𝑔 ) = ( 𝑓 ( +g ‘ 𝐺 ) ℎ ) ) )
29 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝐺 ∈ Grp )
30 simpr2 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) )
31 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) )
32 17 18 19 21 22 31 mndtchom ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) = ( Base ‘ 𝐺 ) )
33 30 32 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝑔 ∈ ( Base ‘ 𝐺 ) )
34 simpr3 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) )
35 34 32 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ℎ ∈ ( Base ‘ 𝐺 ) )
36 simplr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
37 17 18 19 22 23 31 mndtchom ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) = ( Base ‘ 𝐺 ) )
38 36 37 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝑓 ∈ ( Base ‘ 𝐺 ) )
39 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
40 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
41 39 40 grplcan ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑔 ∈ ( Base ‘ 𝐺 ) ∧ ℎ ∈ ( Base ‘ 𝐺 ) ∧ 𝑓 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑓 ( +g ‘ 𝐺 ) 𝑔 ) = ( 𝑓 ( +g ‘ 𝐺 ) ℎ ) ↔ 𝑔 = ℎ ) )
42 29 33 35 38 41 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( ( 𝑓 ( +g ‘ 𝐺 ) 𝑔 ) = ( 𝑓 ( +g ‘ 𝐺 ) ℎ ) ↔ 𝑔 = ℎ ) )
43 28 42 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) ↔ 𝑔 = ℎ ) )
44 43 biimpd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) → 𝑔 = ℎ ) )
45 44 ralrimivvva ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) → ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∀ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ( ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) → 𝑔 = ℎ ) )
46 16 45 mpbiran3d ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑋 ( Mono ‘ 𝐶 ) 𝑌 ) ↔ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) )
47 46 eqrdv ⊢ ( 𝜑 → ( 𝑋 ( Mono ‘ 𝐶 ) 𝑌 ) = ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
48 7 oveqd ⊢ ( 𝜑 → ( 𝑋 𝑀 𝑌 ) = ( 𝑋 ( Mono ‘ 𝐶 ) 𝑌 ) )
49 6 oveqd ⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
50 47 48 49 3eqtr4d ⊢ ( 𝜑 → ( 𝑋 𝑀 𝑌 ) = ( 𝑋 𝐻 𝑌 ) )