Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . 4
⊢
(1st ‘𝑅) = (1st ‘𝑅) |
2 | | eqid 2610 |
. . . 4
⊢ ran
(1st ‘𝑅) =
ran (1st ‘𝑅) |
3 | | keridl.1 |
. . . 4
⊢ 𝐺 = (1st ‘𝑆) |
4 | | eqid 2610 |
. . . 4
⊢ ran 𝐺 = ran 𝐺 |
5 | 1, 2, 3, 4 | rngohomf 32935 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → 𝐹:ran (1st ‘𝑅)⟶ran 𝐺) |
6 | | cnvimass 5404 |
. . . 4
⊢ (◡𝐹 “ {𝑍}) ⊆ dom 𝐹 |
7 | | fdm 5964 |
. . . 4
⊢ (𝐹:ran (1st
‘𝑅)⟶ran 𝐺 → dom 𝐹 = ran (1st ‘𝑅)) |
8 | 6, 7 | syl5sseq 3616 |
. . 3
⊢ (𝐹:ran (1st
‘𝑅)⟶ran 𝐺 → (◡𝐹 “ {𝑍}) ⊆ ran (1st ‘𝑅)) |
9 | 5, 8 | syl 17 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (◡𝐹 “ {𝑍}) ⊆ ran (1st ‘𝑅)) |
10 | | eqid 2610 |
. . . . 5
⊢
(GId‘(1st ‘𝑅)) = (GId‘(1st ‘𝑅)) |
11 | 1, 2, 10 | rngo0cl 32888 |
. . . 4
⊢ (𝑅 ∈ RingOps →
(GId‘(1st ‘𝑅)) ∈ ran (1st ‘𝑅)) |
12 | 11 | 3ad2ant1 1075 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (GId‘(1st
‘𝑅)) ∈ ran
(1st ‘𝑅)) |
13 | | keridl.2 |
. . . . 5
⊢ 𝑍 = (GId‘𝐺) |
14 | 1, 10, 3, 13 | rngohom0 32941 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹‘(GId‘(1st
‘𝑅))) = 𝑍) |
15 | | fvex 6113 |
. . . . 5
⊢ (𝐹‘(GId‘(1st
‘𝑅))) ∈
V |
16 | 15 | elsn 4140 |
. . . 4
⊢ ((𝐹‘(GId‘(1st
‘𝑅))) ∈ {𝑍} ↔ (𝐹‘(GId‘(1st
‘𝑅))) = 𝑍) |
17 | 14, 16 | sylibr 223 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹‘(GId‘(1st
‘𝑅))) ∈ {𝑍}) |
18 | | ffn 5958 |
. . . 4
⊢ (𝐹:ran (1st
‘𝑅)⟶ran 𝐺 → 𝐹 Fn ran (1st ‘𝑅)) |
19 | | elpreima 6245 |
. . . 4
⊢ (𝐹 Fn ran (1st
‘𝑅) →
((GId‘(1st ‘𝑅)) ∈ (◡𝐹 “ {𝑍}) ↔ ((GId‘(1st
‘𝑅)) ∈ ran
(1st ‘𝑅)
∧ (𝐹‘(GId‘(1st
‘𝑅))) ∈ {𝑍}))) |
20 | 5, 18, 19 | 3syl 18 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((GId‘(1st
‘𝑅)) ∈ (◡𝐹 “ {𝑍}) ↔ ((GId‘(1st
‘𝑅)) ∈ ran
(1st ‘𝑅)
∧ (𝐹‘(GId‘(1st
‘𝑅))) ∈ {𝑍}))) |
21 | 12, 17, 20 | mpbir2and 959 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (GId‘(1st
‘𝑅)) ∈ (◡𝐹 “ {𝑍})) |
22 | | an4 861 |
. . . . . . . 8
⊢ (((𝑥 ∈ ran (1st
‘𝑅) ∧ (𝐹‘𝑥) ∈ {𝑍}) ∧ (𝑦 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑦) ∈ {𝑍})) ↔ ((𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅)) ∧ ((𝐹‘𝑥) ∈ {𝑍} ∧ (𝐹‘𝑦) ∈ {𝑍}))) |
23 | 1, 2, 3 | rngohomadd 32938 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (𝐹‘(𝑥(1st ‘𝑅)𝑦)) = ((𝐹‘𝑥)𝐺(𝐹‘𝑦))) |
24 | 23 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) ∧ ((𝐹‘𝑥) = 𝑍 ∧ (𝐹‘𝑦) = 𝑍)) → (𝐹‘(𝑥(1st ‘𝑅)𝑦)) = ((𝐹‘𝑥)𝐺(𝐹‘𝑦))) |
25 | | oveq12 6558 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑥) = 𝑍 ∧ (𝐹‘𝑦) = 𝑍) → ((𝐹‘𝑥)𝐺(𝐹‘𝑦)) = (𝑍𝐺𝑍)) |
26 | 25 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) ∧ ((𝐹‘𝑥) = 𝑍 ∧ (𝐹‘𝑦) = 𝑍)) → ((𝐹‘𝑥)𝐺(𝐹‘𝑦)) = (𝑍𝐺𝑍)) |
27 | 3 | rngogrpo 32879 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ∈ RingOps → 𝐺 ∈ GrpOp) |
28 | 4, 13 | grpoidcl 26752 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ GrpOp → 𝑍 ∈ ran 𝐺) |
29 | 4, 13 | grpolid 26754 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ GrpOp ∧ 𝑍 ∈ ran 𝐺) → (𝑍𝐺𝑍) = 𝑍) |
30 | 28, 29 | mpdan 699 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ GrpOp → (𝑍𝐺𝑍) = 𝑍) |
31 | 27, 30 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ RingOps → (𝑍𝐺𝑍) = 𝑍) |
32 | 31 | 3ad2ant2 1076 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝑍𝐺𝑍) = 𝑍) |
33 | 32 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) ∧ ((𝐹‘𝑥) = 𝑍 ∧ (𝐹‘𝑦) = 𝑍)) → (𝑍𝐺𝑍) = 𝑍) |
34 | 24, 26, 33 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) ∧ ((𝐹‘𝑥) = 𝑍 ∧ (𝐹‘𝑦) = 𝑍)) → (𝐹‘(𝑥(1st ‘𝑅)𝑦)) = 𝑍) |
35 | 34 | ex 449 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (((𝐹‘𝑥) = 𝑍 ∧ (𝐹‘𝑦) = 𝑍) → (𝐹‘(𝑥(1st ‘𝑅)𝑦)) = 𝑍)) |
36 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢ (𝐹‘𝑥) ∈ V |
37 | 36 | elsn 4140 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑥) ∈ {𝑍} ↔ (𝐹‘𝑥) = 𝑍) |
38 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢ (𝐹‘𝑦) ∈ V |
39 | 38 | elsn 4140 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑦) ∈ {𝑍} ↔ (𝐹‘𝑦) = 𝑍) |
40 | 37, 39 | anbi12i 729 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑥) ∈ {𝑍} ∧ (𝐹‘𝑦) ∈ {𝑍}) ↔ ((𝐹‘𝑥) = 𝑍 ∧ (𝐹‘𝑦) = 𝑍)) |
41 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ (𝐹‘(𝑥(1st ‘𝑅)𝑦)) ∈ V |
42 | 41 | elsn 4140 |
. . . . . . . . . . 11
⊢ ((𝐹‘(𝑥(1st ‘𝑅)𝑦)) ∈ {𝑍} ↔ (𝐹‘(𝑥(1st ‘𝑅)𝑦)) = 𝑍) |
43 | 35, 40, 42 | 3imtr4g 284 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (((𝐹‘𝑥) ∈ {𝑍} ∧ (𝐹‘𝑦) ∈ {𝑍}) → (𝐹‘(𝑥(1st ‘𝑅)𝑦)) ∈ {𝑍})) |
44 | 43 | imdistanda 725 |
. . . . . . . . 9
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (((𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅)) ∧ ((𝐹‘𝑥) ∈ {𝑍} ∧ (𝐹‘𝑦) ∈ {𝑍})) → ((𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅)) ∧ (𝐹‘(𝑥(1st ‘𝑅)𝑦)) ∈ {𝑍}))) |
45 | 1, 2 | rngogcl 32881 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ RingOps ∧ 𝑥 ∈ ran (1st
‘𝑅) ∧ 𝑦 ∈ ran (1st
‘𝑅)) → (𝑥(1st ‘𝑅)𝑦) ∈ ran (1st ‘𝑅)) |
46 | 45 | 3expib 1260 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ RingOps → ((𝑥 ∈ ran (1st
‘𝑅) ∧ 𝑦 ∈ ran (1st
‘𝑅)) → (𝑥(1st ‘𝑅)𝑦) ∈ ran (1st ‘𝑅))) |
47 | 46 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅)) → (𝑥(1st ‘𝑅)𝑦) ∈ ran (1st ‘𝑅))) |
48 | 47 | anim1d 586 |
. . . . . . . . 9
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (((𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅)) ∧ (𝐹‘(𝑥(1st ‘𝑅)𝑦)) ∈ {𝑍}) → ((𝑥(1st ‘𝑅)𝑦) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑥(1st ‘𝑅)𝑦)) ∈ {𝑍}))) |
49 | 44, 48 | syld 46 |
. . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (((𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅)) ∧ ((𝐹‘𝑥) ∈ {𝑍} ∧ (𝐹‘𝑦) ∈ {𝑍})) → ((𝑥(1st ‘𝑅)𝑦) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑥(1st ‘𝑅)𝑦)) ∈ {𝑍}))) |
50 | 22, 49 | syl5bi 231 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (((𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) ∈ {𝑍}) ∧ (𝑦 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑦) ∈ {𝑍})) → ((𝑥(1st ‘𝑅)𝑦) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑥(1st ‘𝑅)𝑦)) ∈ {𝑍}))) |
51 | | elpreima 6245 |
. . . . . . . . 9
⊢ (𝐹 Fn ran (1st
‘𝑅) → (𝑥 ∈ (◡𝐹 “ {𝑍}) ↔ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) ∈ {𝑍}))) |
52 | 5, 18, 51 | 3syl 18 |
. . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝑥 ∈ (◡𝐹 “ {𝑍}) ↔ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) ∈ {𝑍}))) |
53 | | elpreima 6245 |
. . . . . . . . 9
⊢ (𝐹 Fn ran (1st
‘𝑅) → (𝑦 ∈ (◡𝐹 “ {𝑍}) ↔ (𝑦 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑦) ∈ {𝑍}))) |
54 | 5, 18, 53 | 3syl 18 |
. . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝑦 ∈ (◡𝐹 “ {𝑍}) ↔ (𝑦 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑦) ∈ {𝑍}))) |
55 | 52, 54 | anbi12d 743 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ (◡𝐹 “ {𝑍}) ∧ 𝑦 ∈ (◡𝐹 “ {𝑍})) ↔ ((𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) ∈ {𝑍}) ∧ (𝑦 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑦) ∈ {𝑍})))) |
56 | | elpreima 6245 |
. . . . . . . 8
⊢ (𝐹 Fn ran (1st
‘𝑅) → ((𝑥(1st ‘𝑅)𝑦) ∈ (◡𝐹 “ {𝑍}) ↔ ((𝑥(1st ‘𝑅)𝑦) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑥(1st ‘𝑅)𝑦)) ∈ {𝑍}))) |
57 | 5, 18, 56 | 3syl 18 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥(1st ‘𝑅)𝑦) ∈ (◡𝐹 “ {𝑍}) ↔ ((𝑥(1st ‘𝑅)𝑦) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑥(1st ‘𝑅)𝑦)) ∈ {𝑍}))) |
58 | 50, 55, 57 | 3imtr4d 282 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ (◡𝐹 “ {𝑍}) ∧ 𝑦 ∈ (◡𝐹 “ {𝑍})) → (𝑥(1st ‘𝑅)𝑦) ∈ (◡𝐹 “ {𝑍}))) |
59 | 58 | impl 648 |
. . . . 5
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ (◡𝐹 “ {𝑍})) ∧ 𝑦 ∈ (◡𝐹 “ {𝑍})) → (𝑥(1st ‘𝑅)𝑦) ∈ (◡𝐹 “ {𝑍})) |
60 | 59 | ralrimiva 2949 |
. . . 4
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ (◡𝐹 “ {𝑍})) → ∀𝑦 ∈ (◡𝐹 “ {𝑍})(𝑥(1st ‘𝑅)𝑦) ∈ (◡𝐹 “ {𝑍})) |
61 | 37 | anbi2i 726 |
. . . . . . 7
⊢ ((𝑥 ∈ ran (1st
‘𝑅) ∧ (𝐹‘𝑥) ∈ {𝑍}) ↔ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) |
62 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(2nd ‘𝑅) = (2nd ‘𝑅) |
63 | 1, 62, 2 | rngocl 32870 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran (1st
‘𝑅) ∧ 𝑥 ∈ ran (1st
‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ ran (1st ‘𝑅)) |
64 | 63 | 3expb 1258 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ RingOps ∧ (𝑧 ∈ ran (1st
‘𝑅) ∧ 𝑥 ∈ ran (1st
‘𝑅))) → (𝑧(2nd ‘𝑅)𝑥) ∈ ran (1st ‘𝑅)) |
65 | 64 | 3ad2antl1 1216 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑧 ∈ ran (1st ‘𝑅) ∧ 𝑥 ∈ ran (1st ‘𝑅))) → (𝑧(2nd ‘𝑅)𝑥) ∈ ran (1st ‘𝑅)) |
66 | 65 | anass1rs 845 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st ‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ ran (1st ‘𝑅)) |
67 | 66 | adantlrr 753 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ ran (1st ‘𝑅)) |
68 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(2nd ‘𝑆) = (2nd ‘𝑆) |
69 | 1, 2, 62, 68 | rngohommul 32939 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑧 ∈ ran (1st ‘𝑅) ∧ 𝑥 ∈ ran (1st ‘𝑅))) → (𝐹‘(𝑧(2nd ‘𝑅)𝑥)) = ((𝐹‘𝑧)(2nd ‘𝑆)(𝐹‘𝑥))) |
70 | 69 | anass1rs 845 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st ‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑧(2nd ‘𝑅)𝑥)) = ((𝐹‘𝑧)(2nd ‘𝑆)(𝐹‘𝑥))) |
71 | 70 | adantlrr 753 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑧(2nd ‘𝑅)𝑥)) = ((𝐹‘𝑧)(2nd ‘𝑆)(𝐹‘𝑥))) |
72 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑥) = 𝑍 → ((𝐹‘𝑧)(2nd ‘𝑆)(𝐹‘𝑥)) = ((𝐹‘𝑧)(2nd ‘𝑆)𝑍)) |
73 | 72 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ran (1st
‘𝑅) ∧ (𝐹‘𝑥) = 𝑍) → ((𝐹‘𝑧)(2nd ‘𝑆)(𝐹‘𝑥)) = ((𝐹‘𝑧)(2nd ‘𝑆)𝑍)) |
74 | 73 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → ((𝐹‘𝑧)(2nd ‘𝑆)(𝐹‘𝑥)) = ((𝐹‘𝑧)(2nd ‘𝑆)𝑍)) |
75 | 1, 2, 3, 4 | rngohomcl 32936 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝐹‘𝑧) ∈ ran 𝐺) |
76 | 13, 4, 3, 68 | rngorz 32892 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ RingOps ∧ (𝐹‘𝑧) ∈ ran 𝐺) → ((𝐹‘𝑧)(2nd ‘𝑆)𝑍) = 𝑍) |
77 | 76 | 3ad2antl2 1217 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝐹‘𝑧) ∈ ran 𝐺) → ((𝐹‘𝑧)(2nd ‘𝑆)𝑍) = 𝑍) |
78 | 75, 77 | syldan 486 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → ((𝐹‘𝑧)(2nd ‘𝑆)𝑍) = 𝑍) |
79 | 78 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → ((𝐹‘𝑧)(2nd ‘𝑆)𝑍) = 𝑍) |
80 | 71, 74, 79 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑧(2nd ‘𝑅)𝑥)) = 𝑍) |
81 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢ (𝐹‘(𝑧(2nd ‘𝑅)𝑥)) ∈ V |
82 | 81 | elsn 4140 |
. . . . . . . . . . . 12
⊢ ((𝐹‘(𝑧(2nd ‘𝑅)𝑥)) ∈ {𝑍} ↔ (𝐹‘(𝑧(2nd ‘𝑅)𝑥)) = 𝑍) |
83 | 80, 82 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑧(2nd ‘𝑅)𝑥)) ∈ {𝑍}) |
84 | | elpreima 6245 |
. . . . . . . . . . . . 13
⊢ (𝐹 Fn ran (1st
‘𝑅) → ((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ↔ ((𝑧(2nd ‘𝑅)𝑥) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑧(2nd ‘𝑅)𝑥)) ∈ {𝑍}))) |
85 | 5, 18, 84 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ↔ ((𝑧(2nd ‘𝑅)𝑥) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑧(2nd ‘𝑅)𝑥)) ∈ {𝑍}))) |
86 | 85 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → ((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ↔ ((𝑧(2nd ‘𝑅)𝑥) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑧(2nd ‘𝑅)𝑥)) ∈ {𝑍}))) |
87 | 67, 83, 86 | mpbir2and 959 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍})) |
88 | 1, 62, 2 | rngocl 32870 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ RingOps ∧ 𝑥 ∈ ran (1st
‘𝑅) ∧ 𝑧 ∈ ran (1st
‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ ran (1st ‘𝑅)) |
89 | 88 | 3expb 1258 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ RingOps ∧ (𝑥 ∈ ran (1st
‘𝑅) ∧ 𝑧 ∈ ran (1st
‘𝑅))) → (𝑥(2nd ‘𝑅)𝑧) ∈ ran (1st ‘𝑅)) |
90 | 89 | 3ad2antl1 1216 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑧 ∈ ran (1st ‘𝑅))) → (𝑥(2nd ‘𝑅)𝑧) ∈ ran (1st ‘𝑅)) |
91 | 90 | anassrs 678 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st ‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ ran (1st ‘𝑅)) |
92 | 91 | adantlrr 753 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ ran (1st ‘𝑅)) |
93 | 1, 2, 62, 68 | rngohommul 32939 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑧 ∈ ran (1st ‘𝑅))) → (𝐹‘(𝑥(2nd ‘𝑅)𝑧)) = ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑧))) |
94 | 93 | anassrs 678 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st ‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑥(2nd ‘𝑅)𝑧)) = ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑧))) |
95 | 94 | adantlrr 753 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑥(2nd ‘𝑅)𝑧)) = ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑧))) |
96 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑥) = 𝑍 → ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑧)) = (𝑍(2nd ‘𝑆)(𝐹‘𝑧))) |
97 | 96 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ran (1st
‘𝑅) ∧ (𝐹‘𝑥) = 𝑍) → ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑧)) = (𝑍(2nd ‘𝑆)(𝐹‘𝑧))) |
98 | 97 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑧)) = (𝑍(2nd ‘𝑆)(𝐹‘𝑧))) |
99 | 13, 4, 3, 68 | rngolz 32891 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ RingOps ∧ (𝐹‘𝑧) ∈ ran 𝐺) → (𝑍(2nd ‘𝑆)(𝐹‘𝑧)) = 𝑍) |
100 | 99 | 3ad2antl2 1217 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝐹‘𝑧) ∈ ran 𝐺) → (𝑍(2nd ‘𝑆)(𝐹‘𝑧)) = 𝑍) |
101 | 75, 100 | syldan 486 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑍(2nd ‘𝑆)(𝐹‘𝑧)) = 𝑍) |
102 | 101 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑍(2nd ‘𝑆)(𝐹‘𝑧)) = 𝑍) |
103 | 95, 98, 102 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑥(2nd ‘𝑅)𝑧)) = 𝑍) |
104 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢ (𝐹‘(𝑥(2nd ‘𝑅)𝑧)) ∈ V |
105 | 104 | elsn 4140 |
. . . . . . . . . . . 12
⊢ ((𝐹‘(𝑥(2nd ‘𝑅)𝑧)) ∈ {𝑍} ↔ (𝐹‘(𝑥(2nd ‘𝑅)𝑧)) = 𝑍) |
106 | 103, 105 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑥(2nd ‘𝑅)𝑧)) ∈ {𝑍}) |
107 | | elpreima 6245 |
. . . . . . . . . . . . 13
⊢ (𝐹 Fn ran (1st
‘𝑅) → ((𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍}) ↔ ((𝑥(2nd ‘𝑅)𝑧) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑥(2nd ‘𝑅)𝑧)) ∈ {𝑍}))) |
108 | 5, 18, 107 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍}) ↔ ((𝑥(2nd ‘𝑅)𝑧) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑥(2nd ‘𝑅)𝑧)) ∈ {𝑍}))) |
109 | 108 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → ((𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍}) ↔ ((𝑥(2nd ‘𝑅)𝑧) ∈ ran (1st ‘𝑅) ∧ (𝐹‘(𝑥(2nd ‘𝑅)𝑧)) ∈ {𝑍}))) |
110 | 92, 106, 109 | mpbir2and 959 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍})) |
111 | 87, 110 | jca 553 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → ((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍}))) |
112 | 111 | ralrimiva 2949 |
. . . . . . . 8
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍}))) |
113 | 112 | ex 449 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) = 𝑍) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍})))) |
114 | 61, 113 | syl5bi 231 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st ‘𝑅) ∧ (𝐹‘𝑥) ∈ {𝑍}) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍})))) |
115 | 52, 114 | sylbid 229 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝑥 ∈ (◡𝐹 “ {𝑍}) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍})))) |
116 | 115 | imp 444 |
. . . 4
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ (◡𝐹 “ {𝑍})) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍}))) |
117 | 60, 116 | jca 553 |
. . 3
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ (◡𝐹 “ {𝑍})) → (∀𝑦 ∈ (◡𝐹 “ {𝑍})(𝑥(1st ‘𝑅)𝑦) ∈ (◡𝐹 “ {𝑍}) ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍})))) |
118 | 117 | ralrimiva 2949 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ∀𝑥 ∈ (◡𝐹 “ {𝑍})(∀𝑦 ∈ (◡𝐹 “ {𝑍})(𝑥(1st ‘𝑅)𝑦) ∈ (◡𝐹 “ {𝑍}) ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍})))) |
119 | 1, 62, 2, 10 | isidl 32983 |
. . 3
⊢ (𝑅 ∈ RingOps → ((◡𝐹 “ {𝑍}) ∈ (Idl‘𝑅) ↔ ((◡𝐹 “ {𝑍}) ⊆ ran (1st ‘𝑅) ∧
(GId‘(1st ‘𝑅)) ∈ (◡𝐹 “ {𝑍}) ∧ ∀𝑥 ∈ (◡𝐹 “ {𝑍})(∀𝑦 ∈ (◡𝐹 “ {𝑍})(𝑥(1st ‘𝑅)𝑦) ∈ (◡𝐹 “ {𝑍}) ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍})))))) |
120 | 119 | 3ad2ant1 1075 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((◡𝐹 “ {𝑍}) ∈ (Idl‘𝑅) ↔ ((◡𝐹 “ {𝑍}) ⊆ ran (1st ‘𝑅) ∧
(GId‘(1st ‘𝑅)) ∈ (◡𝐹 “ {𝑍}) ∧ ∀𝑥 ∈ (◡𝐹 “ {𝑍})(∀𝑦 ∈ (◡𝐹 “ {𝑍})(𝑥(1st ‘𝑅)𝑦) ∈ (◡𝐹 “ {𝑍}) ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ (◡𝐹 “ {𝑍}) ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ (◡𝐹 “ {𝑍})))))) |
121 | 9, 21, 118, 120 | mpbir3and 1238 |
1
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (◡𝐹 “ {𝑍}) ∈ (Idl‘𝑅)) |