| Step | Hyp | Ref
| Expression |
| 1 | | neeq1 3003 |
. . . 4
⊢ (𝑝 = ∪
𝑍 → (𝑝 ≠ 𝐵 ↔ ∪ 𝑍 ≠ 𝐵)) |
| 2 | | sseq2 4010 |
. . . 4
⊢ (𝑝 = ∪
𝑍 → (𝐼 ⊆ 𝑝 ↔ 𝐼 ⊆ ∪ 𝑍)) |
| 3 | 1, 2 | anbi12d 632 |
. . 3
⊢ (𝑝 = ∪
𝑍 → ((𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝) ↔ (∪ 𝑍 ≠ 𝐵 ∧ 𝐼 ⊆ ∪ 𝑍))) |
| 4 | | ssmxidllem2.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ⊆ 𝑃) |
| 5 | | ssmxidllem.1 |
. . . . . . . . . 10
⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ (𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝)} |
| 6 | 5 | ssrab3 4082 |
. . . . . . . . 9
⊢ 𝑃 ⊆ (LIdeal‘𝑅) |
| 7 | 4, 6 | sstrdi 3996 |
. . . . . . . 8
⊢ (𝜑 → 𝑍 ⊆ (LIdeal‘𝑅)) |
| 8 | 7 | sselda 3983 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ (LIdeal‘𝑅)) |
| 9 | | ssmxidl.1 |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑅) |
| 10 | | eqid 2737 |
. . . . . . . 8
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
| 11 | 9, 10 | lidlss 21222 |
. . . . . . 7
⊢ (𝑗 ∈ (LIdeal‘𝑅) → 𝑗 ⊆ 𝐵) |
| 12 | 8, 11 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ⊆ 𝐵) |
| 13 | 12 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ 𝑍 𝑗 ⊆ 𝐵) |
| 14 | | unissb 4939 |
. . . . 5
⊢ (∪ 𝑍
⊆ 𝐵 ↔
∀𝑗 ∈ 𝑍 𝑗 ⊆ 𝐵) |
| 15 | 13, 14 | sylibr 234 |
. . . 4
⊢ (𝜑 → ∪ 𝑍
⊆ 𝐵) |
| 16 | | ssmxidllem2.2 |
. . . . . . 7
⊢ (𝜑 → 𝑍 ≠ ∅) |
| 17 | | ssmxidllem.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 18 | 17 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑅 ∈ Ring) |
| 19 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 20 | 10, 19 | lidl0cl 21230 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅)) →
(0g‘𝑅)
∈ 𝑗) |
| 21 | 18, 8, 20 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (0g‘𝑅) ∈ 𝑗) |
| 22 | | n0i 4340 |
. . . . . . . . 9
⊢
((0g‘𝑅) ∈ 𝑗 → ¬ 𝑗 = ∅) |
| 23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ¬ 𝑗 = ∅) |
| 24 | 23 | reximdva0 4355 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑍 ≠ ∅) → ∃𝑗 ∈ 𝑍 ¬ 𝑗 = ∅) |
| 25 | 16, 24 | mpdan 687 |
. . . . . 6
⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ¬ 𝑗 = ∅) |
| 26 | | rexnal 3100 |
. . . . . 6
⊢
(∃𝑗 ∈
𝑍 ¬ 𝑗 = ∅ ↔ ¬ ∀𝑗 ∈ 𝑍 𝑗 = ∅) |
| 27 | 25, 26 | sylib 218 |
. . . . 5
⊢ (𝜑 → ¬ ∀𝑗 ∈ 𝑍 𝑗 = ∅) |
| 28 | | uni0c 4934 |
. . . . . 6
⊢ (∪ 𝑍 =
∅ ↔ ∀𝑗
∈ 𝑍 𝑗 = ∅) |
| 29 | 28 | necon3abii 2987 |
. . . . 5
⊢ (∪ 𝑍
≠ ∅ ↔ ¬ ∀𝑗 ∈ 𝑍 𝑗 = ∅) |
| 30 | 27, 29 | sylibr 234 |
. . . 4
⊢ (𝜑 → ∪ 𝑍
≠ ∅) |
| 31 | | eluni2 4911 |
. . . . . . . 8
⊢ (𝑎 ∈ ∪ 𝑍
↔ ∃𝑖 ∈
𝑍 𝑎 ∈ 𝑖) |
| 32 | | eluni2 4911 |
. . . . . . . 8
⊢ (𝑏 ∈ ∪ 𝑍
↔ ∃𝑗 ∈
𝑍 𝑏 ∈ 𝑗) |
| 33 | 31, 32 | anbi12i 628 |
. . . . . . 7
⊢ ((𝑎 ∈ ∪ 𝑍
∧ 𝑏 ∈ ∪ 𝑍)
↔ (∃𝑖 ∈
𝑍 𝑎 ∈ 𝑖 ∧ ∃𝑗 ∈ 𝑍 𝑏 ∈ 𝑗)) |
| 34 | | an32 646 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ ∃𝑖 ∈ 𝑍 𝑎 ∈ 𝑖) ∧ 𝑗 ∈ 𝑍) ↔ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ ∃𝑖 ∈ 𝑍 𝑎 ∈ 𝑖)) |
| 35 | 17 | ad6antr 736 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → 𝑅 ∈ Ring) |
| 36 | 7 | ad5antr 734 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) → 𝑍 ⊆ (LIdeal‘𝑅)) |
| 37 | | simp-4r 784 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) → 𝑗 ∈ 𝑍) |
| 38 | 36, 37 | sseldd 3984 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) → 𝑗 ∈ (LIdeal‘𝑅)) |
| 39 | 38 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → 𝑗 ∈ (LIdeal‘𝑅)) |
| 40 | | simp-6r 788 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → 𝑥 ∈ 𝐵) |
| 41 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → 𝑖 ⊆ 𝑗) |
| 42 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → 𝑎 ∈ 𝑖) |
| 43 | 41, 42 | sseldd 3984 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → 𝑎 ∈ 𝑗) |
| 44 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 45 | 10, 9, 44 | lidlmcl 21235 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝑗)) → (𝑥(.r‘𝑅)𝑎) ∈ 𝑗) |
| 46 | 35, 39, 40, 43, 45 | syl22anc 839 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → (𝑥(.r‘𝑅)𝑎) ∈ 𝑗) |
| 47 | | simp-4r 784 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → 𝑏 ∈ 𝑗) |
| 48 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 49 | 10, 48 | lidlacl 21231 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅)) ∧ ((𝑥(.r‘𝑅)𝑎) ∈ 𝑗 ∧ 𝑏 ∈ 𝑗)) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ 𝑗) |
| 50 | 35, 39, 46, 47, 49 | syl22anc 839 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ 𝑗) |
| 51 | 37 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → 𝑗 ∈ 𝑍) |
| 52 | | elunii 4912 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ 𝑗 ∧ 𝑗 ∈ 𝑍) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ ∪ 𝑍) |
| 53 | 50, 51, 52 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ ∪ 𝑍) |
| 54 | 17 | ad6antr 736 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → 𝑅 ∈ Ring) |
| 55 | 36 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → 𝑍 ⊆ (LIdeal‘𝑅)) |
| 56 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) → 𝑖 ∈ 𝑍) |
| 57 | 56 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → 𝑖 ∈ 𝑍) |
| 58 | 55, 57 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → 𝑖 ∈ (LIdeal‘𝑅)) |
| 59 | | simp-6r 788 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → 𝑥 ∈ 𝐵) |
| 60 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → 𝑎 ∈ 𝑖) |
| 61 | 10, 9, 44 | lidlmcl 21235 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝑖)) → (𝑥(.r‘𝑅)𝑎) ∈ 𝑖) |
| 62 | 54, 58, 59, 60, 61 | syl22anc 839 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → (𝑥(.r‘𝑅)𝑎) ∈ 𝑖) |
| 63 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → 𝑗 ⊆ 𝑖) |
| 64 | | simp-4r 784 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → 𝑏 ∈ 𝑗) |
| 65 | 63, 64 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → 𝑏 ∈ 𝑖) |
| 66 | 10, 48 | lidlacl 21231 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑥(.r‘𝑅)𝑎) ∈ 𝑖 ∧ 𝑏 ∈ 𝑖)) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ 𝑖) |
| 67 | 54, 58, 62, 65, 66 | syl22anc 839 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ 𝑖) |
| 68 | | elunii 4912 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ 𝑖 ∧ 𝑖 ∈ 𝑍) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ ∪ 𝑍) |
| 69 | 67, 57, 68 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ ∪ 𝑍) |
| 70 | | ssmxidllem2.3 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → [⊊] Or 𝑍) |
| 71 | 70 | ad5antr 734 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) → [⊊] Or 𝑍) |
| 72 | | sorpssi 7749 |
. . . . . . . . . . . . . 14
⊢ ((
[⊊] Or 𝑍
∧ (𝑖 ∈ 𝑍 ∧ 𝑗 ∈ 𝑍)) → (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖)) |
| 73 | 71, 56, 37, 72 | syl12anc 837 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) → (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖)) |
| 74 | 53, 69, 73 | mpjaodan 961 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ ∪ 𝑍) |
| 75 | 74 | r19.29an 3158 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ ∃𝑖 ∈ 𝑍 𝑎 ∈ 𝑖) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ ∪ 𝑍) |
| 76 | 75 | an32s 652 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ ∃𝑖 ∈ 𝑍 𝑎 ∈ 𝑖) ∧ 𝑏 ∈ 𝑗) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ ∪ 𝑍) |
| 77 | 34, 76 | sylanb 581 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ ∃𝑖 ∈ 𝑍 𝑎 ∈ 𝑖) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ ∪ 𝑍) |
| 78 | 77 | r19.29an 3158 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ ∃𝑖 ∈ 𝑍 𝑎 ∈ 𝑖) ∧ ∃𝑗 ∈ 𝑍 𝑏 ∈ 𝑗) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ ∪ 𝑍) |
| 79 | 78 | anasss 466 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (∃𝑖 ∈ 𝑍 𝑎 ∈ 𝑖 ∧ ∃𝑗 ∈ 𝑍 𝑏 ∈ 𝑗)) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ ∪ 𝑍) |
| 80 | 33, 79 | sylan2b 594 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑎 ∈ ∪ 𝑍 ∧ 𝑏 ∈ ∪ 𝑍)) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ ∪ 𝑍) |
| 81 | 80 | ralrimivva 3202 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑎 ∈ ∪ 𝑍∀𝑏 ∈ ∪ 𝑍((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ ∪ 𝑍) |
| 82 | 81 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ ∪ 𝑍∀𝑏 ∈ ∪ 𝑍((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ ∪ 𝑍) |
| 83 | 10, 9, 48, 44 | islidl 21225 |
. . . 4
⊢ (∪ 𝑍
∈ (LIdeal‘𝑅)
↔ (∪ 𝑍 ⊆ 𝐵 ∧ ∪ 𝑍 ≠ ∅ ∧
∀𝑥 ∈ 𝐵 ∀𝑎 ∈ ∪ 𝑍∀𝑏 ∈ ∪ 𝑍((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ ∪ 𝑍)) |
| 84 | 15, 30, 82, 83 | syl3anbrc 1344 |
. . 3
⊢ (𝜑 → ∪ 𝑍
∈ (LIdeal‘𝑅)) |
| 85 | 4 | sselda 3983 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ 𝑃) |
| 86 | | neeq1 3003 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑗 → (𝑝 ≠ 𝐵 ↔ 𝑗 ≠ 𝐵)) |
| 87 | | sseq2 4010 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑗 → (𝐼 ⊆ 𝑝 ↔ 𝐼 ⊆ 𝑗)) |
| 88 | 86, 87 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑗 → ((𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝) ↔ (𝑗 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑗))) |
| 89 | 88, 5 | elrab2 3695 |
. . . . . . . . . 10
⊢ (𝑗 ∈ 𝑃 ↔ (𝑗 ∈ (LIdeal‘𝑅) ∧ (𝑗 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑗))) |
| 90 | 85, 89 | sylib 218 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝑗 ∈ (LIdeal‘𝑅) ∧ (𝑗 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑗))) |
| 91 | 90 | simprld 772 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ≠ 𝐵) |
| 92 | | eqid 2737 |
. . . . . . . . 9
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 93 | 9, 92 | pridln1 33471 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅) ∧ 𝑗 ≠ 𝐵) → ¬ (1r‘𝑅) ∈ 𝑗) |
| 94 | 18, 8, 91, 93 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ¬ (1r‘𝑅) ∈ 𝑗) |
| 95 | 94 | nrexdv 3149 |
. . . . . 6
⊢ (𝜑 → ¬ ∃𝑗 ∈ 𝑍 (1r‘𝑅) ∈ 𝑗) |
| 96 | | eluni2 4911 |
. . . . . 6
⊢
((1r‘𝑅) ∈ ∪ 𝑍 ↔ ∃𝑗 ∈ 𝑍 (1r‘𝑅) ∈ 𝑗) |
| 97 | 95, 96 | sylnibr 329 |
. . . . 5
⊢ (𝜑 → ¬
(1r‘𝑅)
∈ ∪ 𝑍) |
| 98 | 10, 9, 92 | lidl1el 21236 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ ∪ 𝑍
∈ (LIdeal‘𝑅))
→ ((1r‘𝑅) ∈ ∪ 𝑍 ↔ ∪ 𝑍 =
𝐵)) |
| 99 | 17, 84, 98 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 →
((1r‘𝑅)
∈ ∪ 𝑍 ↔ ∪ 𝑍 = 𝐵)) |
| 100 | 99 | necon3bbid 2978 |
. . . . 5
⊢ (𝜑 → (¬
(1r‘𝑅)
∈ ∪ 𝑍 ↔ ∪ 𝑍 ≠ 𝐵)) |
| 101 | 97, 100 | mpbid 232 |
. . . 4
⊢ (𝜑 → ∪ 𝑍
≠ 𝐵) |
| 102 | 90 | simprrd 774 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝐼 ⊆ 𝑗) |
| 103 | 102 | ralrimiva 3146 |
. . . . . 6
⊢ (𝜑 → ∀𝑗 ∈ 𝑍 𝐼 ⊆ 𝑗) |
| 104 | | ssint 4964 |
. . . . . 6
⊢ (𝐼 ⊆ ∩ 𝑍
↔ ∀𝑗 ∈
𝑍 𝐼 ⊆ 𝑗) |
| 105 | 103, 104 | sylibr 234 |
. . . . 5
⊢ (𝜑 → 𝐼 ⊆ ∩ 𝑍) |
| 106 | | intssuni 4970 |
. . . . . 6
⊢ (𝑍 ≠ ∅ → ∩ 𝑍
⊆ ∪ 𝑍) |
| 107 | 16, 106 | syl 17 |
. . . . 5
⊢ (𝜑 → ∩ 𝑍
⊆ ∪ 𝑍) |
| 108 | 105, 107 | sstrd 3994 |
. . . 4
⊢ (𝜑 → 𝐼 ⊆ ∪ 𝑍) |
| 109 | 101, 108 | jca 511 |
. . 3
⊢ (𝜑 → (∪ 𝑍
≠ 𝐵 ∧ 𝐼 ⊆ ∪ 𝑍)) |
| 110 | 3, 84, 109 | elrabd 3694 |
. 2
⊢ (𝜑 → ∪ 𝑍
∈ {𝑝 ∈
(LIdeal‘𝑅) ∣
(𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝)}) |
| 111 | 110, 5 | eleqtrrdi 2852 |
1
⊢ (𝜑 → ∪ 𝑍
∈ 𝑃) |