Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  grpokerinj Structured version   Visualization version   GIF version

Theorem grpokerinj 32862
Description: A group homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011.)
Hypotheses
Ref Expression
grpkerinj.1 𝑋 = ran 𝐺
grpkerinj.2 𝑊 = (GId‘𝐺)
grpkerinj.3 𝑌 = ran 𝐻
grpkerinj.4 𝑈 = (GId‘𝐻)
Assertion
Ref Expression
grpokerinj ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → (𝐹:𝑋1-1𝑌 ↔ (𝐹 “ {𝑈}) = {𝑊}))

Proof of Theorem grpokerinj
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 grpkerinj.2 . . . . . . . . 9 𝑊 = (GId‘𝐺)
2 grpkerinj.4 . . . . . . . . 9 𝑈 = (GId‘𝐻)
31, 2ghomidOLD 32858 . . . . . . . 8 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → (𝐹𝑊) = 𝑈)
43sneqd 4137 . . . . . . 7 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → {(𝐹𝑊)} = {𝑈})
5 grpkerinj.1 . . . . . . . . . 10 𝑋 = ran 𝐺
6 grpkerinj.3 . . . . . . . . . 10 𝑌 = ran 𝐻
75, 6ghomf 32859 . . . . . . . . 9 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → 𝐹:𝑋𝑌)
8 ffn 5958 . . . . . . . . 9 (𝐹:𝑋𝑌𝐹 Fn 𝑋)
97, 8syl 17 . . . . . . . 8 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → 𝐹 Fn 𝑋)
105, 1grpoidcl 26752 . . . . . . . . 9 (𝐺 ∈ GrpOp → 𝑊𝑋)
11103ad2ant1 1075 . . . . . . . 8 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → 𝑊𝑋)
12 fnsnfv 6168 . . . . . . . 8 ((𝐹 Fn 𝑋𝑊𝑋) → {(𝐹𝑊)} = (𝐹 “ {𝑊}))
139, 11, 12syl2anc 691 . . . . . . 7 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → {(𝐹𝑊)} = (𝐹 “ {𝑊}))
144, 13eqtr3d 2646 . . . . . 6 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → {𝑈} = (𝐹 “ {𝑊}))
1514imaeq2d 5385 . . . . 5 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → (𝐹 “ {𝑈}) = (𝐹 “ (𝐹 “ {𝑊})))
1615adantl 481 . . . 4 ((𝐹:𝑋1-1𝑌 ∧ (𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻))) → (𝐹 “ {𝑈}) = (𝐹 “ (𝐹 “ {𝑊})))
1710snssd 4281 . . . . . 6 (𝐺 ∈ GrpOp → {𝑊} ⊆ 𝑋)
18173ad2ant1 1075 . . . . 5 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → {𝑊} ⊆ 𝑋)
19 f1imacnv 6066 . . . . 5 ((𝐹:𝑋1-1𝑌 ∧ {𝑊} ⊆ 𝑋) → (𝐹 “ (𝐹 “ {𝑊})) = {𝑊})
2018, 19sylan2 490 . . . 4 ((𝐹:𝑋1-1𝑌 ∧ (𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻))) → (𝐹 “ (𝐹 “ {𝑊})) = {𝑊})
2116, 20eqtrd 2644 . . 3 ((𝐹:𝑋1-1𝑌 ∧ (𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻))) → (𝐹 “ {𝑈}) = {𝑊})
2221expcom 450 . 2 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → (𝐹:𝑋1-1𝑌 → (𝐹 “ {𝑈}) = {𝑊}))
237adantr 480 . . . 4 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) → 𝐹:𝑋𝑌)
24 simpl2 1058 . . . . . . . 8 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → 𝐻 ∈ GrpOp)
257ffvelrnda 6267 . . . . . . . . 9 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ 𝑥𝑋) → (𝐹𝑥) ∈ 𝑌)
2625adantrr 749 . . . . . . . 8 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → (𝐹𝑥) ∈ 𝑌)
277ffvelrnda 6267 . . . . . . . . 9 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ 𝑦𝑋) → (𝐹𝑦) ∈ 𝑌)
2827adantrl 748 . . . . . . . 8 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → (𝐹𝑦) ∈ 𝑌)
29 eqid 2610 . . . . . . . . 9 ( /𝑔𝐻) = ( /𝑔𝐻)
306, 2, 29grpoeqdivid 32850 . . . . . . . 8 ((𝐻 ∈ GrpOp ∧ (𝐹𝑥) ∈ 𝑌 ∧ (𝐹𝑦) ∈ 𝑌) → ((𝐹𝑥) = (𝐹𝑦) ↔ ((𝐹𝑥)( /𝑔𝐻)(𝐹𝑦)) = 𝑈))
3124, 26, 28, 30syl3anc 1318 . . . . . . 7 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → ((𝐹𝑥) = (𝐹𝑦) ↔ ((𝐹𝑥)( /𝑔𝐻)(𝐹𝑦)) = 𝑈))
3231adantlr 747 . . . . . 6 ((((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) ∧ (𝑥𝑋𝑦𝑋)) → ((𝐹𝑥) = (𝐹𝑦) ↔ ((𝐹𝑥)( /𝑔𝐻)(𝐹𝑦)) = 𝑈))
33 eqid 2610 . . . . . . . . . 10 ( /𝑔𝐺) = ( /𝑔𝐺)
345, 33, 29ghomdiv 32861 . . . . . . . . 9 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → (𝐹‘(𝑥( /𝑔𝐺)𝑦)) = ((𝐹𝑥)( /𝑔𝐻)(𝐹𝑦)))
3534adantlr 747 . . . . . . . 8 ((((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) ∧ (𝑥𝑋𝑦𝑋)) → (𝐹‘(𝑥( /𝑔𝐺)𝑦)) = ((𝐹𝑥)( /𝑔𝐻)(𝐹𝑦)))
3635eqeq1d 2612 . . . . . . 7 ((((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) ∧ (𝑥𝑋𝑦𝑋)) → ((𝐹‘(𝑥( /𝑔𝐺)𝑦)) = 𝑈 ↔ ((𝐹𝑥)( /𝑔𝐻)(𝐹𝑦)) = 𝑈))
37 fvex 6113 . . . . . . . . . . 11 (GId‘𝐻) ∈ V
382, 37eqeltri 2684 . . . . . . . . . 10 𝑈 ∈ V
3938snid 4155 . . . . . . . . 9 𝑈 ∈ {𝑈}
40 eleq1 2676 . . . . . . . . 9 ((𝐹‘(𝑥( /𝑔𝐺)𝑦)) = 𝑈 → ((𝐹‘(𝑥( /𝑔𝐺)𝑦)) ∈ {𝑈} ↔ 𝑈 ∈ {𝑈}))
4139, 40mpbiri 247 . . . . . . . 8 ((𝐹‘(𝑥( /𝑔𝐺)𝑦)) = 𝑈 → (𝐹‘(𝑥( /𝑔𝐺)𝑦)) ∈ {𝑈})
42 ffun 5961 . . . . . . . . . . . . . 14 (𝐹:𝑋𝑌 → Fun 𝐹)
437, 42syl 17 . . . . . . . . . . . . 13 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → Fun 𝐹)
4443adantr 480 . . . . . . . . . . . 12 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → Fun 𝐹)
455, 33grpodivcl 26777 . . . . . . . . . . . . . . 15 ((𝐺 ∈ GrpOp ∧ 𝑥𝑋𝑦𝑋) → (𝑥( /𝑔𝐺)𝑦) ∈ 𝑋)
46453expb 1258 . . . . . . . . . . . . . 14 ((𝐺 ∈ GrpOp ∧ (𝑥𝑋𝑦𝑋)) → (𝑥( /𝑔𝐺)𝑦) ∈ 𝑋)
47463ad2antl1 1216 . . . . . . . . . . . . 13 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥( /𝑔𝐺)𝑦) ∈ 𝑋)
48 fdm 5964 . . . . . . . . . . . . . . 15 (𝐹:𝑋𝑌 → dom 𝐹 = 𝑋)
497, 48syl 17 . . . . . . . . . . . . . 14 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → dom 𝐹 = 𝑋)
5049adantr 480 . . . . . . . . . . . . 13 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → dom 𝐹 = 𝑋)
5147, 50eleqtrrd 2691 . . . . . . . . . . . 12 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥( /𝑔𝐺)𝑦) ∈ dom 𝐹)
52 fvimacnv 6240 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ (𝑥( /𝑔𝐺)𝑦) ∈ dom 𝐹) → ((𝐹‘(𝑥( /𝑔𝐺)𝑦)) ∈ {𝑈} ↔ (𝑥( /𝑔𝐺)𝑦) ∈ (𝐹 “ {𝑈})))
5344, 51, 52syl2anc 691 . . . . . . . . . . 11 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → ((𝐹‘(𝑥( /𝑔𝐺)𝑦)) ∈ {𝑈} ↔ (𝑥( /𝑔𝐺)𝑦) ∈ (𝐹 “ {𝑈})))
54 eleq2 2677 . . . . . . . . . . 11 ((𝐹 “ {𝑈}) = {𝑊} → ((𝑥( /𝑔𝐺)𝑦) ∈ (𝐹 “ {𝑈}) ↔ (𝑥( /𝑔𝐺)𝑦) ∈ {𝑊}))
5553, 54sylan9bb 732 . . . . . . . . . 10 ((((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) ∧ (𝐹 “ {𝑈}) = {𝑊}) → ((𝐹‘(𝑥( /𝑔𝐺)𝑦)) ∈ {𝑈} ↔ (𝑥( /𝑔𝐺)𝑦) ∈ {𝑊}))
5655an32s 842 . . . . . . . . 9 ((((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) ∧ (𝑥𝑋𝑦𝑋)) → ((𝐹‘(𝑥( /𝑔𝐺)𝑦)) ∈ {𝑈} ↔ (𝑥( /𝑔𝐺)𝑦) ∈ {𝑊}))
57 elsni 4142 . . . . . . . . . . 11 ((𝑥( /𝑔𝐺)𝑦) ∈ {𝑊} → (𝑥( /𝑔𝐺)𝑦) = 𝑊)
585, 1, 33grpoeqdivid 32850 . . . . . . . . . . . . . 14 ((𝐺 ∈ GrpOp ∧ 𝑥𝑋𝑦𝑋) → (𝑥 = 𝑦 ↔ (𝑥( /𝑔𝐺)𝑦) = 𝑊))
5958biimprd 237 . . . . . . . . . . . . 13 ((𝐺 ∈ GrpOp ∧ 𝑥𝑋𝑦𝑋) → ((𝑥( /𝑔𝐺)𝑦) = 𝑊𝑥 = 𝑦))
60593expb 1258 . . . . . . . . . . . 12 ((𝐺 ∈ GrpOp ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥( /𝑔𝐺)𝑦) = 𝑊𝑥 = 𝑦))
61603ad2antl1 1216 . . . . . . . . . . 11 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥( /𝑔𝐺)𝑦) = 𝑊𝑥 = 𝑦))
6257, 61syl5 33 . . . . . . . . . 10 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥( /𝑔𝐺)𝑦) ∈ {𝑊} → 𝑥 = 𝑦))
6362adantlr 747 . . . . . . . . 9 ((((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥( /𝑔𝐺)𝑦) ∈ {𝑊} → 𝑥 = 𝑦))
6456, 63sylbid 229 . . . . . . . 8 ((((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) ∧ (𝑥𝑋𝑦𝑋)) → ((𝐹‘(𝑥( /𝑔𝐺)𝑦)) ∈ {𝑈} → 𝑥 = 𝑦))
6541, 64syl5 33 . . . . . . 7 ((((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) ∧ (𝑥𝑋𝑦𝑋)) → ((𝐹‘(𝑥( /𝑔𝐺)𝑦)) = 𝑈𝑥 = 𝑦))
6636, 65sylbird 249 . . . . . 6 ((((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) ∧ (𝑥𝑋𝑦𝑋)) → (((𝐹𝑥)( /𝑔𝐻)(𝐹𝑦)) = 𝑈𝑥 = 𝑦))
6732, 66sylbid 229 . . . . 5 ((((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) ∧ (𝑥𝑋𝑦𝑋)) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
6867ralrimivva 2954 . . . 4 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) → ∀𝑥𝑋𝑦𝑋 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
69 dff13 6416 . . . 4 (𝐹:𝑋1-1𝑌 ↔ (𝐹:𝑋𝑌 ∧ ∀𝑥𝑋𝑦𝑋 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
7023, 68, 69sylanbrc 695 . . 3 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) → 𝐹:𝑋1-1𝑌)
7170ex 449 . 2 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → ((𝐹 “ {𝑈}) = {𝑊} → 𝐹:𝑋1-1𝑌))
7222, 71impbid 201 1 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → (𝐹:𝑋1-1𝑌 ↔ (𝐹 “ {𝑈}) = {𝑊}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383  w3a 1031   = wceq 1475  wcel 1977  wral 2896  Vcvv 3173  wss 3540  {csn 4125  ccnv 5037  dom cdm 5038  ran crn 5039  cima 5041  Fun wfun 5798   Fn wfn 5799  wf 5800  1-1wf1 5801  cfv 5804  (class class class)co 6549  GrpOpcgr 26727  GIdcgi 26728   /𝑔 cgs 26730   GrpOpHom cghomOLD 32852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-grpo 26731  df-gid 26732  df-ginv 26733  df-gdiv 26734  df-ghomOLD 32853
This theorem is referenced by:  rngokerinj  32944
  Copyright terms: Public domain W3C validator