Step | Hyp | Ref
| Expression |
1 | | rhmpreimacn.g |
. . . . . 6
⊢ 𝐺 = (𝑖 ∈ 𝐵 ↦ (◡𝐹 “ 𝑖)) |
2 | | imaeq2 5890 |
. . . . . 6
⊢ (𝑖 = 𝑔 → (◡𝐹 “ 𝑖) = (◡𝐹 “ 𝑔)) |
3 | | simpr 489 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ 𝐵) |
4 | | rhmpreimacn.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
5 | 4 | elexd 3429 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ V) |
6 | | cnvexg 7627 |
. . . . . . . 8
⊢ (𝐹 ∈ V → ◡𝐹 ∈ V) |
7 | | imaexg 7618 |
. . . . . . . 8
⊢ (◡𝐹 ∈ V → (◡𝐹 “ 𝑔) ∈ V) |
8 | 5, 6, 7 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (◡𝐹 “ 𝑔) ∈ V) |
9 | 8 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (◡𝐹 “ 𝑔) ∈ V) |
10 | 1, 2, 3, 9 | fvmptd3 6775 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (𝐺‘𝑔) = (◡𝐹 “ 𝑔)) |
11 | 10 | eleq1d 2835 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → ((𝐺‘𝑔) ∈ (𝑉‘𝐼) ↔ (◡𝐹 “ 𝑔) ∈ (𝑉‘𝐼))) |
12 | 11 | pm5.32da 583 |
. . 3
⊢ (𝜑 → ((𝑔 ∈ 𝐵 ∧ (𝐺‘𝑔) ∈ (𝑉‘𝐼)) ↔ (𝑔 ∈ 𝐵 ∧ (◡𝐹 “ 𝑔) ∈ (𝑉‘𝐼)))) |
13 | | rhmpreimacn.s |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ CRing) |
14 | 13 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵) → 𝑆 ∈ CRing) |
15 | 4 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵) → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
16 | | simpr 489 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵) → 𝑖 ∈ 𝐵) |
17 | | rhmpreimacn.b |
. . . . . . . 8
⊢ 𝐵 = (PrmIdeal‘𝑆) |
18 | 16, 17 | eleqtrdi 2861 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵) → 𝑖 ∈ (PrmIdeal‘𝑆)) |
19 | | rhmpreimacn.a |
. . . . . . . 8
⊢ 𝐴 = (PrmIdeal‘𝑅) |
20 | 19 | rhmpreimaprmidl 31133 |
. . . . . . 7
⊢ (((𝑆 ∈ CRing ∧ 𝐹 ∈ (𝑅 RingHom 𝑆)) ∧ 𝑖 ∈ (PrmIdeal‘𝑆)) → (◡𝐹 “ 𝑖) ∈ 𝐴) |
21 | 14, 15, 18, 20 | syl21anc 837 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵) → (◡𝐹 “ 𝑖) ∈ 𝐴) |
22 | 21, 1 | fmptd 6862 |
. . . . 5
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) |
23 | 22 | ffnd 6492 |
. . . 4
⊢ (𝜑 → 𝐺 Fn 𝐵) |
24 | | elpreima 6812 |
. . . 4
⊢ (𝐺 Fn 𝐵 → (𝑔 ∈ (◡𝐺 “ (𝑉‘𝐼)) ↔ (𝑔 ∈ 𝐵 ∧ (𝐺‘𝑔) ∈ (𝑉‘𝐼)))) |
25 | 23, 24 | syl 17 |
. . 3
⊢ (𝜑 → (𝑔 ∈ (◡𝐺 “ (𝑉‘𝐼)) ↔ (𝑔 ∈ 𝐵 ∧ (𝐺‘𝑔) ∈ (𝑉‘𝐼)))) |
26 | | rhmpreimacnlem.w |
. . . . . . . . 9
⊢ 𝑊 = (𝑗 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑗 ⊆ 𝑘}) |
27 | | sseq1 3913 |
. . . . . . . . . 10
⊢ (𝑗 = (𝐹 “ 𝐼) → (𝑗 ⊆ 𝑘 ↔ (𝐹 “ 𝐼) ⊆ 𝑘)) |
28 | 27 | rabbidv 3390 |
. . . . . . . . 9
⊢ (𝑗 = (𝐹 “ 𝐼) → {𝑘 ∈ 𝐵 ∣ 𝑗 ⊆ 𝑘} = {𝑘 ∈ 𝐵 ∣ (𝐹 “ 𝐼) ⊆ 𝑘}) |
29 | | rhmpreimacn.1 |
. . . . . . . . . 10
⊢ (𝜑 → ran 𝐹 = (Base‘𝑆)) |
30 | | rhmpreimacnlem.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) |
31 | | eqid 2759 |
. . . . . . . . . . 11
⊢
(Base‘𝑆) =
(Base‘𝑆) |
32 | | eqid 2759 |
. . . . . . . . . . 11
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
33 | | eqid 2759 |
. . . . . . . . . . 11
⊢
(LIdeal‘𝑆) =
(LIdeal‘𝑆) |
34 | 31, 32, 33 | rhmimaidl 31115 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = (Base‘𝑆) ∧ 𝐼 ∈ (LIdeal‘𝑅)) → (𝐹 “ 𝐼) ∈ (LIdeal‘𝑆)) |
35 | 4, 29, 30, 34 | syl3anc 1369 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 “ 𝐼) ∈ (LIdeal‘𝑆)) |
36 | 17 | fvexi 6665 |
. . . . . . . . . . 11
⊢ 𝐵 ∈ V |
37 | 36 | rabex 5195 |
. . . . . . . . . 10
⊢ {𝑘 ∈ 𝐵 ∣ (𝐹 “ 𝐼) ⊆ 𝑘} ∈ V |
38 | 37 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → {𝑘 ∈ 𝐵 ∣ (𝐹 “ 𝐼) ⊆ 𝑘} ∈ V) |
39 | 26, 28, 35, 38 | fvmptd3 6775 |
. . . . . . . 8
⊢ (𝜑 → (𝑊‘(𝐹 “ 𝐼)) = {𝑘 ∈ 𝐵 ∣ (𝐹 “ 𝐼) ⊆ 𝑘}) |
40 | 39 | eleq2d 2836 |
. . . . . . 7
⊢ (𝜑 → (𝑔 ∈ (𝑊‘(𝐹 “ 𝐼)) ↔ 𝑔 ∈ {𝑘 ∈ 𝐵 ∣ (𝐹 “ 𝐼) ⊆ 𝑘})) |
41 | | sseq2 3914 |
. . . . . . . 8
⊢ (𝑘 = 𝑔 → ((𝐹 “ 𝐼) ⊆ 𝑘 ↔ (𝐹 “ 𝐼) ⊆ 𝑔)) |
42 | 41 | elrab 3600 |
. . . . . . 7
⊢ (𝑔 ∈ {𝑘 ∈ 𝐵 ∣ (𝐹 “ 𝐼) ⊆ 𝑘} ↔ (𝑔 ∈ 𝐵 ∧ (𝐹 “ 𝐼) ⊆ 𝑔)) |
43 | 40, 42 | syl6bb 291 |
. . . . . 6
⊢ (𝜑 → (𝑔 ∈ (𝑊‘(𝐹 “ 𝐼)) ↔ (𝑔 ∈ 𝐵 ∧ (𝐹 “ 𝐼) ⊆ 𝑔))) |
44 | | eqid 2759 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
45 | 44, 31 | rhmf 19534 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:(Base‘𝑅)⟶(Base‘𝑆)) |
46 | 4, 45 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:(Base‘𝑅)⟶(Base‘𝑆)) |
47 | 46 | ffund 6495 |
. . . . . . . 8
⊢ (𝜑 → Fun 𝐹) |
48 | 44, 32 | lidlss 20036 |
. . . . . . . . . 10
⊢ (𝐼 ∈ (LIdeal‘𝑅) → 𝐼 ⊆ (Base‘𝑅)) |
49 | 30, 48 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ⊆ (Base‘𝑅)) |
50 | 46 | fdmd 6501 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = (Base‘𝑅)) |
51 | 49, 50 | sseqtrrd 3929 |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ⊆ dom 𝐹) |
52 | | funimass3 6808 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝐼 ⊆ dom 𝐹) → ((𝐹 “ 𝐼) ⊆ 𝑔 ↔ 𝐼 ⊆ (◡𝐹 “ 𝑔))) |
53 | 47, 51, 52 | syl2anc 588 |
. . . . . . 7
⊢ (𝜑 → ((𝐹 “ 𝐼) ⊆ 𝑔 ↔ 𝐼 ⊆ (◡𝐹 “ 𝑔))) |
54 | 53 | anbi2d 632 |
. . . . . 6
⊢ (𝜑 → ((𝑔 ∈ 𝐵 ∧ (𝐹 “ 𝐼) ⊆ 𝑔) ↔ (𝑔 ∈ 𝐵 ∧ 𝐼 ⊆ (◡𝐹 “ 𝑔)))) |
55 | 13 | adantr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → 𝑆 ∈ CRing) |
56 | 4 | adantr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
57 | 3, 17 | eleqtrdi 2861 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ (PrmIdeal‘𝑆)) |
58 | 19 | rhmpreimaprmidl 31133 |
. . . . . . . . 9
⊢ (((𝑆 ∈ CRing ∧ 𝐹 ∈ (𝑅 RingHom 𝑆)) ∧ 𝑔 ∈ (PrmIdeal‘𝑆)) → (◡𝐹 “ 𝑔) ∈ 𝐴) |
59 | 55, 56, 57, 58 | syl21anc 837 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (◡𝐹 “ 𝑔) ∈ 𝐴) |
60 | 59 | biantrurd 537 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (𝐼 ⊆ (◡𝐹 “ 𝑔) ↔ ((◡𝐹 “ 𝑔) ∈ 𝐴 ∧ 𝐼 ⊆ (◡𝐹 “ 𝑔)))) |
61 | 60 | pm5.32da 583 |
. . . . . 6
⊢ (𝜑 → ((𝑔 ∈ 𝐵 ∧ 𝐼 ⊆ (◡𝐹 “ 𝑔)) ↔ (𝑔 ∈ 𝐵 ∧ ((◡𝐹 “ 𝑔) ∈ 𝐴 ∧ 𝐼 ⊆ (◡𝐹 “ 𝑔))))) |
62 | 43, 54, 61 | 3bitrd 309 |
. . . . 5
⊢ (𝜑 → (𝑔 ∈ (𝑊‘(𝐹 “ 𝐼)) ↔ (𝑔 ∈ 𝐵 ∧ ((◡𝐹 “ 𝑔) ∈ 𝐴 ∧ 𝐼 ⊆ (◡𝐹 “ 𝑔))))) |
63 | | sseq2 3914 |
. . . . . . 7
⊢ (𝑘 = (◡𝐹 “ 𝑔) → (𝐼 ⊆ 𝑘 ↔ 𝐼 ⊆ (◡𝐹 “ 𝑔))) |
64 | 63 | elrab 3600 |
. . . . . 6
⊢ ((◡𝐹 “ 𝑔) ∈ {𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘} ↔ ((◡𝐹 “ 𝑔) ∈ 𝐴 ∧ 𝐼 ⊆ (◡𝐹 “ 𝑔))) |
65 | 64 | anbi2i 626 |
. . . . 5
⊢ ((𝑔 ∈ 𝐵 ∧ (◡𝐹 “ 𝑔) ∈ {𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘}) ↔ (𝑔 ∈ 𝐵 ∧ ((◡𝐹 “ 𝑔) ∈ 𝐴 ∧ 𝐼 ⊆ (◡𝐹 “ 𝑔)))) |
66 | 62, 65 | bitr4di 293 |
. . . 4
⊢ (𝜑 → (𝑔 ∈ (𝑊‘(𝐹 “ 𝐼)) ↔ (𝑔 ∈ 𝐵 ∧ (◡𝐹 “ 𝑔) ∈ {𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘}))) |
67 | | rhmpreimacnlem.v |
. . . . . . 7
⊢ 𝑉 = (𝑗 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑗 ⊆ 𝑘}) |
68 | | sseq1 3913 |
. . . . . . . 8
⊢ (𝑗 = 𝐼 → (𝑗 ⊆ 𝑘 ↔ 𝐼 ⊆ 𝑘)) |
69 | 68 | rabbidv 3390 |
. . . . . . 7
⊢ (𝑗 = 𝐼 → {𝑘 ∈ 𝐴 ∣ 𝑗 ⊆ 𝑘} = {𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘}) |
70 | 19 | fvexi 6665 |
. . . . . . . . 9
⊢ 𝐴 ∈ V |
71 | 70 | rabex 5195 |
. . . . . . . 8
⊢ {𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘} ∈ V |
72 | 71 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → {𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘} ∈ V) |
73 | 67, 69, 30, 72 | fvmptd3 6775 |
. . . . . 6
⊢ (𝜑 → (𝑉‘𝐼) = {𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘}) |
74 | 73 | eleq2d 2836 |
. . . . 5
⊢ (𝜑 → ((◡𝐹 “ 𝑔) ∈ (𝑉‘𝐼) ↔ (◡𝐹 “ 𝑔) ∈ {𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘})) |
75 | 74 | anbi2d 632 |
. . . 4
⊢ (𝜑 → ((𝑔 ∈ 𝐵 ∧ (◡𝐹 “ 𝑔) ∈ (𝑉‘𝐼)) ↔ (𝑔 ∈ 𝐵 ∧ (◡𝐹 “ 𝑔) ∈ {𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘}))) |
76 | 66, 75 | bitr4d 285 |
. . 3
⊢ (𝜑 → (𝑔 ∈ (𝑊‘(𝐹 “ 𝐼)) ↔ (𝑔 ∈ 𝐵 ∧ (◡𝐹 “ 𝑔) ∈ (𝑉‘𝐼)))) |
77 | 12, 25, 76 | 3bitr4rd 316 |
. 2
⊢ (𝜑 → (𝑔 ∈ (𝑊‘(𝐹 “ 𝐼)) ↔ 𝑔 ∈ (◡𝐺 “ (𝑉‘𝐼)))) |
78 | 77 | eqrdv 2757 |
1
⊢ (𝜑 → (𝑊‘(𝐹 “ 𝐼)) = (◡𝐺 “ (𝑉‘𝐼))) |