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

Metamath Proof Explorer

Theorem pridlnr

Description: A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Hypotheses pridlnr.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
prdilnr.2 ⊢ 𝑋 = ran 𝐺
Assertion pridlnr ( ( 𝑅 ∈ RingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) → 𝑃 ≠ 𝑋 )

Proof

Step Hyp Ref Expression
1 pridlnr.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 prdilnr.2 ⊢ 𝑋 = ran 𝐺
3 eqid ⊢ ( 2nd ‘ 𝑅 ) = ( 2nd ‘ 𝑅 )
4 1 3 2 ispridl ⊢ ( 𝑅 ∈ RingOps → ( 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ↔ ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ) )
5 3anan12 ⊢ ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ↔ ( 𝑃 ≠ 𝑋 ∧ ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ) )
6 4 5 bitrdi ⊢ ( 𝑅 ∈ RingOps → ( 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ↔ ( 𝑃 ≠ 𝑋 ∧ ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ) ) )
7 6 simprbda ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) → 𝑃 ≠ 𝑋 )