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