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	lidlabl.l	|- L = ( LIdeal ` R )
	lidlabl.i	|- I = ( R |`s U )
Assertion	lidlssbas	|- ( U e. L -> ( Base ` I ) C_ ( Base ` R ) )

Proof

Step	Hyp	Ref	Expression
1		lidlabl.l	|- L = ( LIdeal ` R )
2		lidlabl.i	|- I = ( R |`s U )
3		eqid	|- ( Base ` R ) = ( Base ` R )
4	2 3	ressbas	|- ( U e. L -> ( U i^i ( Base ` R ) ) = ( Base ` I ) )
5		inss2	|- ( U i^i ( Base ` R ) ) C_ ( Base ` R )
6	4 5	eqsstrrdi	|- ( U e. L -> ( Base ` I ) C_ ( Base ` R ) )