Metamath Proof Explorer

Theorem grptcepi

Description: All morphisms in a category converted from a group are epimorphisms. (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 ‘ 𝐶 ) )
grptcepi.e ⊢ ( 𝜑 → 𝐸 = ( Epi ‘ 𝐶 ) )
Assertion grptcepi ( 𝜑 → ( 𝑋 𝐸 𝑌 ) = ( 𝑋 𝐻 𝑌 ) )

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 grptcepi.e ⊢ ( 𝜑 → 𝐸 = ( Epi ‘ 𝐶 ) )
8 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
9 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
10 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
11 eqid ⊢ ( Epi ‘ 𝐶 ) = ( Epi ‘ 𝐶 )
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 isepi2 ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑋 ( Epi ‘ 𝐶 ) 𝑌 ) ↔ ( 𝑓 ∈ ( 𝑋 ( 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 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑋 ∈ 𝐵 )
21 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑌 ∈ 𝐵 )
22 simpr1 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
23 22 19 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑧 ∈ 𝐵 )
24 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 ) )
25 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) = ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) )
26 17 18 19 20 21 23 24 25 mndtcco2 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( +g ‘ 𝐺 ) 𝑓 ) )
27 17 18 19 20 21 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 23 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 20 21 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 grprcan ⊢ ( ( 𝐺 ∈ 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 ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑋 ( Epi ‘ 𝐶 ) 𝑌 ) ↔ 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) )
47 46 eqrdv ⊢ ( 𝜑 → ( 𝑋 ( Epi ‘ 𝐶 ) 𝑌 ) = ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
48 7 oveqd ⊢ ( 𝜑 → ( 𝑋 𝐸 𝑌 ) = ( 𝑋 ( Epi ‘ 𝐶 ) 𝑌 ) )
49 6 oveqd ⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
50 47 48 49 3eqtr4d ⊢ ( 𝜑 → ( 𝑋 𝐸 𝑌 ) = ( 𝑋 𝐻 𝑌 ) )