This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prmidl2

Description: A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Thierry Arnoux, 12-Jan-2024)

Ref Expression
Hypotheses prmidlval.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
prmidlval.2 ⊢ · = ( .r ‘ 𝑅 )
Assertion prmidl2 ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑃 ≠ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ) → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) )

Proof

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 ‘ 𝑅 ) )