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

Metamath Proof Explorer

Theorem prmidlc

Description: Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011) (Revised by Thierry Arnoux, 12-Jan-2024)

Ref Expression
Hypotheses isprmidlc.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
isprmidlc.2 ⊢ · = ( .r ‘ 𝑅 )
Assertion prmidlc ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ 𝐵 ∧ 𝐽 ∈ 𝐵 ∧ ( 𝐼 · 𝐽 ) ∈ 𝑃 ) ) → ( 𝐼 ∈ 𝑃 ∨ 𝐽 ∈ 𝑃 ) )

Proof

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