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 φC=MndToCatG
grptcmon.g φGGrp
grptcmon.b φB=BaseC
grptcmon.x φXB
grptcmon.y φYB
grptcmon.h φH=HomC
grptcmon.m φM=MonoC
Assertion grptcmon φXMY=XHY

Proof

Step Hyp Ref Expression
1 grptcmon.c φC=MndToCatG
2 grptcmon.g φGGrp
3 grptcmon.b φB=BaseC
4 grptcmon.x φXB
5 grptcmon.y φYB
6 grptcmon.h φH=HomC
7 grptcmon.m φM=MonoC
8 eqid BaseC=BaseC
9 eqid HomC=HomC
10 eqid compC=compC
11 eqid MonoC=MonoC
12 2 grpmndd φGMnd
13 1 12 mndtccat φCCat
14 4 3 eleqtrd φXBaseC
15 5 3 eleqtrd φYBaseC
16 8 9 10 11 13 14 15 ismon2 φfXMonoCYfXHomCYzBaseCgzHomCXhzHomCXfzXcompCYg=fzXcompCYhg=h
17 1 ad2antrr φfXHomCYzBaseCgzHomCXhzHomCXC=MndToCatG
18 12 ad2antrr φfXHomCYzBaseCgzHomCXhzHomCXGMnd
19 3 ad2antrr φfXHomCYzBaseCgzHomCXhzHomCXB=BaseC
20 simpr1 φfXHomCYzBaseCgzHomCXhzHomCXzBaseC
21 20 19 eleqtrrd φfXHomCYzBaseCgzHomCXhzHomCXzB
22 4 ad2antrr φfXHomCYzBaseCgzHomCXhzHomCXXB
23 5 ad2antrr φfXHomCYzBaseCgzHomCXhzHomCXYB
24 eqidd φfXHomCYzBaseCgzHomCXhzHomCXcompC=compC
25 eqidd φfXHomCYzBaseCgzHomCXhzHomCXzXcompCY=zXcompCY
26 17 18 19 21 22 23 24 25 mndtcco2 φfXHomCYzBaseCgzHomCXhzHomCXfzXcompCYg=f+Gg
27 17 18 19 21 22 23 24 25 mndtcco2 φfXHomCYzBaseCgzHomCXhzHomCXfzXcompCYh=f+Gh
28 26 27 eqeq12d φfXHomCYzBaseCgzHomCXhzHomCXfzXcompCYg=fzXcompCYhf+Gg=f+Gh
29 2 ad2antrr φfXHomCYzBaseCgzHomCXhzHomCXGGrp
30 simpr2 φfXHomCYzBaseCgzHomCXhzHomCXgzHomCX
31 eqidd φfXHomCYzBaseCgzHomCXhzHomCXHomC=HomC
32 17 18 19 21 22 31 mndtchom φfXHomCYzBaseCgzHomCXhzHomCXzHomCX=BaseG
33 30 32 eleqtrd φfXHomCYzBaseCgzHomCXhzHomCXgBaseG
34 simpr3 φfXHomCYzBaseCgzHomCXhzHomCXhzHomCX
35 34 32 eleqtrd φfXHomCYzBaseCgzHomCXhzHomCXhBaseG
36 simplr φfXHomCYzBaseCgzHomCXhzHomCXfXHomCY
37 17 18 19 22 23 31 mndtchom φfXHomCYzBaseCgzHomCXhzHomCXXHomCY=BaseG
38 36 37 eleqtrd φfXHomCYzBaseCgzHomCXhzHomCXfBaseG
39 eqid BaseG=BaseG
40 eqid +G=+G
41 39 40 grplcan GGrpgBaseGhBaseGfBaseGf+Gg=f+Ghg=h
42 29 33 35 38 41 syl13anc φfXHomCYzBaseCgzHomCXhzHomCXf+Gg=f+Ghg=h
43 28 42 bitrd φfXHomCYzBaseCgzHomCXhzHomCXfzXcompCYg=fzXcompCYhg=h
44 43 biimpd φfXHomCYzBaseCgzHomCXhzHomCXfzXcompCYg=fzXcompCYhg=h
45 44 ralrimivvva φfXHomCYzBaseCgzHomCXhzHomCXfzXcompCYg=fzXcompCYhg=h
46 16 45 mpbiran3d φfXMonoCYfXHomCY
47 46 eqrdv φXMonoCY=XHomCY
48 7 oveqd φXMY=XMonoCY
49 6 oveqd φXHY=XHomCY
50 47 48 49 3eqtr4d φXMY=XHY