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 ‘ 𝑅 ) ) ∧ 𝐴 ∈ 𝐼 ) → 𝐴 ∈ 𝑋 )