| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rhmpreimacn.g | . . . . . 6
⊢ 𝐺 = (𝑖 ∈ 𝐵 ↦ (◡𝐹 “ 𝑖)) | 
| 2 |  | imaeq2 6074 | . . . . . 6
⊢ (𝑖 = 𝑔 → (◡𝐹 “ 𝑖) = (◡𝐹 “ 𝑔)) | 
| 3 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ 𝐵) | 
| 4 |  | rhmpreimacn.f | . . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) | 
| 5 | 4 | elexd 3504 | . . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ V) | 
| 6 |  | cnvexg 7946 | . . . . . . . 8
⊢ (𝐹 ∈ V → ◡𝐹 ∈ V) | 
| 7 |  | imaexg 7935 | . . . . . . . 8
⊢ (◡𝐹 ∈ V → (◡𝐹 “ 𝑔) ∈ V) | 
| 8 | 5, 6, 7 | 3syl 18 | . . . . . . 7
⊢ (𝜑 → (◡𝐹 “ 𝑔) ∈ V) | 
| 9 | 8 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (◡𝐹 “ 𝑔) ∈ V) | 
| 10 | 1, 2, 3, 9 | fvmptd3 7039 | . . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (𝐺‘𝑔) = (◡𝐹 “ 𝑔)) | 
| 11 | 10 | eleq1d 2826 | . . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → ((𝐺‘𝑔) ∈ (𝑉‘𝐼) ↔ (◡𝐹 “ 𝑔) ∈ (𝑉‘𝐼))) | 
| 12 | 11 | pm5.32da 579 | . . 3
⊢ (𝜑 → ((𝑔 ∈ 𝐵 ∧ (𝐺‘𝑔) ∈ (𝑉‘𝐼)) ↔ (𝑔 ∈ 𝐵 ∧ (◡𝐹 “ 𝑔) ∈ (𝑉‘𝐼)))) | 
| 13 |  | rhmpreimacn.s | . . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ CRing) | 
| 14 | 13 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵) → 𝑆 ∈ CRing) | 
| 15 | 4 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵) → 𝐹 ∈ (𝑅 RingHom 𝑆)) | 
| 16 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵) → 𝑖 ∈ 𝐵) | 
| 17 |  | rhmpreimacn.b | . . . . . . . 8
⊢ 𝐵 = (PrmIdeal‘𝑆) | 
| 18 | 16, 17 | eleqtrdi 2851 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵) → 𝑖 ∈ (PrmIdeal‘𝑆)) | 
| 19 |  | rhmpreimacn.a | . . . . . . . 8
⊢ 𝐴 = (PrmIdeal‘𝑅) | 
| 20 | 19 | rhmpreimaprmidl 33479 | . . . . . . 7
⊢ (((𝑆 ∈ CRing ∧ 𝐹 ∈ (𝑅 RingHom 𝑆)) ∧ 𝑖 ∈ (PrmIdeal‘𝑆)) → (◡𝐹 “ 𝑖) ∈ 𝐴) | 
| 21 | 14, 15, 18, 20 | syl21anc 838 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵) → (◡𝐹 “ 𝑖) ∈ 𝐴) | 
| 22 | 21, 1 | fmptd 7134 | . . . . 5
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) | 
| 23 | 22 | ffnd 6737 | . . . 4
⊢ (𝜑 → 𝐺 Fn 𝐵) | 
| 24 |  | elpreima 7078 | . . . 4
⊢ (𝐺 Fn 𝐵 → (𝑔 ∈ (◡𝐺 “ (𝑉‘𝐼)) ↔ (𝑔 ∈ 𝐵 ∧ (𝐺‘𝑔) ∈ (𝑉‘𝐼)))) | 
| 25 | 23, 24 | syl 17 | . . 3
⊢ (𝜑 → (𝑔 ∈ (◡𝐺 “ (𝑉‘𝐼)) ↔ (𝑔 ∈ 𝐵 ∧ (𝐺‘𝑔) ∈ (𝑉‘𝐼)))) | 
| 26 |  | rhmpreimacnlem.w | . . . . . . . . 9
⊢ 𝑊 = (𝑗 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑗 ⊆ 𝑘}) | 
| 27 |  | sseq1 4009 | . . . . . . . . . 10
⊢ (𝑗 = (𝐹 “ 𝐼) → (𝑗 ⊆ 𝑘 ↔ (𝐹 “ 𝐼) ⊆ 𝑘)) | 
| 28 | 27 | rabbidv 3444 | . . . . . . . . 9
⊢ (𝑗 = (𝐹 “ 𝐼) → {𝑘 ∈ 𝐵 ∣ 𝑗 ⊆ 𝑘} = {𝑘 ∈ 𝐵 ∣ (𝐹 “ 𝐼) ⊆ 𝑘}) | 
| 29 |  | rhmpreimacn.1 | . . . . . . . . . 10
⊢ (𝜑 → ran 𝐹 = (Base‘𝑆)) | 
| 30 |  | rhmpreimacnlem.1 | . . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) | 
| 31 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(Base‘𝑆) =
(Base‘𝑆) | 
| 32 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) | 
| 33 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(LIdeal‘𝑆) =
(LIdeal‘𝑆) | 
| 34 | 31, 32, 33 | rhmimaidl 33460 | . . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = (Base‘𝑆) ∧ 𝐼 ∈ (LIdeal‘𝑅)) → (𝐹 “ 𝐼) ∈ (LIdeal‘𝑆)) | 
| 35 | 4, 29, 30, 34 | syl3anc 1373 | . . . . . . . . 9
⊢ (𝜑 → (𝐹 “ 𝐼) ∈ (LIdeal‘𝑆)) | 
| 36 | 17 | fvexi 6920 | . . . . . . . . . . 11
⊢ 𝐵 ∈ V | 
| 37 | 36 | rabex 5339 | . . . . . . . . . 10
⊢ {𝑘 ∈ 𝐵 ∣ (𝐹 “ 𝐼) ⊆ 𝑘} ∈ V | 
| 38 | 37 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → {𝑘 ∈ 𝐵 ∣ (𝐹 “ 𝐼) ⊆ 𝑘} ∈ V) | 
| 39 | 26, 28, 35, 38 | fvmptd3 7039 | . . . . . . . 8
⊢ (𝜑 → (𝑊‘(𝐹 “ 𝐼)) = {𝑘 ∈ 𝐵 ∣ (𝐹 “ 𝐼) ⊆ 𝑘}) | 
| 40 | 39 | eleq2d 2827 | . . . . . . 7
⊢ (𝜑 → (𝑔 ∈ (𝑊‘(𝐹 “ 𝐼)) ↔ 𝑔 ∈ {𝑘 ∈ 𝐵 ∣ (𝐹 “ 𝐼) ⊆ 𝑘})) | 
| 41 |  | sseq2 4010 | . . . . . . . 8
⊢ (𝑘 = 𝑔 → ((𝐹 “ 𝐼) ⊆ 𝑘 ↔ (𝐹 “ 𝐼) ⊆ 𝑔)) | 
| 42 | 41 | elrab 3692 | . . . . . . 7
⊢ (𝑔 ∈ {𝑘 ∈ 𝐵 ∣ (𝐹 “ 𝐼) ⊆ 𝑘} ↔ (𝑔 ∈ 𝐵 ∧ (𝐹 “ 𝐼) ⊆ 𝑔)) | 
| 43 | 40, 42 | bitrdi 287 | . . . . . 6
⊢ (𝜑 → (𝑔 ∈ (𝑊‘(𝐹 “ 𝐼)) ↔ (𝑔 ∈ 𝐵 ∧ (𝐹 “ 𝐼) ⊆ 𝑔))) | 
| 44 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 45 | 44, 31 | rhmf 20485 | . . . . . . . . . 10
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:(Base‘𝑅)⟶(Base‘𝑆)) | 
| 46 | 4, 45 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝐹:(Base‘𝑅)⟶(Base‘𝑆)) | 
| 47 | 46 | ffund 6740 | . . . . . . . 8
⊢ (𝜑 → Fun 𝐹) | 
| 48 | 44, 32 | lidlss 21222 | . . . . . . . . . 10
⊢ (𝐼 ∈ (LIdeal‘𝑅) → 𝐼 ⊆ (Base‘𝑅)) | 
| 49 | 30, 48 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝐼 ⊆ (Base‘𝑅)) | 
| 50 | 46 | fdmd 6746 | . . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = (Base‘𝑅)) | 
| 51 | 49, 50 | sseqtrrd 4021 | . . . . . . . 8
⊢ (𝜑 → 𝐼 ⊆ dom 𝐹) | 
| 52 |  | funimass3 7074 | . . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝐼 ⊆ dom 𝐹) → ((𝐹 “ 𝐼) ⊆ 𝑔 ↔ 𝐼 ⊆ (◡𝐹 “ 𝑔))) | 
| 53 | 47, 51, 52 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → ((𝐹 “ 𝐼) ⊆ 𝑔 ↔ 𝐼 ⊆ (◡𝐹 “ 𝑔))) | 
| 54 | 53 | anbi2d 630 | . . . . . 6
⊢ (𝜑 → ((𝑔 ∈ 𝐵 ∧ (𝐹 “ 𝐼) ⊆ 𝑔) ↔ (𝑔 ∈ 𝐵 ∧ 𝐼 ⊆ (◡𝐹 “ 𝑔)))) | 
| 55 | 13 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → 𝑆 ∈ CRing) | 
| 56 | 4 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → 𝐹 ∈ (𝑅 RingHom 𝑆)) | 
| 57 | 3, 17 | eleqtrdi 2851 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ (PrmIdeal‘𝑆)) | 
| 58 | 19 | rhmpreimaprmidl 33479 | . . . . . . . . 9
⊢ (((𝑆 ∈ CRing ∧ 𝐹 ∈ (𝑅 RingHom 𝑆)) ∧ 𝑔 ∈ (PrmIdeal‘𝑆)) → (◡𝐹 “ 𝑔) ∈ 𝐴) | 
| 59 | 55, 56, 57, 58 | syl21anc 838 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (◡𝐹 “ 𝑔) ∈ 𝐴) | 
| 60 | 59 | biantrurd 532 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (𝐼 ⊆ (◡𝐹 “ 𝑔) ↔ ((◡𝐹 “ 𝑔) ∈ 𝐴 ∧ 𝐼 ⊆ (◡𝐹 “ 𝑔)))) | 
| 61 | 60 | pm5.32da 579 | . . . . . 6
⊢ (𝜑 → ((𝑔 ∈ 𝐵 ∧ 𝐼 ⊆ (◡𝐹 “ 𝑔)) ↔ (𝑔 ∈ 𝐵 ∧ ((◡𝐹 “ 𝑔) ∈ 𝐴 ∧ 𝐼 ⊆ (◡𝐹 “ 𝑔))))) | 
| 62 | 43, 54, 61 | 3bitrd 305 | . . . . 5
⊢ (𝜑 → (𝑔 ∈ (𝑊‘(𝐹 “ 𝐼)) ↔ (𝑔 ∈ 𝐵 ∧ ((◡𝐹 “ 𝑔) ∈ 𝐴 ∧ 𝐼 ⊆ (◡𝐹 “ 𝑔))))) | 
| 63 |  | sseq2 4010 | . . . . . . 7
⊢ (𝑘 = (◡𝐹 “ 𝑔) → (𝐼 ⊆ 𝑘 ↔ 𝐼 ⊆ (◡𝐹 “ 𝑔))) | 
| 64 | 63 | elrab 3692 | . . . . . 6
⊢ ((◡𝐹 “ 𝑔) ∈ {𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘} ↔ ((◡𝐹 “ 𝑔) ∈ 𝐴 ∧ 𝐼 ⊆ (◡𝐹 “ 𝑔))) | 
| 65 | 64 | anbi2i 623 | . . . . 5
⊢ ((𝑔 ∈ 𝐵 ∧ (◡𝐹 “ 𝑔) ∈ {𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘}) ↔ (𝑔 ∈ 𝐵 ∧ ((◡𝐹 “ 𝑔) ∈ 𝐴 ∧ 𝐼 ⊆ (◡𝐹 “ 𝑔)))) | 
| 66 | 62, 65 | bitr4di 289 | . . . 4
⊢ (𝜑 → (𝑔 ∈ (𝑊‘(𝐹 “ 𝐼)) ↔ (𝑔 ∈ 𝐵 ∧ (◡𝐹 “ 𝑔) ∈ {𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘}))) | 
| 67 |  | rhmpreimacnlem.v | . . . . . . 7
⊢ 𝑉 = (𝑗 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑗 ⊆ 𝑘}) | 
| 68 |  | sseq1 4009 | . . . . . . . 8
⊢ (𝑗 = 𝐼 → (𝑗 ⊆ 𝑘 ↔ 𝐼 ⊆ 𝑘)) | 
| 69 | 68 | rabbidv 3444 | . . . . . . 7
⊢ (𝑗 = 𝐼 → {𝑘 ∈ 𝐴 ∣ 𝑗 ⊆ 𝑘} = {𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘}) | 
| 70 | 19 | fvexi 6920 | . . . . . . . . 9
⊢ 𝐴 ∈ V | 
| 71 | 70 | rabex 5339 | . . . . . . . 8
⊢ {𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘} ∈ V | 
| 72 | 71 | a1i 11 | . . . . . . 7
⊢ (𝜑 → {𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘} ∈ V) | 
| 73 | 67, 69, 30, 72 | fvmptd3 7039 | . . . . . 6
⊢ (𝜑 → (𝑉‘𝐼) = {𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘}) | 
| 74 | 73 | eleq2d 2827 | . . . . 5
⊢ (𝜑 → ((◡𝐹 “ 𝑔) ∈ (𝑉‘𝐼) ↔ (◡𝐹 “ 𝑔) ∈ {𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘})) | 
| 75 | 74 | anbi2d 630 | . . . 4
⊢ (𝜑 → ((𝑔 ∈ 𝐵 ∧ (◡𝐹 “ 𝑔) ∈ (𝑉‘𝐼)) ↔ (𝑔 ∈ 𝐵 ∧ (◡𝐹 “ 𝑔) ∈ {𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘}))) | 
| 76 | 66, 75 | bitr4d 282 | . . 3
⊢ (𝜑 → (𝑔 ∈ (𝑊‘(𝐹 “ 𝐼)) ↔ (𝑔 ∈ 𝐵 ∧ (◡𝐹 “ 𝑔) ∈ (𝑉‘𝐼)))) | 
| 77 | 12, 25, 76 | 3bitr4rd 312 | . 2
⊢ (𝜑 → (𝑔 ∈ (𝑊‘(𝐹 “ 𝐼)) ↔ 𝑔 ∈ (◡𝐺 “ (𝑉‘𝐼)))) | 
| 78 | 77 | eqrdv 2735 | 1
⊢ (𝜑 → (𝑊‘(𝐹 “ 𝐼)) = (◡𝐺 “ (𝑉‘𝐼))) |