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

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	3 1	lidlss	|- ( U e. L -> U C_ ( Base ` R ) )
6		df-ss	|- ( U C_ ( Base ` R ) <-> ( U i^i ( Base ` R ) ) = U )
7	5 6	sylib	|- ( U e. L -> ( U i^i ( Base ` R ) ) = U )
8	4 7	eqtr3d	|- ( U e. L -> ( Base ` I ) = U )