Step |
Hyp |
Ref |
Expression |
1 |
|
prmidlval.1 |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
2 |
|
prmidlval.2 |
⊢ · = ( .r ‘ 𝑅 ) |
3 |
|
simpr |
⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃 ≠ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) |
4 |
|
simplrr |
⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃 ≠ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) |
5 |
|
eqid |
⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 ) |
6 |
1 5
|
lidlss |
⊢ ( 𝑏 ∈ ( LIdeal ‘ 𝑅 ) → 𝑏 ⊆ 𝐵 ) |
7 |
4 6
|
syl |
⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃 ≠ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → 𝑏 ⊆ 𝐵 ) |
8 |
|
simplrl |
⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃 ≠ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ) |
9 |
1 5
|
lidlss |
⊢ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) → 𝑎 ⊆ 𝐵 ) |
10 |
8 9
|
syl |
⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃 ≠ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → 𝑎 ⊆ 𝐵 ) |
11 |
|
simpllr |
⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃 ≠ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) |
12 |
|
ssralv |
⊢ ( 𝑎 ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) → ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ) |
13 |
10 11 12
|
sylc |
⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃 ≠ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) |
14 |
|
ssralv |
⊢ ( 𝑏 ⊆ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) → ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ) |
15 |
14
|
ralimdv |
⊢ ( 𝑏 ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) → ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ) |
16 |
7 13 15
|
sylc |
⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃 ≠ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) |
17 |
|
r19.26-2 |
⊢ ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 ∧ ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ) |
18 |
|
pm3.35 |
⊢ ( ( ( 𝑥 · 𝑦 ) ∈ 𝑃 ∧ ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) |
19 |
18
|
2ralimi |
⊢ ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 ∧ ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) → ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) |
20 |
17 19
|
sylbir |
⊢ ( ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) → ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) |
21 |
3 16 20
|
syl2anc |
⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃 ≠ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) |
22 |
|
2ralor |
⊢ ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ↔ ( ∀ 𝑥 ∈ 𝑎 𝑥 ∈ 𝑃 ∨ ∀ 𝑦 ∈ 𝑏 𝑦 ∈ 𝑃 ) ) |
23 |
|
dfss3 |
⊢ ( 𝑎 ⊆ 𝑃 ↔ ∀ 𝑥 ∈ 𝑎 𝑥 ∈ 𝑃 ) |
24 |
|
dfss3 |
⊢ ( 𝑏 ⊆ 𝑃 ↔ ∀ 𝑦 ∈ 𝑏 𝑦 ∈ 𝑃 ) |
25 |
23 24
|
orbi12i |
⊢ ( ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ↔ ( ∀ 𝑥 ∈ 𝑎 𝑥 ∈ 𝑃 ∨ ∀ 𝑦 ∈ 𝑏 𝑦 ∈ 𝑃 ) ) |
26 |
22 25
|
sylbb2 |
⊢ ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) |
27 |
21 26
|
syl |
⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃 ≠ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) |
28 |
27
|
ex |
⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃 ≠ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ∧ ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ) → ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) |
29 |
28
|
ralrimivva |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃 ≠ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) → ∀ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) |
30 |
1 2
|
isprmidl |
⊢ ( 𝑅 ∈ Ring → ( 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ↔ ( 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑃 ≠ 𝐵 ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ) ) |
31 |
30
|
biimpar |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑃 ≠ 𝐵 ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ) → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) |
32 |
31
|
3anassrs |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃 ≠ 𝐵 ) ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) |
33 |
29 32
|
syldan |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑃 ≠ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) |
34 |
33
|
anasss |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑃 ≠ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ) → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) |