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 
|- ( ph -> C = ( MndToCat ` G ) )
grptcmon.g 
|- ( ph -> G e. Grp )
grptcmon.b 
|- ( ph -> B = ( Base ` C ) )
grptcmon.x 
|- ( ph -> X e. B )
grptcmon.y 
|- ( ph -> Y e. B )
grptcmon.h 
|- ( ph -> H = ( Hom ` C ) )
grptcmon.m 
|- ( ph -> M = ( Mono ` C ) )
Assertion grptcmon 
|- ( ph -> ( X M Y ) = ( X H Y ) )

Proof

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