Step |
Hyp |
Ref |
Expression |
1 |
|
prmidlval.1 |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
2 |
|
prmidlval.2 |
⊢ · = ( .r ‘ 𝑅 ) |
3 |
|
raleq |
⊢ ( 𝑏 = 𝐽 → ( ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ↔ ∀ 𝑦 ∈ 𝐽 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ) |
4 |
3
|
ralbidv |
⊢ ( 𝑏 = 𝐽 → ( ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ↔ ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐽 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ) |
5 |
|
sseq1 |
⊢ ( 𝑏 = 𝐽 → ( 𝑏 ⊆ 𝑃 ↔ 𝐽 ⊆ 𝑃 ) ) |
6 |
5
|
orbi2d |
⊢ ( 𝑏 = 𝐽 → ( ( 𝐼 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ↔ ( 𝐼 ⊆ 𝑃 ∨ 𝐽 ⊆ 𝑃 ) ) ) |
7 |
4 6
|
imbi12d |
⊢ ( 𝑏 = 𝐽 → ( ( ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝐼 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ↔ ( ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐽 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝐼 ⊆ 𝑃 ∨ 𝐽 ⊆ 𝑃 ) ) ) ) |
8 |
|
raleq |
⊢ ( 𝑎 = 𝐼 → ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ↔ ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ) |
9 |
|
sseq1 |
⊢ ( 𝑎 = 𝐼 → ( 𝑎 ⊆ 𝑃 ↔ 𝐼 ⊆ 𝑃 ) ) |
10 |
9
|
orbi1d |
⊢ ( 𝑎 = 𝐼 → ( ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ↔ ( 𝐼 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) |
11 |
8 10
|
imbi12d |
⊢ ( 𝑎 = 𝐼 → ( ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ↔ ( ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝐼 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ) |
12 |
11
|
ralbidv |
⊢ ( 𝑎 = 𝐼 → ( ∀ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ↔ ∀ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝐼 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ) |
13 |
1 2
|
isprmidl |
⊢ ( 𝑅 ∈ Ring → ( 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ↔ ( 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑃 ≠ 𝐵 ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ) ) |
14 |
13
|
biimpa |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ( 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑃 ≠ 𝐵 ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ) |
15 |
14
|
simp3d |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ∀ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) |
16 |
15
|
adantr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) ) → ∀ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) |
17 |
|
simprl |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) |
18 |
12 16 17
|
rspcdva |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) ) → ∀ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝑏 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝐼 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) |
19 |
|
simprr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) ) → 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) |
20 |
7 18 19
|
rspcdva |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) ) → ( ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐽 ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝐼 ⊆ 𝑃 ∨ 𝐽 ⊆ 𝑃 ) ) ) |
21 |
20
|
imp |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐽 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → ( 𝐼 ⊆ 𝑃 ∨ 𝐽 ⊆ 𝑃 ) ) |