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 ‘ 𝑅 ) ) → 𝑃 ≠ 𝑋 )