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 33324
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 33320 . . . . . . . 8 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → (𝐹𝑊) = 𝑈)
43sneqd 4160 . . . . . . 7 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → {(𝐹𝑊)} = {𝑈})
5 grpkerinj.1 . . . . . . . . . 10 𝑋 = ran 𝐺
6 grpkerinj.3 . . . . . . . . . 10 𝑌 = ran 𝐻
75, 6ghomf 33321 . . . . . . . . 9 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → 𝐹:𝑋𝑌)
8 ffn 6002 . . . . . . . . 9 (𝐹:𝑋𝑌𝐹 Fn 𝑋)
97, 8syl 17 . . . . . . . 8 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → 𝐹 Fn 𝑋)
105, 1grpoidcl 27217 . . . . . . . . 9 (𝐺 ∈ GrpOp → 𝑊𝑋)
11103ad2ant1 1080 . . . . . . . 8 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → 𝑊𝑋)
12 fnsnfv 6215 . . . . . . . 8 ((𝐹 Fn 𝑋𝑊𝑋) → {(𝐹𝑊)} = (𝐹 “ {𝑊}))
139, 11, 12syl2anc 692 . . . . . . 7 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → {(𝐹𝑊)} = (𝐹 “ {𝑊}))
144, 13eqtr3d 2657 . . . . . 6 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → {𝑈} = (𝐹 “ {𝑊}))
1514imaeq2d 5425 . . . . 5 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → (𝐹 “ {𝑈}) = (𝐹 “ (𝐹 “ {𝑊})))
1615adantl 482 . . . 4 ((𝐹:𝑋1-1𝑌 ∧ (𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻))) → (𝐹 “ {𝑈}) = (𝐹 “ (𝐹 “ {𝑊})))
1710snssd 4309 . . . . . 6 (𝐺 ∈ GrpOp → {𝑊} ⊆ 𝑋)
18173ad2ant1 1080 . . . . 5 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → {𝑊} ⊆ 𝑋)
19 f1imacnv 6110 . . . . 5 ((𝐹:𝑋1-1𝑌 ∧ {𝑊} ⊆ 𝑋) → (𝐹 “ (𝐹 “ {𝑊})) = {𝑊})
2018, 19sylan2 491 . . . 4 ((𝐹:𝑋1-1𝑌 ∧ (𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻))) → (𝐹 “ (𝐹 “ {𝑊})) = {𝑊})
2116, 20eqtrd 2655 . . 3 ((𝐹:𝑋1-1𝑌 ∧ (𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻))) → (𝐹 “ {𝑈}) = {𝑊})
2221expcom 451 . 2 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → (𝐹:𝑋1-1𝑌 → (𝐹 “ {𝑈}) = {𝑊}))
237adantr 481 . . . 4 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) → 𝐹:𝑋𝑌)
24 simpl2 1063 . . . . . . . 8 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → 𝐻 ∈ GrpOp)
257ffvelrnda 6315 . . . . . . . . 9 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ 𝑥𝑋) → (𝐹𝑥) ∈ 𝑌)
2625adantrr 752 . . . . . . . 8 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → (𝐹𝑥) ∈ 𝑌)
277ffvelrnda 6315 . . . . . . . . 9 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ 𝑦𝑋) → (𝐹𝑦) ∈ 𝑌)
2827adantrl 751 . . . . . . . 8 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → (𝐹𝑦) ∈ 𝑌)
29 eqid 2621 . . . . . . . . 9 ( /𝑔𝐻) = ( /𝑔𝐻)
306, 2, 29grpoeqdivid 33312 . . . . . . . 8 ((𝐻 ∈ GrpOp ∧ (𝐹𝑥) ∈ 𝑌 ∧ (𝐹𝑦) ∈ 𝑌) → ((𝐹𝑥) = (𝐹𝑦) ↔ ((𝐹𝑥)( /𝑔𝐻)(𝐹𝑦)) = 𝑈))
3124, 26, 28, 30syl3anc 1323 . . . . . . 7 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → ((𝐹𝑥) = (𝐹𝑦) ↔ ((𝐹𝑥)( /𝑔𝐻)(𝐹𝑦)) = 𝑈))
3231adantlr 750 . . . . . 6 ((((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) ∧ (𝑥𝑋𝑦𝑋)) → ((𝐹𝑥) = (𝐹𝑦) ↔ ((𝐹𝑥)( /𝑔𝐻)(𝐹𝑦)) = 𝑈))
33 eqid 2621 . . . . . . . . . 10 ( /𝑔𝐺) = ( /𝑔𝐺)
345, 33, 29ghomdiv 33323 . . . . . . . . 9 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → (𝐹‘(𝑥( /𝑔𝐺)𝑦)) = ((𝐹𝑥)( /𝑔𝐻)(𝐹𝑦)))
3534adantlr 750 . . . . . . . 8 ((((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) ∧ (𝑥𝑋𝑦𝑋)) → (𝐹‘(𝑥( /𝑔𝐺)𝑦)) = ((𝐹𝑥)( /𝑔𝐻)(𝐹𝑦)))
3635eqeq1d 2623 . . . . . . 7 ((((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) ∧ (𝑥𝑋𝑦𝑋)) → ((𝐹‘(𝑥( /𝑔𝐺)𝑦)) = 𝑈 ↔ ((𝐹𝑥)( /𝑔𝐻)(𝐹𝑦)) = 𝑈))
37 fvex 6158 . . . . . . . . . . 11 (GId‘𝐻) ∈ V
382, 37eqeltri 2694 . . . . . . . . . 10 𝑈 ∈ V
3938snid 4179 . . . . . . . . 9 𝑈 ∈ {𝑈}
40 eleq1 2686 . . . . . . . . 9 ((𝐹‘(𝑥( /𝑔𝐺)𝑦)) = 𝑈 → ((𝐹‘(𝑥( /𝑔𝐺)𝑦)) ∈ {𝑈} ↔ 𝑈 ∈ {𝑈}))
4139, 40mpbiri 248 . . . . . . . 8 ((𝐹‘(𝑥( /𝑔𝐺)𝑦)) = 𝑈 → (𝐹‘(𝑥( /𝑔𝐺)𝑦)) ∈ {𝑈})
42 ffun 6005 . . . . . . . . . . . . . 14 (𝐹:𝑋𝑌 → Fun 𝐹)
437, 42syl 17 . . . . . . . . . . . . 13 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → Fun 𝐹)
4443adantr 481 . . . . . . . . . . . 12 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → Fun 𝐹)
455, 33grpodivcl 27242 . . . . . . . . . . . . . . 15 ((𝐺 ∈ GrpOp ∧ 𝑥𝑋𝑦𝑋) → (𝑥( /𝑔𝐺)𝑦) ∈ 𝑋)
46453expb 1263 . . . . . . . . . . . . . 14 ((𝐺 ∈ GrpOp ∧ (𝑥𝑋𝑦𝑋)) → (𝑥( /𝑔𝐺)𝑦) ∈ 𝑋)
47463ad2antl1 1221 . . . . . . . . . . . . 13 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥( /𝑔𝐺)𝑦) ∈ 𝑋)
48 fdm 6008 . . . . . . . . . . . . . . 15 (𝐹:𝑋𝑌 → dom 𝐹 = 𝑋)
497, 48syl 17 . . . . . . . . . . . . . 14 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → dom 𝐹 = 𝑋)
5049adantr 481 . . . . . . . . . . . . 13 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → dom 𝐹 = 𝑋)
5147, 50eleqtrrd 2701 . . . . . . . . . . . 12 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥( /𝑔𝐺)𝑦) ∈ dom 𝐹)
52 fvimacnv 6288 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ (𝑥( /𝑔𝐺)𝑦) ∈ dom 𝐹) → ((𝐹‘(𝑥( /𝑔𝐺)𝑦)) ∈ {𝑈} ↔ (𝑥( /𝑔𝐺)𝑦) ∈ (𝐹 “ {𝑈})))
5344, 51, 52syl2anc 692 . . . . . . . . . . 11 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → ((𝐹‘(𝑥( /𝑔𝐺)𝑦)) ∈ {𝑈} ↔ (𝑥( /𝑔𝐺)𝑦) ∈ (𝐹 “ {𝑈})))
54 eleq2 2687 . . . . . . . . . . 11 ((𝐹 “ {𝑈}) = {𝑊} → ((𝑥( /𝑔𝐺)𝑦) ∈ (𝐹 “ {𝑈}) ↔ (𝑥( /𝑔𝐺)𝑦) ∈ {𝑊}))
5553, 54sylan9bb 735 . . . . . . . . . 10 ((((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) ∧ (𝐹 “ {𝑈}) = {𝑊}) → ((𝐹‘(𝑥( /𝑔𝐺)𝑦)) ∈ {𝑈} ↔ (𝑥( /𝑔𝐺)𝑦) ∈ {𝑊}))
5655an32s 845 . . . . . . . . 9 ((((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) ∧ (𝑥𝑋𝑦𝑋)) → ((𝐹‘(𝑥( /𝑔𝐺)𝑦)) ∈ {𝑈} ↔ (𝑥( /𝑔𝐺)𝑦) ∈ {𝑊}))
57 elsni 4165 . . . . . . . . . . 11 ((𝑥( /𝑔𝐺)𝑦) ∈ {𝑊} → (𝑥( /𝑔𝐺)𝑦) = 𝑊)
585, 1, 33grpoeqdivid 33312 . . . . . . . . . . . . . 14 ((𝐺 ∈ GrpOp ∧ 𝑥𝑋𝑦𝑋) → (𝑥 = 𝑦 ↔ (𝑥( /𝑔𝐺)𝑦) = 𝑊))
5958biimprd 238 . . . . . . . . . . . . 13 ((𝐺 ∈ GrpOp ∧ 𝑥𝑋𝑦𝑋) → ((𝑥( /𝑔𝐺)𝑦) = 𝑊𝑥 = 𝑦))
60593expb 1263 . . . . . . . . . . . 12 ((𝐺 ∈ GrpOp ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥( /𝑔𝐺)𝑦) = 𝑊𝑥 = 𝑦))
61603ad2antl1 1221 . . . . . . . . . . 11 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥( /𝑔𝐺)𝑦) = 𝑊𝑥 = 𝑦))
6257, 61syl5 34 . . . . . . . . . 10 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥( /𝑔𝐺)𝑦) ∈ {𝑊} → 𝑥 = 𝑦))
6362adantlr 750 . . . . . . . . 9 ((((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥( /𝑔𝐺)𝑦) ∈ {𝑊} → 𝑥 = 𝑦))
6456, 63sylbid 230 . . . . . . . 8 ((((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) ∧ (𝑥𝑋𝑦𝑋)) → ((𝐹‘(𝑥( /𝑔𝐺)𝑦)) ∈ {𝑈} → 𝑥 = 𝑦))
6541, 64syl5 34 . . . . . . 7 ((((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) ∧ (𝑥𝑋𝑦𝑋)) → ((𝐹‘(𝑥( /𝑔𝐺)𝑦)) = 𝑈𝑥 = 𝑦))
6636, 65sylbird 250 . . . . . 6 ((((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) ∧ (𝑥𝑋𝑦𝑋)) → (((𝐹𝑥)( /𝑔𝐻)(𝐹𝑦)) = 𝑈𝑥 = 𝑦))
6732, 66sylbid 230 . . . . 5 ((((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) ∧ (𝑥𝑋𝑦𝑋)) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
6867ralrimivva 2965 . . . 4 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) → ∀𝑥𝑋𝑦𝑋 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
69 dff13 6466 . . . 4 (𝐹:𝑋1-1𝑌 ↔ (𝐹:𝑋𝑌 ∧ ∀𝑥𝑋𝑦𝑋 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
7023, 68, 69sylanbrc 697 . . 3 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐹 “ {𝑈}) = {𝑊}) → 𝐹:𝑋1-1𝑌)
7170ex 450 . 2 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → ((𝐹 “ {𝑈}) = {𝑊} → 𝐹:𝑋1-1𝑌))
7222, 71impbid 202 1 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → (𝐹:𝑋1-1𝑌 ↔ (𝐹 “ {𝑈}) = {𝑊}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wral 2907  Vcvv 3186  wss 3555  {csn 4148  ccnv 5073  dom cdm 5074  ran crn 5075  cima 5077  Fun wfun 5841   Fn wfn 5842  wf 5843  1-1wf1 5844  cfv 5847  (class class class)co 6604  GrpOpcgr 27192  GIdcgi 27193   /𝑔 cgs 27195   GrpOpHom cghomOLD 33314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-1st 7113  df-2nd 7114  df-grpo 27196  df-gid 27197  df-ginv 27198  df-gdiv 27199  df-ghomOLD 33315
This theorem is referenced by:  rngokerinj  33406
  Copyright terms: Public domain W3C validator