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	$$⊢G=1^{st}\left(R\right)$$
	idlss.2	$$⊢X=\mathrm{ran}G$$
Assertion	idlcl	$$⊢\left(\left(R\in \mathrm{RingOps}\wedge I\in \mathrm{Idl}\left(R\right)\right)\wedge A\in I\right)\to A\in X$$

Proof

Step	Hyp	Ref	Expression
1		idlss.1	$$⊢G=1^{st}\left(R\right)$$
2		idlss.2	$$⊢X=\mathrm{ran}G$$
3	1 2	idlss	$$⊢\left(R\in \mathrm{RingOps}\wedge I\in \mathrm{Idl}\left(R\right)\right)\to I\subseteq X$$
4	3	sselda	$$⊢\left(\left(R\in \mathrm{RingOps}\wedge I\in \mathrm{Idl}\left(R\right)\right)\wedge A\in I\right)\to A\in X$$