Theorem prmidl

Description: The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Thierry Arnoux, 12-Jan-2024)

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

Proof

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 ‘ 𝑅 ) ) ) ∧ ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐽 ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → ( 𝐼 ⊆ 𝑃 ∨ 𝐽 ⊆ 𝑃 ) )