# Metamath Proof Explorer

## Theorem grpokerinj

Description: A group homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011)

Ref Expression
Hypotheses grpkerinj.1 ${⊢}{X}=\mathrm{ran}{G}$
grpkerinj.2 ${⊢}{W}=\mathrm{GId}\left({G}\right)$
grpkerinj.3 ${⊢}{Y}=\mathrm{ran}{H}$
grpkerinj.4 ${⊢}{U}=\mathrm{GId}\left({H}\right)$
Assertion grpokerinj ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to \left({F}:{X}\underset{1-1}{⟶}{Y}↔{{F}}^{-1}\left[\left\{{U}\right\}\right]=\left\{{W}\right\}\right)$

### Proof

Step Hyp Ref Expression
1 grpkerinj.1 ${⊢}{X}=\mathrm{ran}{G}$
2 grpkerinj.2 ${⊢}{W}=\mathrm{GId}\left({G}\right)$
3 grpkerinj.3 ${⊢}{Y}=\mathrm{ran}{H}$
4 grpkerinj.4 ${⊢}{U}=\mathrm{GId}\left({H}\right)$
5 2 4 ghomidOLD ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to {F}\left({W}\right)={U}$
6 5 sneqd ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to \left\{{F}\left({W}\right)\right\}=\left\{{U}\right\}$
7 1 3 ghomf ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to {F}:{X}⟶{Y}$
8 7 ffnd ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to {F}Fn{X}$
9 1 2 grpoidcl ${⊢}{G}\in \mathrm{GrpOp}\to {W}\in {X}$
10 9 3ad2ant1 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to {W}\in {X}$
11 fnsnfv ${⊢}\left({F}Fn{X}\wedge {W}\in {X}\right)\to \left\{{F}\left({W}\right)\right\}={F}\left[\left\{{W}\right\}\right]$
12 8 10 11 syl2anc ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to \left\{{F}\left({W}\right)\right\}={F}\left[\left\{{W}\right\}\right]$
13 6 12 eqtr3d ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to \left\{{U}\right\}={F}\left[\left\{{W}\right\}\right]$
14 13 imaeq2d ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to {{F}}^{-1}\left[\left\{{U}\right\}\right]={{F}}^{-1}\left[{F}\left[\left\{{W}\right\}\right]\right]$
15 14 adantl ${⊢}\left({F}:{X}\underset{1-1}{⟶}{Y}\wedge \left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\right)\to {{F}}^{-1}\left[\left\{{U}\right\}\right]={{F}}^{-1}\left[{F}\left[\left\{{W}\right\}\right]\right]$
16 9 snssd ${⊢}{G}\in \mathrm{GrpOp}\to \left\{{W}\right\}\subseteq {X}$
17 16 3ad2ant1 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to \left\{{W}\right\}\subseteq {X}$
18 f1imacnv ${⊢}\left({F}:{X}\underset{1-1}{⟶}{Y}\wedge \left\{{W}\right\}\subseteq {X}\right)\to {{F}}^{-1}\left[{F}\left[\left\{{W}\right\}\right]\right]=\left\{{W}\right\}$
19 17 18 sylan2 ${⊢}\left({F}:{X}\underset{1-1}{⟶}{Y}\wedge \left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\right)\to {{F}}^{-1}\left[{F}\left[\left\{{W}\right\}\right]\right]=\left\{{W}\right\}$
20 15 19 eqtrd ${⊢}\left({F}:{X}\underset{1-1}{⟶}{Y}\wedge \left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\right)\to {{F}}^{-1}\left[\left\{{U}\right\}\right]=\left\{{W}\right\}$
21 20 expcom ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to \left({F}:{X}\underset{1-1}{⟶}{Y}\to {{F}}^{-1}\left[\left\{{U}\right\}\right]=\left\{{W}\right\}\right)$
22 7 adantr ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge {{F}}^{-1}\left[\left\{{U}\right\}\right]=\left\{{W}\right\}\right)\to {F}:{X}⟶{Y}$
23 simpl2 ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {H}\in \mathrm{GrpOp}$
24 7 ffvelrnda ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge {x}\in {X}\right)\to {F}\left({x}\right)\in {Y}$
25 24 adantrr ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {F}\left({x}\right)\in {Y}$
26 7 ffvelrnda ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge {y}\in {X}\right)\to {F}\left({y}\right)\in {Y}$
27 26 adantrl ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {F}\left({y}\right)\in {Y}$
28 eqid ${⊢}{/}_{g}\left({H}\right)={/}_{g}\left({H}\right)$
29 3 4 28 grpoeqdivid ${⊢}\left({H}\in \mathrm{GrpOp}\wedge {F}\left({x}\right)\in {Y}\wedge {F}\left({y}\right)\in {Y}\right)\to \left({F}\left({x}\right)={F}\left({y}\right)↔{F}\left({x}\right){/}_{g}\left({H}\right){F}\left({y}\right)={U}\right)$
30 23 25 27 29 syl3anc ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left({F}\left({x}\right)={F}\left({y}\right)↔{F}\left({x}\right){/}_{g}\left({H}\right){F}\left({y}\right)={U}\right)$
31 30 adantlr ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge {{F}}^{-1}\left[\left\{{U}\right\}\right]=\left\{{W}\right\}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left({F}\left({x}\right)={F}\left({y}\right)↔{F}\left({x}\right){/}_{g}\left({H}\right){F}\left({y}\right)={U}\right)$
32 eqid ${⊢}{/}_{g}\left({G}\right)={/}_{g}\left({G}\right)$
33 1 32 28 ghomdiv ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {F}\left({x}{/}_{g}\left({G}\right){y}\right)={F}\left({x}\right){/}_{g}\left({H}\right){F}\left({y}\right)$
34 33 adantlr ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge {{F}}^{-1}\left[\left\{{U}\right\}\right]=\left\{{W}\right\}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {F}\left({x}{/}_{g}\left({G}\right){y}\right)={F}\left({x}\right){/}_{g}\left({H}\right){F}\left({y}\right)$
35 34 eqeq1d ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge {{F}}^{-1}\left[\left\{{U}\right\}\right]=\left\{{W}\right\}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left({F}\left({x}{/}_{g}\left({G}\right){y}\right)={U}↔{F}\left({x}\right){/}_{g}\left({H}\right){F}\left({y}\right)={U}\right)$
36 4 fvexi ${⊢}{U}\in \mathrm{V}$
37 36 snid ${⊢}{U}\in \left\{{U}\right\}$
38 eleq1 ${⊢}{F}\left({x}{/}_{g}\left({G}\right){y}\right)={U}\to \left({F}\left({x}{/}_{g}\left({G}\right){y}\right)\in \left\{{U}\right\}↔{U}\in \left\{{U}\right\}\right)$
39 37 38 mpbiri ${⊢}{F}\left({x}{/}_{g}\left({G}\right){y}\right)={U}\to {F}\left({x}{/}_{g}\left({G}\right){y}\right)\in \left\{{U}\right\}$
40 7 ffund ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to \mathrm{Fun}{F}$
41 40 adantr ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \mathrm{Fun}{F}$
42 1 32 grpodivcl ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {x}\in {X}\wedge {y}\in {X}\right)\to {x}{/}_{g}\left({G}\right){y}\in {X}$
43 42 3expb ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{/}_{g}\left({G}\right){y}\in {X}$
44 43 3ad2antl1 ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{/}_{g}\left({G}\right){y}\in {X}$
45 7 fdmd ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to \mathrm{dom}{F}={X}$
46 45 adantr ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \mathrm{dom}{F}={X}$
47 44 46 eleqtrrd ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{/}_{g}\left({G}\right){y}\in \mathrm{dom}{F}$
48 fvimacnv ${⊢}\left(\mathrm{Fun}{F}\wedge {x}{/}_{g}\left({G}\right){y}\in \mathrm{dom}{F}\right)\to \left({F}\left({x}{/}_{g}\left({G}\right){y}\right)\in \left\{{U}\right\}↔{x}{/}_{g}\left({G}\right){y}\in {{F}}^{-1}\left[\left\{{U}\right\}\right]\right)$
49 41 47 48 syl2anc ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left({F}\left({x}{/}_{g}\left({G}\right){y}\right)\in \left\{{U}\right\}↔{x}{/}_{g}\left({G}\right){y}\in {{F}}^{-1}\left[\left\{{U}\right\}\right]\right)$
50 eleq2 ${⊢}{{F}}^{-1}\left[\left\{{U}\right\}\right]=\left\{{W}\right\}\to \left({x}{/}_{g}\left({G}\right){y}\in {{F}}^{-1}\left[\left\{{U}\right\}\right]↔{x}{/}_{g}\left({G}\right){y}\in \left\{{W}\right\}\right)$
51 49 50 sylan9bb ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge {{F}}^{-1}\left[\left\{{U}\right\}\right]=\left\{{W}\right\}\right)\to \left({F}\left({x}{/}_{g}\left({G}\right){y}\right)\in \left\{{U}\right\}↔{x}{/}_{g}\left({G}\right){y}\in \left\{{W}\right\}\right)$
52 51 an32s ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge {{F}}^{-1}\left[\left\{{U}\right\}\right]=\left\{{W}\right\}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left({F}\left({x}{/}_{g}\left({G}\right){y}\right)\in \left\{{U}\right\}↔{x}{/}_{g}\left({G}\right){y}\in \left\{{W}\right\}\right)$
53 elsni ${⊢}{x}{/}_{g}\left({G}\right){y}\in \left\{{W}\right\}\to {x}{/}_{g}\left({G}\right){y}={W}$
54 1 2 32 grpoeqdivid ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {x}\in {X}\wedge {y}\in {X}\right)\to \left({x}={y}↔{x}{/}_{g}\left({G}\right){y}={W}\right)$
55 54 biimprd ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {x}\in {X}\wedge {y}\in {X}\right)\to \left({x}{/}_{g}\left({G}\right){y}={W}\to {x}={y}\right)$
56 55 3expb ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left({x}{/}_{g}\left({G}\right){y}={W}\to {x}={y}\right)$
57 56 3ad2antl1 ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left({x}{/}_{g}\left({G}\right){y}={W}\to {x}={y}\right)$
58 53 57 syl5 ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left({x}{/}_{g}\left({G}\right){y}\in \left\{{W}\right\}\to {x}={y}\right)$
59 58 adantlr ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge {{F}}^{-1}\left[\left\{{U}\right\}\right]=\left\{{W}\right\}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left({x}{/}_{g}\left({G}\right){y}\in \left\{{W}\right\}\to {x}={y}\right)$
60 52 59 sylbid ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge {{F}}^{-1}\left[\left\{{U}\right\}\right]=\left\{{W}\right\}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left({F}\left({x}{/}_{g}\left({G}\right){y}\right)\in \left\{{U}\right\}\to {x}={y}\right)$
61 39 60 syl5 ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge {{F}}^{-1}\left[\left\{{U}\right\}\right]=\left\{{W}\right\}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left({F}\left({x}{/}_{g}\left({G}\right){y}\right)={U}\to {x}={y}\right)$
62 35 61 sylbird ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge {{F}}^{-1}\left[\left\{{U}\right\}\right]=\left\{{W}\right\}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left({F}\left({x}\right){/}_{g}\left({H}\right){F}\left({y}\right)={U}\to {x}={y}\right)$
63 31 62 sylbid ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge {{F}}^{-1}\left[\left\{{U}\right\}\right]=\left\{{W}\right\}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)$
64 63 ralrimivva ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge {{F}}^{-1}\left[\left\{{U}\right\}\right]=\left\{{W}\right\}\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)$
65 dff13 ${⊢}{F}:{X}\underset{1-1}{⟶}{Y}↔\left({F}:{X}⟶{Y}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)\right)$
66 22 64 65 sylanbrc ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge {{F}}^{-1}\left[\left\{{U}\right\}\right]=\left\{{W}\right\}\right)\to {F}:{X}\underset{1-1}{⟶}{Y}$
67 66 ex ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to \left({{F}}^{-1}\left[\left\{{U}\right\}\right]=\left\{{W}\right\}\to {F}:{X}\underset{1-1}{⟶}{Y}\right)$
68 21 67 impbid ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to \left({F}:{X}\underset{1-1}{⟶}{Y}↔{{F}}^{-1}\left[\left\{{U}\right\}\right]=\left\{{W}\right\}\right)$