Metamath Proof Explorer

Theorem pridlidl

Description: Obsolete theorem, use prmidlidl instead. A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	pridlidl	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) → 𝑃 ∈ ( Idl ‘ 𝑅 ) )

Proof

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