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

Metamath Proof Explorer

Theorem idlcl

Description: An element of an ideal is an element of the ring. (Contributed by Jeff Madsen, 19-Jun-2010)

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

Proof

Step Hyp Ref Expression
1 idlss.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 idlss.2 ⊢ 𝑋 = ran 𝐺
3 1 2 idlss ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → 𝐼 ⊆ 𝑋 )
4 3 sselda ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝐴 ∈ 𝐼 ) → 𝐴 ∈ 𝑋 )