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

Metamath Proof Explorer

Theorem idlss

Description: An ideal of R is a subset of R . (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses idlss.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
idlss.2 ⊢ 𝑋 = ran 𝐺
Assertion idlss ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → 𝐼 ⊆ 𝑋 )

Proof

Step Hyp Ref Expression
1 idlss.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 idlss.2 ⊢ 𝑋 = ran 𝐺
3 eqid ⊢ ( 2nd ‘ 𝑅 ) = ( 2nd ‘ 𝑅 )
4 eqid ⊢ ( GId ‘ 𝐺 ) = ( GId ‘ 𝐺 )
5 1 3 2 4 isidl ⊢ ( 𝑅 ∈ RingOps → ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ↔ ( 𝐼 ⊆ 𝑋 ∧ ( GId ‘ 𝐺 ) ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ 𝐼 ) ) ) ) )
6 5 biimpa ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝐼 ⊆ 𝑋 ∧ ( GId ‘ 𝐺 ) ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ 𝐼 ) ) ) )
7 6 simp1d ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → 𝐼 ⊆ 𝑋 )