Metamath Proof Explorer


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