Theorem lidlssbas

Description: The base set of the restriction of the ring to a (left) ideal is a subset of the base set of the ring. (Contributed by AV, 17-Feb-2020)

	Ref	Expression
Hypotheses	lidlssbas.l	$$⊢L=\mathrm{LIdeal}\left(R\right)$$
	lidlssbas.i	$$⊢I=R{\upharpoonright }_{𝑠}U$$
Assertion	lidlssbas	$$⊢U\in L\to {\mathrm{Base}}_I\subseteq {\mathrm{Base}}_R$$

Proof

Step	Hyp	Ref	Expression
1		lidlssbas.l	$$⊢L=\mathrm{LIdeal}\left(R\right)$$
2		lidlssbas.i	$$⊢I=R{\upharpoonright }_{𝑠}U$$
3		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
4	2 3	ressbas	$$⊢U\in L\to U\cap {\mathrm{Base}}_R={\mathrm{Base}}_I$$
5		inss2	$$⊢U\cap {\mathrm{Base}}_R\subseteq {\mathrm{Base}}_R$$
6	4 5	eqsstrrdi	$$⊢U\in L\to {\mathrm{Base}}_I\subseteq {\mathrm{Base}}_R$$