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

Metamath Proof Explorer

Theorem pridlc2

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 pridlc2 ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 ) ) → 𝐵 ∈ 𝑃 )

Proof

Step Hyp Ref Expression
1 ispridlc.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 ispridlc.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 ispridlc.3 ⊢ 𝑋 = ran 𝐺
4 eldifn ⊢ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) → ¬ 𝐴 ∈ 𝑃 )
5 4 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 ) → ¬ 𝐴 ∈ 𝑃 )
6 5 adantl ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 ) ) → ¬ 𝐴 ∈ 𝑃 )
7 eldifi ⊢ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) → 𝐴 ∈ 𝑋 )
8 1 2 3 pridlc ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 ) ) → ( 𝐴 ∈ 𝑃 ∨ 𝐵 ∈ 𝑃 ) )
9 8 ord ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 ) ) → ( ¬ 𝐴 ∈ 𝑃 → 𝐵 ∈ 𝑃 ) )
10 7 9 syl3anr1 ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 ) ) → ( ¬ 𝐴 ∈ 𝑃 → 𝐵 ∈ 𝑃 ) )
11 6 10 mpd ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ 𝑃 ) ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐵 ) ∈ 𝑃 ) ) → 𝐵 ∈ 𝑃 )