Metamath Proof Explorer

Theorem pridlc

Description: Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011)

Ref Expression
Hypotheses ispridlc.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
ispridlc.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
ispridlc.3 ⊢ 𝑋 = ran 𝐺
Assertion pridlc ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 ) ) → ( 𝐴 ∈ 𝑃 ∨ 𝐵 ∈ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 ispridlc.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 ispridlc.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 ispridlc.3 ⊢ 𝑋 = ran 𝐺
4 1 2 3 ispridlc ⊢ ( 𝑅 ∈ CRingOps → ( 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ↔ ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) ) )
5 4 biimpa ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) → ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) )
6 5 simp3d ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) → ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) )
7 oveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 𝐻 𝑏 ) = ( 𝐴 𝐻 𝑏 ) )
8 7 eleq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ↔ ( 𝐴 𝐻 𝑏 ) ∈ 𝑃 ) )
9 eleq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ∈ 𝑃 ↔ 𝐴 ∈ 𝑃 ) )
10 9 orbi1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ↔ ( 𝐴 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) )
11 8 10 imbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ↔ ( ( 𝐴 𝐻 𝑏 ) ∈ 𝑃 → ( 𝐴 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) )
12 oveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐴 𝐻 𝑏 ) = ( 𝐴 𝐻 𝐵 ) )
13 12 eleq1d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 𝐻 𝑏 ) ∈ 𝑃 ↔ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 ) )
14 eleq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ∈ 𝑃 ↔ 𝐵 ∈ 𝑃 ) )
15 14 orbi2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ↔ ( 𝐴 ∈ 𝑃 ∨ 𝐵 ∈ 𝑃 ) ) )
16 13 15 imbi12d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝐴 𝐻 𝑏 ) ∈ 𝑃 → ( 𝐴 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ↔ ( ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 → ( 𝐴 ∈ 𝑃 ∨ 𝐵 ∈ 𝑃 ) ) ) )
17 11 16 rspc2v ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) → ( ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 → ( 𝐴 ∈ 𝑃 ∨ 𝐵 ∈ 𝑃 ) ) ) )
18 17 com12 ⊢ ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 → ( 𝐴 ∈ 𝑃 ∨ 𝐵 ∈ 𝑃 ) ) ) )
19 18 expd ⊢ ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) → ( 𝐴 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 → ( 𝐴 ∈ 𝑃 ∨ 𝐵 ∈ 𝑃 ) ) ) ) )
20 19 3imp2 ⊢ ( ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 ) ) → ( 𝐴 ∈ 𝑃 ∨ 𝐵 ∈ 𝑃 ) )
21 6 20 sylan ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 ) ) → ( 𝐴 ∈ 𝑃 ∨ 𝐵 ∈ 𝑃 ) )