Step | Hyp | Ref
| Expression |
1 | | cnvimass 5739 |
. . 3
⊢ (◡𝐹 “ {𝑍}) ⊆ dom 𝐹 |
2 | | eqid 2778 |
. . . 4
⊢
(1st ‘𝑅) = (1st ‘𝑅) |
3 | | eqid 2778 |
. . . 4
⊢ ran
(1st ‘𝑅) =
ran (1st ‘𝑅) |
4 | | keridl.1 |
. . . 4
⊢ 𝐺 = (1st ‘𝑆) |
5 | | eqid 2778 |
. . . 4
⊢ ran 𝐺 = ran 𝐺 |
6 | 2, 3, 4, 5 | rngohomf 34391 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → 𝐹:ran (1st ‘𝑅)⟶ran 𝐺) |
7 | 1, 6 | fssdm 6307 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (◡𝐹 “ {𝑍}) ⊆ ran (1st ‘𝑅)) |
8 | | eqid 2778 |
. . . . 5
⊢
(GId‘(1st ‘𝑅)) = (GId‘(1st ‘𝑅)) |
9 | 2, 3, 8 | rngo0cl 34344 |
. . . 4
⊢ (𝑅 ∈ RingOps →
(GId‘(1st ‘𝑅)) ∈ ran (1st ‘𝑅)) |
10 | 9 | 3ad2ant1 1124 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (GId‘(1st
‘𝑅)) ∈ ran
(1st ‘𝑅)) |
11 | | keridl.2 |
. . . . 5
⊢ 𝑍 = (GId‘𝐺) |
12 | 2, 8, 4, 11 | rngohom0 34397 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹‘(GId‘(1st
‘𝑅))) = 𝑍) |
13 | | fvex 6459 |
. . . . 5
⊢ (𝐹‘(GId‘(1st
‘𝑅))) ∈
V |
14 | 13 | elsn 4413 |
. . . 4
⊢ ((𝐹‘(GId‘(1st
‘𝑅))) ∈ {𝑍} ↔ (𝐹‘(GId‘(1st
‘𝑅))) = 𝑍) |
15 | 12, 14 | sylibr 226 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹‘(GId‘(1st
‘𝑅))) ∈ {𝑍}) |
16 | | ffn 6291 |
. . . 4
⊢ (𝐹:ran (1st
‘𝑅)⟶ran 𝐺 → 𝐹 Fn ran (1st ‘𝑅)) |
17 | | elpreima 6600 |
. . . 4
⊢ (𝐹 Fn ran (1st
‘𝑅) →
((GId‘(1st ‘𝑅)) ∈ (◡𝐹 “ {𝑍}) ↔ ((GId‘(1st
‘𝑅)) ∈ ran
(1st ‘𝑅)
∧ (𝐹‘(GId‘(1st
‘𝑅))) ∈ {𝑍}))) |
18 | 6, 16, 17 | 3syl 18 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((GId‘(1st
‘𝑅)) ∈ (◡𝐹 “ {𝑍}) ↔ ((GId‘(1st
‘𝑅)) ∈ ran
(1st ‘𝑅)
∧ (𝐹‘(GId‘(1st
‘𝑅))) ∈ {𝑍}))) |
19 | 10, 15, 18 | mpbir2and 703 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (GId‘(1st
‘𝑅)) ∈ (◡𝐹 “ {𝑍})) |
20 | | an4 646 |
. . . . . . . 8
⊢ (((𝑥 ∈ ran (1st
‘𝑅) ∧ (𝐹‘𝑥) ∈ {𝑍}) ∧ (𝑦 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑦) ∈ {𝑍})) ↔ ((𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅)) ∧ ((𝐹‘𝑥) ∈ {𝑍} ∧ (𝐹‘𝑦) ∈ {𝑍}))) |
21 | 2, 3, 4 | rngohomadd 34394 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (𝐹‘(𝑥(1st ‘𝑅)𝑦)) = ((𝐹‘𝑥)𝐺(𝐹‘𝑦))) |
22 | 21 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) ∧ ((𝐹‘𝑥) = 𝑍 ∧ (𝐹‘𝑦) = 𝑍)) → (𝐹‘(𝑥(1st ‘𝑅)𝑦)) = ((𝐹‘𝑥)𝐺(𝐹‘𝑦))) |
23 | | oveq12 6931 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑥) = 𝑍 ∧ (𝐹‘𝑦) = 𝑍) → ((𝐹‘𝑥)𝐺(𝐹‘𝑦)) = (𝑍𝐺𝑍)) |
24 | 23 | adantl 475 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) ∧ ((𝐹‘𝑥) = 𝑍 ∧ (𝐹‘𝑦) = 𝑍)) → ((𝐹‘𝑥)𝐺(𝐹‘𝑦)) = (𝑍𝐺𝑍)) |
25 | 4 | rngogrpo 34335 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ∈ RingOps → 𝐺 ∈ GrpOp) |
26 | 5, 11 | grpoidcl 27941 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ GrpOp → 𝑍 ∈ ran 𝐺) |
27 | 5, 11 | grpolid 27943 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ GrpOp ∧ 𝑍 ∈ ran 𝐺) → (𝑍𝐺𝑍) = 𝑍) |
28 | 26, 27 | mpdan 677 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ GrpOp → (𝑍𝐺𝑍) = 𝑍) |
29 | 25, 28 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ RingOps → (𝑍𝐺𝑍) = 𝑍) |
30 | 29 | 3ad2ant2 1125 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝑍𝐺𝑍) = 𝑍) |
31 | 30 | ad2antrr 716 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) ∧ ((𝐹‘𝑥) = 𝑍 ∧ (𝐹‘𝑦) = 𝑍)) → (𝑍𝐺𝑍) = 𝑍) |
32 | 22, 24, 31 | 3eqtrd 2818 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) ∧ ((𝐹‘𝑥) = 𝑍 ∧ (𝐹‘𝑦) = 𝑍)) → (𝐹‘(𝑥(1st ‘𝑅)𝑦)) = 𝑍) |
33 | 32 | ex 403 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (((𝐹‘𝑥) = 𝑍 ∧ (𝐹‘𝑦) = 𝑍) → (𝐹‘(𝑥(1st ‘𝑅)𝑦)) = 𝑍)) |
34 | | fvex 6459 |
. . . . . . . . . . . . 13
⊢ (𝐹‘𝑥) ∈ V |
35 | 34 | elsn 4413 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑥) ∈ {𝑍} ↔ (𝐹‘𝑥) = 𝑍) |
36 | | fvex 6459 |
. . . . . . . . . . . . 13
⊢ (𝐹‘𝑦) ∈ V |
37 | 36 | elsn 4413 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑦) ∈ {𝑍} ↔ (𝐹‘𝑦) = 𝑍) |
38 | 35, 37 | anbi12i 620 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑥) ∈ {𝑍} ∧ (𝐹‘𝑦) ∈ {𝑍}) ↔ ((𝐹‘𝑥) = 𝑍 ∧ (𝐹‘𝑦) = 𝑍)) |
39 | | fvex 6459 |
. . . . . . . . . . . 12
⊢ (𝐹‘(𝑥(1st ‘𝑅)𝑦)) ∈ V |
40 | 39 | elsn 4413 |
. . . . . . . . . . 11
⊢ ((𝐹‘(𝑥(1st ‘𝑅)𝑦)) ∈ {𝑍} ↔ (𝐹‘(𝑥(1st ‘𝑅)𝑦)) = 𝑍) |
41 | 33, 38, 40 | 3imtr4g 288 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (((𝐹‘𝑥) ∈ {𝑍} ∧ (𝐹‘𝑦) ∈ {𝑍}) → (𝐹‘(𝑥(1st ‘𝑅)𝑦)) ∈ {𝑍})) |
42 | 41 | imdistanda 567 |
. . . . . . . . 9
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (((𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅)) ∧ ((𝐹‘𝑥) ∈ {𝑍} ∧ (𝐹‘𝑦) ∈ {𝑍})) → ((𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅)) ∧ (𝐹‘(𝑥(1st ‘𝑅)𝑦)) ∈ {𝑍}))) |
43 | 2, 3 | rngogcl 34337 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ RingOps ∧ 𝑥 ∈ ran (1st
‘𝑅) ∧ 𝑦 ∈ ran (1st
‘𝑅)) → (𝑥(1st ‘𝑅)𝑦) ∈ ran (1st ‘𝑅)) |
44 | 43 | 3expib 1113 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ RingOps → ((𝑥 ∈ ran (1st
‘𝑅) ∧ 𝑦 ∈ ran (1st
‘𝑅)) → (𝑥(1st ‘𝑅)𝑦) ∈ ran (1st ‘𝑅))) |
45 | 44 | 3ad2ant1 1124 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅)) → (𝑥(1st ‘𝑅)𝑦) ∈ ran (1st ‘𝑅))) |
46 | 45 | anim1d 604 |
. . . . . . . . 9
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (((𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅)) ∧ (𝐹‘(𝑥(1st ‘𝑅)𝑦)) ∈ {𝑍}) → ((𝑥(1st ‘𝑅)𝑦) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑥(1st ‘𝑅)𝑦)) ∈ {𝑍}))) |
47 | 42, 46 | syld 47 |
. . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (((𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅)) ∧ ((𝐹‘𝑥) ∈ {𝑍} ∧ (𝐹‘𝑦) ∈ {𝑍})) → ((𝑥(1st ‘𝑅)𝑦) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑥(1st ‘𝑅)𝑦)) ∈ {𝑍}))) |
48 | 20, 47 | syl5bi 234 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (((𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) ∈ {𝑍}) ∧ (𝑦 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑦) ∈ {𝑍})) → ((𝑥(1st ‘𝑅)𝑦) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑥(1st ‘𝑅)𝑦)) ∈ {𝑍}))) |
49 | | elpreima 6600 |
. . . . . . . . 9
⊢ (𝐹 Fn ran (1st
‘𝑅) → (𝑥 ∈ (◡𝐹 “ {𝑍}) ↔ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) ∈ {𝑍}))) |
50 | 6, 16, 49 | 3syl 18 |
. . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝑥 ∈ (◡𝐹 “ {𝑍}) ↔ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) ∈ {𝑍}))) |
51 | | elpreima 6600 |
. . . . . . . . 9
⊢ (𝐹 Fn ran (1st
‘𝑅) → (𝑦 ∈ (◡𝐹 “ {𝑍}) ↔ (𝑦 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑦) ∈ {𝑍}))) |
52 | 6, 16, 51 | 3syl 18 |
. . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝑦 ∈ (◡𝐹 “ {𝑍}) ↔ (𝑦 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑦) ∈ {𝑍}))) |
53 | 50, 52 | anbi12d 624 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ (◡𝐹 “ {𝑍}) ∧ 𝑦 ∈ (◡𝐹 “ {𝑍})) ↔ ((𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) ∈ {𝑍}) ∧ (𝑦 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑦) ∈ {𝑍})))) |
54 | | elpreima 6600 |
. . . . . . . 8
⊢ (𝐹 Fn ran (1st
‘𝑅) → ((𝑥(1st ‘𝑅)𝑦) ∈ (◡𝐹 “ {𝑍}) ↔ ((𝑥(1st ‘𝑅)𝑦) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑥(1st ‘𝑅)𝑦)) ∈ {𝑍}))) |
55 | 6, 16, 54 | 3syl 18 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥(1st ‘𝑅)𝑦) ∈ (◡𝐹 “ {𝑍}) ↔ ((𝑥(1st ‘𝑅)𝑦) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑥(1st ‘𝑅)𝑦)) ∈ {𝑍}))) |
56 | 48, 53, 55 | 3imtr4d 286 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ (◡𝐹 “ {𝑍}) ∧ 𝑦 ∈ (◡𝐹 “ {𝑍})) → (𝑥(1st ‘𝑅)𝑦) ∈ (◡𝐹 “ {𝑍}))) |
57 | 56 | impl 449 |
. . . . 5
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ (◡𝐹 “ {𝑍})) ∧ 𝑦 ∈ (◡𝐹 “ {𝑍})) → (𝑥(1st ‘𝑅)𝑦) ∈ (◡𝐹 “ {𝑍})) |
58 | 57 | ralrimiva 3148 |
. . . 4
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ (◡𝐹 “ {𝑍})) → ∀𝑦 ∈ (◡𝐹 “ {𝑍})(𝑥(1st ‘𝑅)𝑦) ∈ (◡𝐹 “ {𝑍})) |
59 | 35 | anbi2i 616 |
. . . . . . 7
⊢ ((𝑥 ∈ ran (1st
‘𝑅) ∧ (𝐹‘𝑥) ∈ {𝑍}) ↔ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) |
60 | | eqid 2778 |
. . . . . . . . . . . . . . . 16
⊢
(2nd ‘𝑅) = (2nd ‘𝑅) |
61 | 2, 60, 3 | rngocl 34326 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran (1st
‘𝑅) ∧ 𝑥 ∈ ran (1st
‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ ran (1st ‘𝑅)) |
62 | 61 | 3expb 1110 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ RingOps ∧ (𝑧 ∈ ran (1st
‘𝑅) ∧ 𝑥 ∈ ran (1st
‘𝑅))) → (𝑧(2nd ‘𝑅)𝑥) ∈ ran (1st ‘𝑅)) |
63 | 62 | 3ad2antl1 1193 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑧 ∈ ran (1st ‘𝑅) ∧ 𝑥 ∈ ran (1st ‘𝑅))) → (𝑧(2nd ‘𝑅)𝑥) ∈ ran (1st ‘𝑅)) |
64 | 63 | anass1rs 645 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st ‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ ran (1st ‘𝑅)) |
65 | 64 | adantlrr 711 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ ran (1st ‘𝑅)) |
66 | | eqid 2778 |
. . . . . . . . . . . . . . . 16
⊢
(2nd ‘𝑆) = (2nd ‘𝑆) |
67 | 2, 3, 60, 66 | rngohommul 34395 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑧 ∈ ran (1st ‘𝑅) ∧ 𝑥 ∈ ran (1st ‘𝑅))) → (𝐹‘(𝑧(2nd ‘𝑅)𝑥)) = ((𝐹‘𝑧)(2nd ‘𝑆)(𝐹‘𝑥))) |
68 | 67 | anass1rs 645 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st ‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑧(2nd ‘𝑅)𝑥)) = ((𝐹‘𝑧)(2nd ‘𝑆)(𝐹‘𝑥))) |
69 | 68 | adantlrr 711 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑧(2nd ‘𝑅)𝑥)) = ((𝐹‘𝑧)(2nd ‘𝑆)(𝐹‘𝑥))) |
70 | | oveq2 6930 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑥) = 𝑍 → ((𝐹‘𝑧)(2nd ‘𝑆)(𝐹‘𝑥)) = ((𝐹‘𝑧)(2nd ‘𝑆)𝑍)) |
71 | 70 | adantl 475 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ran (1st
‘𝑅) ∧ (𝐹‘𝑥) = 𝑍) → ((𝐹‘𝑧)(2nd ‘𝑆)(𝐹‘𝑥)) = ((𝐹‘𝑧)(2nd ‘𝑆)𝑍)) |
72 | 71 | ad2antlr 717 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → ((𝐹‘𝑧)(2nd ‘𝑆)(𝐹‘𝑥)) = ((𝐹‘𝑧)(2nd ‘𝑆)𝑍)) |
73 | 2, 3, 4, 5 | rngohomcl 34392 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝐹‘𝑧) ∈ ran 𝐺) |
74 | 11, 5, 4, 66 | rngorz 34348 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ RingOps ∧ (𝐹‘𝑧) ∈ ran 𝐺) → ((𝐹‘𝑧)(2nd ‘𝑆)𝑍) = 𝑍) |
75 | 74 | 3ad2antl2 1194 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝐹‘𝑧) ∈ ran 𝐺) → ((𝐹‘𝑧)(2nd ‘𝑆)𝑍) = 𝑍) |
76 | 73, 75 | syldan 585 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → ((𝐹‘𝑧)(2nd ‘𝑆)𝑍) = 𝑍) |
77 | 76 | adantlr 705 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → ((𝐹‘𝑧)(2nd ‘𝑆)𝑍) = 𝑍) |
78 | 69, 72, 77 | 3eqtrd 2818 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑧(2nd ‘𝑅)𝑥)) = 𝑍) |
79 | | fvex 6459 |
. . . . . . . . . . . . 13
⊢ (𝐹‘(𝑧(2nd ‘𝑅)𝑥)) ∈ V |
80 | 79 | elsn 4413 |
. . . . . . . . . . . 12
⊢ ((𝐹‘(𝑧(2nd ‘𝑅)𝑥)) ∈ {𝑍} ↔ (𝐹‘(𝑧(2nd ‘𝑅)𝑥)) = 𝑍) |
81 | 78, 80 | sylibr 226 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑧(2nd ‘𝑅)𝑥)) ∈ {𝑍}) |
82 | | elpreima 6600 |
. . . . . . . . . . . . 13
⊢ (𝐹 Fn ran (1st
‘𝑅) → ((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ↔ ((𝑧(2nd ‘𝑅)𝑥) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑧(2nd ‘𝑅)𝑥)) ∈ {𝑍}))) |
83 | 6, 16, 82 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ↔ ((𝑧(2nd ‘𝑅)𝑥) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑧(2nd ‘𝑅)𝑥)) ∈ {𝑍}))) |
84 | 83 | ad2antrr 716 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → ((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ↔ ((𝑧(2nd ‘𝑅)𝑥) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑧(2nd ‘𝑅)𝑥)) ∈ {𝑍}))) |
85 | 65, 81, 84 | mpbir2and 703 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍})) |
86 | 2, 60, 3 | rngocl 34326 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ RingOps ∧ 𝑥 ∈ ran (1st
‘𝑅) ∧ 𝑧 ∈ ran (1st
‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ ran (1st ‘𝑅)) |
87 | 86 | 3expb 1110 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ RingOps ∧ (𝑥 ∈ ran (1st
‘𝑅) ∧ 𝑧 ∈ ran (1st
‘𝑅))) → (𝑥(2nd ‘𝑅)𝑧) ∈ ran (1st ‘𝑅)) |
88 | 87 | 3ad2antl1 1193 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑧 ∈ ran (1st ‘𝑅))) → (𝑥(2nd ‘𝑅)𝑧) ∈ ran (1st ‘𝑅)) |
89 | 88 | anassrs 461 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st ‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ ran (1st ‘𝑅)) |
90 | 89 | adantlrr 711 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ ran (1st ‘𝑅)) |
91 | 2, 3, 60, 66 | rngohommul 34395 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑧 ∈ ran (1st ‘𝑅))) → (𝐹‘(𝑥(2nd ‘𝑅)𝑧)) = ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑧))) |
92 | 91 | anassrs 461 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st ‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑥(2nd ‘𝑅)𝑧)) = ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑧))) |
93 | 92 | adantlrr 711 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑥(2nd ‘𝑅)𝑧)) = ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑧))) |
94 | | oveq1 6929 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑥) = 𝑍 → ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑧)) = (𝑍(2nd ‘𝑆)(𝐹‘𝑧))) |
95 | 94 | adantl 475 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ran (1st
‘𝑅) ∧ (𝐹‘𝑥) = 𝑍) → ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑧)) = (𝑍(2nd ‘𝑆)(𝐹‘𝑧))) |
96 | 95 | ad2antlr 717 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑧)) = (𝑍(2nd ‘𝑆)(𝐹‘𝑧))) |
97 | 11, 5, 4, 66 | rngolz 34347 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ RingOps ∧ (𝐹‘𝑧) ∈ ran 𝐺) → (𝑍(2nd ‘𝑆)(𝐹‘𝑧)) = 𝑍) |
98 | 97 | 3ad2antl2 1194 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝐹‘𝑧) ∈ ran 𝐺) → (𝑍(2nd ‘𝑆)(𝐹‘𝑧)) = 𝑍) |
99 | 73, 98 | syldan 585 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑍(2nd ‘𝑆)(𝐹‘𝑧)) = 𝑍) |
100 | 99 | adantlr 705 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑍(2nd ‘𝑆)(𝐹‘𝑧)) = 𝑍) |
101 | 93, 96, 100 | 3eqtrd 2818 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑥(2nd ‘𝑅)𝑧)) = 𝑍) |
102 | | fvex 6459 |
. . . . . . . . . . . . 13
⊢ (𝐹‘(𝑥(2nd ‘𝑅)𝑧)) ∈ V |
103 | 102 | elsn 4413 |
. . . . . . . . . . . 12
⊢ ((𝐹‘(𝑥(2nd ‘𝑅)𝑧)) ∈ {𝑍} ↔ (𝐹‘(𝑥(2nd ‘𝑅)𝑧)) = 𝑍) |
104 | 101, 103 | sylibr 226 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑥(2nd ‘𝑅)𝑧)) ∈ {𝑍}) |
105 | | elpreima 6600 |
. . . . . . . . . . . . 13
⊢ (𝐹 Fn ran (1st
‘𝑅) → ((𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍}) ↔ ((𝑥(2nd ‘𝑅)𝑧) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑥(2nd ‘𝑅)𝑧)) ∈ {𝑍}))) |
106 | 6, 16, 105 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍}) ↔ ((𝑥(2nd ‘𝑅)𝑧) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑥(2nd ‘𝑅)𝑧)) ∈ {𝑍}))) |
107 | 106 | ad2antrr 716 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → ((𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍}) ↔ ((𝑥(2nd ‘𝑅)𝑧) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑥(2nd ‘𝑅)𝑧)) ∈ {𝑍}))) |
108 | 90, 104, 107 | mpbir2and 703 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍})) |
109 | 85, 108 | jca 507 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → ((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍}))) |
110 | 109 | ralrimiva 3148 |
. . . . . . . 8
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍}))) |
111 | 110 | ex 403 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍})))) |
112 | 59, 111 | syl5bi 234 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) ∈ {𝑍}) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍})))) |
113 | 50, 112 | sylbid 232 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝑥 ∈ (◡𝐹 “ {𝑍}) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍})))) |
114 | 113 | imp 397 |
. . . 4
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ (◡𝐹 “ {𝑍})) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍}))) |
115 | 58, 114 | jca 507 |
. . 3
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ (◡𝐹 “ {𝑍})) → (∀𝑦 ∈ (◡𝐹 “ {𝑍})(𝑥(1st ‘𝑅)𝑦) ∈ (◡𝐹 “ {𝑍}) ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍})))) |
116 | 115 | ralrimiva 3148 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ∀𝑥 ∈ (◡𝐹 “ {𝑍})(∀𝑦 ∈ (◡𝐹 “ {𝑍})(𝑥(1st ‘𝑅)𝑦) ∈ (◡𝐹 “ {𝑍}) ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍})))) |
117 | 2, 60, 3, 8 | isidl 34439 |
. . 3
⊢ (𝑅 ∈ RingOps → ((◡𝐹 “ {𝑍}) ∈ (Idl‘𝑅) ↔ ((◡𝐹 “ {𝑍}) ⊆ ran (1st ‘𝑅) ∧
(GId‘(1st ‘𝑅)) ∈ (◡𝐹 “ {𝑍}) ∧ ∀𝑥 ∈ (◡𝐹 “ {𝑍})(∀𝑦 ∈ (◡𝐹 “ {𝑍})(𝑥(1st ‘𝑅)𝑦) ∈ (◡𝐹 “ {𝑍}) ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍})))))) |
118 | 117 | 3ad2ant1 1124 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((◡𝐹 “ {𝑍}) ∈ (Idl‘𝑅) ↔ ((◡𝐹 “ {𝑍}) ⊆ ran (1st ‘𝑅) ∧
(GId‘(1st ‘𝑅)) ∈ (◡𝐹 “ {𝑍}) ∧ ∀𝑥 ∈ (◡𝐹 “ {𝑍})(∀𝑦 ∈ (◡𝐹 “ {𝑍})(𝑥(1st ‘𝑅)𝑦) ∈ (◡𝐹 “ {𝑍}) ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍})))))) |
119 | 7, 19, 116, 118 | mpbir3and 1399 |
1
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (◡𝐹 “ {𝑍}) ∈ (Idl‘𝑅)) |