| Step | Hyp | Ref
| Expression |
| 1 | | crngring 20242 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
| 2 | | prmidlidl 33472 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) → 𝑃 ∈ (LIdeal‘𝑅)) |
| 3 | 1, 2 | sylan 580 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) → 𝑃 ∈ (LIdeal‘𝑅)) |
| 4 | | isprmidlc.1 |
. . . . 5
⊢ 𝐵 = (Base‘𝑅) |
| 5 | | isprmidlc.2 |
. . . . 5
⊢ · =
(.r‘𝑅) |
| 6 | 4, 5 | prmidlnr 33467 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) → 𝑃 ≠ 𝐵) |
| 7 | 1, 6 | sylan 580 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) → 𝑃 ≠ 𝐵) |
| 8 | 1 | ad4antr 732 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) → 𝑅 ∈ Ring) |
| 9 | | simp-4r 784 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) → 𝑃 ∈ (PrmIdeal‘𝑅)) |
| 10 | | simpllr 776 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈ CRing
∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) → 𝑥 ∈ 𝐵) |
| 11 | 10 | snssd 4809 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ CRing
∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) → {𝑥} ⊆ 𝐵) |
| 12 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(RSpan‘𝑅) =
(RSpan‘𝑅) |
| 13 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
| 14 | 12, 4, 13 | rspcl 21245 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ {𝑥} ⊆ 𝐵) → ((RSpan‘𝑅)‘{𝑥}) ∈ (LIdeal‘𝑅)) |
| 15 | 8, 11, 14 | syl2anc 584 |
. . . . . . . . 9
⊢
(((((𝑅 ∈ CRing
∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) → ((RSpan‘𝑅)‘{𝑥}) ∈ (LIdeal‘𝑅)) |
| 16 | | simplr 769 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈ CRing
∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) → 𝑦 ∈ 𝐵) |
| 17 | 16 | snssd 4809 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ CRing
∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) → {𝑦} ⊆ 𝐵) |
| 18 | 12, 4, 13 | rspcl 21245 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ {𝑦} ⊆ 𝐵) → ((RSpan‘𝑅)‘{𝑦}) ∈ (LIdeal‘𝑅)) |
| 19 | 8, 17, 18 | syl2anc 584 |
. . . . . . . . 9
⊢
(((((𝑅 ∈ CRing
∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) → ((RSpan‘𝑅)‘{𝑦}) ∈ (LIdeal‘𝑅)) |
| 20 | 15, 19 | jca 511 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) → (((RSpan‘𝑅)‘{𝑥}) ∈ (LIdeal‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑦}) ∈ (LIdeal‘𝑅))) |
| 21 | | simpllr 776 |
. . . . . . . . . . . . . 14
⊢
(((((((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) ∧ 𝑚 ∈ 𝐵) ∧ 𝑟 = (𝑚 · 𝑥)) ∧ 𝑛 ∈ 𝐵) ∧ 𝑠 = (𝑛 · 𝑦)) → 𝑟 = (𝑚 · 𝑥)) |
| 22 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢
(((((((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) ∧ 𝑚 ∈ 𝐵) ∧ 𝑟 = (𝑚 · 𝑥)) ∧ 𝑛 ∈ 𝐵) ∧ 𝑠 = (𝑛 · 𝑦)) → 𝑠 = (𝑛 · 𝑦)) |
| 23 | 21, 22 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢
(((((((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) ∧ 𝑚 ∈ 𝐵) ∧ 𝑟 = (𝑚 · 𝑥)) ∧ 𝑛 ∈ 𝐵) ∧ 𝑠 = (𝑛 · 𝑦)) → (𝑟 · 𝑠) = ((𝑚 · 𝑥) · (𝑛 · 𝑦))) |
| 24 | | simp-10l 795 |
. . . . . . . . . . . . . . 15
⊢
(((((((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) ∧ 𝑚 ∈ 𝐵) ∧ 𝑟 = (𝑚 · 𝑥)) ∧ 𝑛 ∈ 𝐵) ∧ 𝑠 = (𝑛 · 𝑦)) → 𝑅 ∈ CRing) |
| 25 | | simp-4r 784 |
. . . . . . . . . . . . . . 15
⊢
(((((((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) ∧ 𝑚 ∈ 𝐵) ∧ 𝑟 = (𝑚 · 𝑥)) ∧ 𝑛 ∈ 𝐵) ∧ 𝑠 = (𝑛 · 𝑦)) → 𝑚 ∈ 𝐵) |
| 26 | 10 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) → 𝑥 ∈ 𝐵) |
| 27 | 26 | ad4antr 732 |
. . . . . . . . . . . . . . 15
⊢
(((((((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) ∧ 𝑚 ∈ 𝐵) ∧ 𝑟 = (𝑚 · 𝑥)) ∧ 𝑛 ∈ 𝐵) ∧ 𝑠 = (𝑛 · 𝑦)) → 𝑥 ∈ 𝐵) |
| 28 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢
(((((((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) ∧ 𝑚 ∈ 𝐵) ∧ 𝑟 = (𝑚 · 𝑥)) ∧ 𝑛 ∈ 𝐵) ∧ 𝑠 = (𝑛 · 𝑦)) → 𝑛 ∈ 𝐵) |
| 29 | 16 | ad4antr 732 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) ∧ 𝑚 ∈ 𝐵) ∧ 𝑟 = (𝑚 · 𝑥)) → 𝑦 ∈ 𝐵) |
| 30 | 29 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢
(((((((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) ∧ 𝑚 ∈ 𝐵) ∧ 𝑟 = (𝑚 · 𝑥)) ∧ 𝑛 ∈ 𝐵) ∧ 𝑠 = (𝑛 · 𝑦)) → 𝑦 ∈ 𝐵) |
| 31 | 4, 5 | cringm4 33474 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ CRing ∧ (𝑚 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) ∧ (𝑛 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑚 · 𝑥) · (𝑛 · 𝑦)) = ((𝑚 · 𝑛) · (𝑥 · 𝑦))) |
| 32 | 24, 25, 27, 28, 30, 31 | syl122anc 1381 |
. . . . . . . . . . . . . 14
⊢
(((((((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) ∧ 𝑚 ∈ 𝐵) ∧ 𝑟 = (𝑚 · 𝑥)) ∧ 𝑛 ∈ 𝐵) ∧ 𝑠 = (𝑛 · 𝑦)) → ((𝑚 · 𝑥) · (𝑛 · 𝑦)) = ((𝑚 · 𝑛) · (𝑥 · 𝑦))) |
| 33 | 24, 1 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) ∧ 𝑚 ∈ 𝐵) ∧ 𝑟 = (𝑚 · 𝑥)) ∧ 𝑛 ∈ 𝐵) ∧ 𝑠 = (𝑛 · 𝑦)) → 𝑅 ∈ Ring) |
| 34 | 3 | ad9antr 742 |
. . . . . . . . . . . . . . 15
⊢
(((((((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) ∧ 𝑚 ∈ 𝐵) ∧ 𝑟 = (𝑚 · 𝑥)) ∧ 𝑛 ∈ 𝐵) ∧ 𝑠 = (𝑛 · 𝑦)) → 𝑃 ∈ (LIdeal‘𝑅)) |
| 35 | 4, 5 | ringcl 20247 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Ring ∧ 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵) → (𝑚 · 𝑛) ∈ 𝐵) |
| 36 | 33, 25, 28, 35 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢
(((((((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) ∧ 𝑚 ∈ 𝐵) ∧ 𝑟 = (𝑚 · 𝑥)) ∧ 𝑛 ∈ 𝐵) ∧ 𝑠 = (𝑛 · 𝑦)) → (𝑚 · 𝑛) ∈ 𝐵) |
| 37 | | simp-7r 790 |
. . . . . . . . . . . . . . 15
⊢
(((((((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) ∧ 𝑚 ∈ 𝐵) ∧ 𝑟 = (𝑚 · 𝑥)) ∧ 𝑛 ∈ 𝐵) ∧ 𝑠 = (𝑛 · 𝑦)) → (𝑥 · 𝑦) ∈ 𝑃) |
| 38 | 13, 4, 5 | lidlmcl 21235 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Ring ∧ 𝑃 ∈ (LIdeal‘𝑅)) ∧ ((𝑚 · 𝑛) ∈ 𝐵 ∧ (𝑥 · 𝑦) ∈ 𝑃)) → ((𝑚 · 𝑛) · (𝑥 · 𝑦)) ∈ 𝑃) |
| 39 | 33, 34, 36, 37, 38 | syl22anc 839 |
. . . . . . . . . . . . . 14
⊢
(((((((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) ∧ 𝑚 ∈ 𝐵) ∧ 𝑟 = (𝑚 · 𝑥)) ∧ 𝑛 ∈ 𝐵) ∧ 𝑠 = (𝑛 · 𝑦)) → ((𝑚 · 𝑛) · (𝑥 · 𝑦)) ∈ 𝑃) |
| 40 | 32, 39 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢
(((((((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) ∧ 𝑚 ∈ 𝐵) ∧ 𝑟 = (𝑚 · 𝑥)) ∧ 𝑛 ∈ 𝐵) ∧ 𝑠 = (𝑛 · 𝑦)) → ((𝑚 · 𝑥) · (𝑛 · 𝑦)) ∈ 𝑃) |
| 41 | 23, 40 | eqeltrd 2841 |
. . . . . . . . . . . 12
⊢
(((((((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) ∧ 𝑚 ∈ 𝐵) ∧ 𝑟 = (𝑚 · 𝑥)) ∧ 𝑛 ∈ 𝐵) ∧ 𝑠 = (𝑛 · 𝑦)) → (𝑟 · 𝑠) ∈ 𝑃) |
| 42 | 8 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) → 𝑅 ∈ Ring) |
| 43 | 42 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢
(((((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) ∧ 𝑚 ∈ 𝐵) ∧ 𝑟 = (𝑚 · 𝑥)) → 𝑅 ∈ Ring) |
| 44 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢
(((((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) ∧ 𝑚 ∈ 𝐵) ∧ 𝑟 = (𝑚 · 𝑥)) → 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) |
| 45 | 4, 5, 12 | elrspsn 21250 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) → (𝑠 ∈ ((RSpan‘𝑅)‘{𝑦}) ↔ ∃𝑛 ∈ 𝐵 𝑠 = (𝑛 · 𝑦))) |
| 46 | 45 | biimpa 476 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) → ∃𝑛 ∈ 𝐵 𝑠 = (𝑛 · 𝑦)) |
| 47 | 43, 29, 44, 46 | syl21anc 838 |
. . . . . . . . . . . 12
⊢
(((((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) ∧ 𝑚 ∈ 𝐵) ∧ 𝑟 = (𝑚 · 𝑥)) → ∃𝑛 ∈ 𝐵 𝑠 = (𝑛 · 𝑦)) |
| 48 | 41, 47 | r19.29a 3162 |
. . . . . . . . . . 11
⊢
(((((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) ∧ 𝑚 ∈ 𝐵) ∧ 𝑟 = (𝑚 · 𝑥)) → (𝑟 · 𝑠) ∈ 𝑃) |
| 49 | | simplr 769 |
. . . . . . . . . . . 12
⊢
(((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) → 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) |
| 50 | 4, 5, 12 | elrspsn 21250 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) → (𝑟 ∈ ((RSpan‘𝑅)‘{𝑥}) ↔ ∃𝑚 ∈ 𝐵 𝑟 = (𝑚 · 𝑥))) |
| 51 | 50 | biimpa 476 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) → ∃𝑚 ∈ 𝐵 𝑟 = (𝑚 · 𝑥)) |
| 52 | 42, 26, 49, 51 | syl21anc 838 |
. . . . . . . . . . 11
⊢
(((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) → ∃𝑚 ∈ 𝐵 𝑟 = (𝑚 · 𝑥)) |
| 53 | 48, 52 | r19.29a 3162 |
. . . . . . . . . 10
⊢
(((((((𝑅 ∈
CRing ∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ 𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})) → (𝑟 · 𝑠) ∈ 𝑃) |
| 54 | 53 | anasss 466 |
. . . . . . . . 9
⊢
((((((𝑅 ∈ CRing
∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) ∧ (𝑟 ∈ ((RSpan‘𝑅)‘{𝑥}) ∧ 𝑠 ∈ ((RSpan‘𝑅)‘{𝑦}))) → (𝑟 · 𝑠) ∈ 𝑃) |
| 55 | 54 | ralrimivva 3202 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) → ∀𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})∀𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})(𝑟 · 𝑠) ∈ 𝑃) |
| 56 | 4, 5 | prmidl 33468 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ (((RSpan‘𝑅)‘{𝑥}) ∈ (LIdeal‘𝑅) ∧ ((RSpan‘𝑅)‘{𝑦}) ∈ (LIdeal‘𝑅))) ∧ ∀𝑟 ∈ ((RSpan‘𝑅)‘{𝑥})∀𝑠 ∈ ((RSpan‘𝑅)‘{𝑦})(𝑟 · 𝑠) ∈ 𝑃) → (((RSpan‘𝑅)‘{𝑥}) ⊆ 𝑃 ∨ ((RSpan‘𝑅)‘{𝑦}) ⊆ 𝑃)) |
| 57 | 8, 9, 20, 55, 56 | syl1111anc 841 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) → (((RSpan‘𝑅)‘{𝑥}) ⊆ 𝑃 ∨ ((RSpan‘𝑅)‘{𝑦}) ⊆ 𝑃)) |
| 58 | 4, 12 | rspsnid 33399 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ((RSpan‘𝑅)‘{𝑥})) |
| 59 | 1, 58 | sylan 580 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ((RSpan‘𝑅)‘{𝑥})) |
| 60 | 59 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ ((RSpan‘𝑅)‘{𝑥})) |
| 61 | | ssel 3977 |
. . . . . . . . . . 11
⊢
(((RSpan‘𝑅)‘{𝑥}) ⊆ 𝑃 → (𝑥 ∈ ((RSpan‘𝑅)‘{𝑥}) → 𝑥 ∈ 𝑃)) |
| 62 | 60, 61 | syl5com 31 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (((RSpan‘𝑅)‘{𝑥}) ⊆ 𝑃 → 𝑥 ∈ 𝑃)) |
| 63 | 4, 12 | rspsnid 33399 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ((RSpan‘𝑅)‘{𝑦})) |
| 64 | 1, 63 | sylan 580 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ((RSpan‘𝑅)‘{𝑦})) |
| 65 | 64 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ((RSpan‘𝑅)‘{𝑦})) |
| 66 | | ssel 3977 |
. . . . . . . . . . 11
⊢
(((RSpan‘𝑅)‘{𝑦}) ⊆ 𝑃 → (𝑦 ∈ ((RSpan‘𝑅)‘{𝑦}) → 𝑦 ∈ 𝑃)) |
| 67 | 65, 66 | syl5com 31 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (((RSpan‘𝑅)‘{𝑦}) ⊆ 𝑃 → 𝑦 ∈ 𝑃)) |
| 68 | 62, 67 | orim12d 967 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → ((((RSpan‘𝑅)‘{𝑥}) ⊆ 𝑃 ∨ ((RSpan‘𝑅)‘{𝑦}) ⊆ 𝑃) → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃))) |
| 69 | 68 | adantllr 719 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → ((((RSpan‘𝑅)‘{𝑥}) ⊆ 𝑃 ∨ ((RSpan‘𝑅)‘{𝑦}) ⊆ 𝑃) → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃))) |
| 70 | 69 | adantr 480 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) → ((((RSpan‘𝑅)‘{𝑥}) ⊆ 𝑃 ∨ ((RSpan‘𝑅)‘{𝑦}) ⊆ 𝑃) → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃))) |
| 71 | 57, 70 | mpd 15 |
. . . . . 6
⊢
(((((𝑅 ∈ CRing
∧ 𝑃 ∈
(PrmIdeal‘𝑅)) ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 · 𝑦) ∈ 𝑃) → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃)) |
| 72 | 71 | ex 412 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → ((𝑥 · 𝑦) ∈ 𝑃 → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃))) |
| 73 | 72 | anasss 466 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑥 · 𝑦) ∈ 𝑃 → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃))) |
| 74 | 73 | ralrimivva 3202 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) ∈ 𝑃 → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃))) |
| 75 | 3, 7, 74 | 3jca 1129 |
. 2
⊢ ((𝑅 ∈ CRing ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) → (𝑃 ∈ (LIdeal‘𝑅) ∧ 𝑃 ≠ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) ∈ 𝑃 → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃)))) |
| 76 | | 3anass 1095 |
. . . 4
⊢ ((𝑃 ∈ (LIdeal‘𝑅) ∧ 𝑃 ≠ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) ∈ 𝑃 → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃))) ↔ (𝑃 ∈ (LIdeal‘𝑅) ∧ (𝑃 ≠ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) ∈ 𝑃 → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃))))) |
| 77 | 4, 5 | prmidl2 33469 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝑃 ∈ (LIdeal‘𝑅)) ∧ (𝑃 ≠ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) ∈ 𝑃 → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃)))) → 𝑃 ∈ (PrmIdeal‘𝑅)) |
| 78 | 77 | anasss 466 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑃 ∈ (LIdeal‘𝑅) ∧ (𝑃 ≠ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) ∈ 𝑃 → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃))))) → 𝑃 ∈ (PrmIdeal‘𝑅)) |
| 79 | 76, 78 | sylan2b 594 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝑃 ∈ (LIdeal‘𝑅) ∧ 𝑃 ≠ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) ∈ 𝑃 → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃)))) → 𝑃 ∈ (PrmIdeal‘𝑅)) |
| 80 | 1, 79 | sylan 580 |
. 2
⊢ ((𝑅 ∈ CRing ∧ (𝑃 ∈ (LIdeal‘𝑅) ∧ 𝑃 ≠ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) ∈ 𝑃 → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃)))) → 𝑃 ∈ (PrmIdeal‘𝑅)) |
| 81 | 75, 80 | impbida 801 |
1
⊢ (𝑅 ∈ CRing → (𝑃 ∈ (PrmIdeal‘𝑅) ↔ (𝑃 ∈ (LIdeal‘𝑅) ∧ 𝑃 ≠ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) ∈ 𝑃 → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃))))) |