Theorem lidlbas

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

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

Proof

Step	Hyp	Ref	Expression
1		lidlabl.l	$$⊢L=\mathrm{LIdeal}\left(R\right)$$
2		lidlabl.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	3 1	lidlss	$$⊢U\in L\to U\subseteq {\mathrm{Base}}_R$$
6		df-ss	$$⊢U\subseteq {\mathrm{Base}}_R\leftrightarrow U\cap {\mathrm{Base}}_R=U$$
7	5 6	sylib	$$⊢U\in L\to U\cap {\mathrm{Base}}_R=U$$
8	4 7	eqtr3d	$$⊢U\in L\to {\mathrm{Base}}_I=U$$