Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵) ∧ 𝑥 ∈ (◡𝐹 “ { 0 })) → (𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵)) |
2 | | f1fn 6102 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴) |
3 | 2 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐹 Fn 𝐴) |
4 | | elpreima 6337 |
. . . . . . . . . 10
⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ (◡𝐹 “ { 0 }) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ { 0 }))) |
5 | 3, 4 | syl 17 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵) → (𝑥 ∈ (◡𝐹 “ { 0 }) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ { 0 }))) |
6 | 5 | biimpa 501 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵) ∧ 𝑥 ∈ (◡𝐹 “ { 0 })) → (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ { 0 })) |
7 | 6 | simpld 475 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵) ∧ 𝑥 ∈ (◡𝐹 “ { 0 })) → 𝑥 ∈ 𝐴) |
8 | 6 | simprd 479 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵) ∧ 𝑥 ∈ (◡𝐹 “ { 0 })) → (𝐹‘𝑥) ∈ { 0 }) |
9 | | fvex 6201 |
. . . . . . . . 9
⊢ (𝐹‘𝑥) ∈ V |
10 | 9 | elsn 4192 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) ∈ { 0 } ↔ (𝐹‘𝑥) = 0 ) |
11 | 8, 10 | sylib 208 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵) ∧ 𝑥 ∈ (◡𝐹 “ { 0 })) → (𝐹‘𝑥) = 0 ) |
12 | | kerf1hrm.a |
. . . . . . . . . . 11
⊢ 𝐴 = (Base‘𝑅) |
13 | | kerf1hrm.b |
. . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝑆) |
14 | | kerf1hrm.0 |
. . . . . . . . . . 11
⊢ 0 =
(0g‘𝑆) |
15 | | kerf1hrm.n |
. . . . . . . . . . 11
⊢ 𝑁 = (0g‘𝑅) |
16 | 12, 13, 14, 15 | f1rhm0to0 18740 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 0 ↔ 𝑥 = 𝑁)) |
17 | 16 | biimpd 219 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 0 → 𝑥 = 𝑁)) |
18 | 17 | 3expa 1265 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 0 → 𝑥 = 𝑁)) |
19 | 18 | imp 445 |
. . . . . . 7
⊢ ((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) ∧ (𝐹‘𝑥) = 0 ) → 𝑥 = 𝑁) |
20 | 1, 7, 11, 19 | syl21anc 1325 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵) ∧ 𝑥 ∈ (◡𝐹 “ { 0 })) → 𝑥 = 𝑁) |
21 | 20 | ex 450 |
. . . . 5
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵) → (𝑥 ∈ (◡𝐹 “ { 0 }) → 𝑥 = 𝑁)) |
22 | | velsn 4193 |
. . . . 5
⊢ (𝑥 ∈ {𝑁} ↔ 𝑥 = 𝑁) |
23 | 21, 22 | syl6ibr 242 |
. . . 4
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵) → (𝑥 ∈ (◡𝐹 “ { 0 }) → 𝑥 ∈ {𝑁})) |
24 | 23 | ssrdv 3609 |
. . 3
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵) → (◡𝐹 “ { 0 }) ⊆ {𝑁}) |
25 | | rhmrcl1 18719 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑅 ∈ Ring) |
26 | | ringgrp 18552 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
27 | 12, 15 | grpidcl 17450 |
. . . . . . 7
⊢ (𝑅 ∈ Grp → 𝑁 ∈ 𝐴) |
28 | 25, 26, 27 | 3syl 18 |
. . . . . 6
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑁 ∈ 𝐴) |
29 | | rhmghm 18725 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
30 | 15, 14 | ghmid 17666 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝑅 GrpHom 𝑆) → (𝐹‘𝑁) = 0 ) |
31 | 29, 30 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘𝑁) = 0 ) |
32 | | fvex 6201 |
. . . . . . . 8
⊢ (𝐹‘𝑁) ∈ V |
33 | 32 | elsn 4192 |
. . . . . . 7
⊢ ((𝐹‘𝑁) ∈ { 0 } ↔ (𝐹‘𝑁) = 0 ) |
34 | 31, 33 | sylibr 224 |
. . . . . 6
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘𝑁) ∈ { 0 }) |
35 | 12, 13 | rhmf 18726 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:𝐴⟶𝐵) |
36 | | ffn 6045 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
37 | | elpreima 6337 |
. . . . . . 7
⊢ (𝐹 Fn 𝐴 → (𝑁 ∈ (◡𝐹 “ { 0 }) ↔ (𝑁 ∈ 𝐴 ∧ (𝐹‘𝑁) ∈ { 0 }))) |
38 | 35, 36, 37 | 3syl 18 |
. . . . . 6
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝑁 ∈ (◡𝐹 “ { 0 }) ↔ (𝑁 ∈ 𝐴 ∧ (𝐹‘𝑁) ∈ { 0 }))) |
39 | 28, 34, 38 | mpbir2and 957 |
. . . . 5
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑁 ∈ (◡𝐹 “ { 0 })) |
40 | 39 | snssd 4340 |
. . . 4
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → {𝑁} ⊆ (◡𝐹 “ { 0 })) |
41 | 40 | adantr 481 |
. . 3
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵) → {𝑁} ⊆ (◡𝐹 “ { 0 })) |
42 | 24, 41 | eqssd 3620 |
. 2
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵) → (◡𝐹 “ { 0 }) = {𝑁}) |
43 | 35 | adantr 481 |
. . 3
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (◡𝐹 “ { 0 }) = {𝑁}) → 𝐹:𝐴⟶𝐵) |
44 | 29 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ((◡𝐹 “ { 0 }) = {𝑁} ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
45 | | simpr2l 1120 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ((◡𝐹 “ { 0 }) = {𝑁} ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → 𝑥 ∈ 𝐴) |
46 | | simpr2r 1121 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ((◡𝐹 “ { 0 }) = {𝑁} ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → 𝑦 ∈ 𝐴) |
47 | | simpr3 1069 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ((◡𝐹 “ { 0 }) = {𝑁} ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝐹‘𝑥) = (𝐹‘𝑦)) |
48 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (◡𝐹 “ { 0 }) = (◡𝐹 “ { 0 }) |
49 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(-g‘𝑅) = (-g‘𝑅) |
50 | 12, 14, 48, 49 | ghmeqker 17687 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝑥(-g‘𝑅)𝑦) ∈ (◡𝐹 “ { 0 }))) |
51 | 50 | biimpa 501 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (𝑥(-g‘𝑅)𝑦) ∈ (◡𝐹 “ { 0 })) |
52 | 44, 45, 46, 47, 51 | syl31anc 1329 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ((◡𝐹 “ { 0 }) = {𝑁} ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝑥(-g‘𝑅)𝑦) ∈ (◡𝐹 “ { 0 })) |
53 | | simpr1 1067 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ((◡𝐹 “ { 0 }) = {𝑁} ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (◡𝐹 “ { 0 }) = {𝑁}) |
54 | 52, 53 | eleqtrd 2703 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ((◡𝐹 “ { 0 }) = {𝑁} ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝑥(-g‘𝑅)𝑦) ∈ {𝑁}) |
55 | | ovex 6678 |
. . . . . . . . 9
⊢ (𝑥(-g‘𝑅)𝑦) ∈ V |
56 | 55 | elsn 4192 |
. . . . . . . 8
⊢ ((𝑥(-g‘𝑅)𝑦) ∈ {𝑁} ↔ (𝑥(-g‘𝑅)𝑦) = 𝑁) |
57 | 54, 56 | sylib 208 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ((◡𝐹 “ { 0 }) = {𝑁} ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝑥(-g‘𝑅)𝑦) = 𝑁) |
58 | 25 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ((◡𝐹 “ { 0 }) = {𝑁} ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → 𝑅 ∈ Ring) |
59 | 58, 26 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ((◡𝐹 “ { 0 }) = {𝑁} ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → 𝑅 ∈ Grp) |
60 | 12, 15, 49 | grpsubeq0 17501 |
. . . . . . . 8
⊢ ((𝑅 ∈ Grp ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑥(-g‘𝑅)𝑦) = 𝑁 ↔ 𝑥 = 𝑦)) |
61 | 59, 45, 46, 60 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ((◡𝐹 “ { 0 }) = {𝑁} ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝑥(-g‘𝑅)𝑦) = 𝑁 ↔ 𝑥 = 𝑦)) |
62 | 57, 61 | mpbid 222 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ((◡𝐹 “ { 0 }) = {𝑁} ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → 𝑥 = 𝑦) |
63 | 62 | 3anassrs 1290 |
. . . . 5
⊢ ((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (◡𝐹 “ { 0 }) = {𝑁}) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑥 = 𝑦) |
64 | 63 | ex 450 |
. . . 4
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (◡𝐹 “ { 0 }) = {𝑁}) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
65 | 64 | ralrimivva 2971 |
. . 3
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (◡𝐹 “ { 0 }) = {𝑁}) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
66 | | dff13 6512 |
. . 3
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
67 | 43, 65, 66 | sylanbrc 698 |
. 2
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (◡𝐹 “ { 0 }) = {𝑁}) → 𝐹:𝐴–1-1→𝐵) |
68 | 42, 67 | impbida 877 |
1
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹:𝐴–1-1→𝐵 ↔ (◡𝐹 “ { 0 }) = {𝑁})) |