Step |
Hyp |
Ref |
Expression |
1 |
|
isprmidlc.1 |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
2 |
|
isprmidlc.2 |
⊢ · = ( .r ‘ 𝑅 ) |
3 |
|
simpr1 |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ 𝐵 ∧ 𝐽 ∈ 𝐵 ∧ ( 𝐼 · 𝐽 ) ∈ 𝑃 ) ) → 𝐼 ∈ 𝐵 ) |
4 |
|
simpr2 |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ 𝐵 ∧ 𝐽 ∈ 𝐵 ∧ ( 𝐼 · 𝐽 ) ∈ 𝑃 ) ) → 𝐽 ∈ 𝐵 ) |
5 |
1 2
|
isprmidlc |
⊢ ( 𝑅 ∈ CRing → ( 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ↔ ( 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑃 ≠ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) ) ) |
6 |
5
|
biimpa |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ( 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑃 ≠ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) ) |
7 |
6
|
simp3d |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) |
8 |
7
|
adantr |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ 𝐵 ∧ 𝐽 ∈ 𝐵 ∧ ( 𝐼 · 𝐽 ) ∈ 𝑃 ) ) → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) |
9 |
|
simpr3 |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ 𝐵 ∧ 𝐽 ∈ 𝐵 ∧ ( 𝐼 · 𝐽 ) ∈ 𝑃 ) ) → ( 𝐼 · 𝐽 ) ∈ 𝑃 ) |
10 |
|
oveq12 |
⊢ ( ( 𝑎 = 𝐼 ∧ 𝑏 = 𝐽 ) → ( 𝑎 · 𝑏 ) = ( 𝐼 · 𝐽 ) ) |
11 |
10
|
eleq1d |
⊢ ( ( 𝑎 = 𝐼 ∧ 𝑏 = 𝐽 ) → ( ( 𝑎 · 𝑏 ) ∈ 𝑃 ↔ ( 𝐼 · 𝐽 ) ∈ 𝑃 ) ) |
12 |
|
simpl |
⊢ ( ( 𝑎 = 𝐼 ∧ 𝑏 = 𝐽 ) → 𝑎 = 𝐼 ) |
13 |
12
|
eleq1d |
⊢ ( ( 𝑎 = 𝐼 ∧ 𝑏 = 𝐽 ) → ( 𝑎 ∈ 𝑃 ↔ 𝐼 ∈ 𝑃 ) ) |
14 |
|
simpr |
⊢ ( ( 𝑎 = 𝐼 ∧ 𝑏 = 𝐽 ) → 𝑏 = 𝐽 ) |
15 |
14
|
eleq1d |
⊢ ( ( 𝑎 = 𝐼 ∧ 𝑏 = 𝐽 ) → ( 𝑏 ∈ 𝑃 ↔ 𝐽 ∈ 𝑃 ) ) |
16 |
13 15
|
orbi12d |
⊢ ( ( 𝑎 = 𝐼 ∧ 𝑏 = 𝐽 ) → ( ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ↔ ( 𝐼 ∈ 𝑃 ∨ 𝐽 ∈ 𝑃 ) ) ) |
17 |
11 16
|
imbi12d |
⊢ ( ( 𝑎 = 𝐼 ∧ 𝑏 = 𝐽 ) → ( ( ( 𝑎 · 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ↔ ( ( 𝐼 · 𝐽 ) ∈ 𝑃 → ( 𝐼 ∈ 𝑃 ∨ 𝐽 ∈ 𝑃 ) ) ) ) |
18 |
17
|
rspc2gv |
⊢ ( ( 𝐼 ∈ 𝐵 ∧ 𝐽 ∈ 𝐵 ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) → ( ( 𝐼 · 𝐽 ) ∈ 𝑃 → ( 𝐼 ∈ 𝑃 ∨ 𝐽 ∈ 𝑃 ) ) ) ) |
19 |
18
|
imp31 |
⊢ ( ( ( ( 𝐼 ∈ 𝐵 ∧ 𝐽 ∈ 𝐵 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) ∧ ( 𝐼 · 𝐽 ) ∈ 𝑃 ) → ( 𝐼 ∈ 𝑃 ∨ 𝐽 ∈ 𝑃 ) ) |
20 |
3 4 8 9 19
|
syl1111anc |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ 𝐵 ∧ 𝐽 ∈ 𝐵 ∧ ( 𝐼 · 𝐽 ) ∈ 𝑃 ) ) → ( 𝐼 ∈ 𝑃 ∨ 𝐽 ∈ 𝑃 ) ) |