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	⊢ 𝐿 = ( LIdeal ‘ 𝑅 )
	lidlabl.i	⊢ 𝐼 = ( 𝑅 ↾s 𝑈 )
Assertion	lidlbas	⊢ ( 𝑈 ∈ 𝐿 → ( Base ‘ 𝐼 ) = 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		lidlabl.l	⊢ 𝐿 = ( LIdeal ‘ 𝑅 )
2		lidlabl.i	⊢ 𝐼 = ( 𝑅 ↾s 𝑈 )
3		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4	2 3	ressbas	⊢ ( 𝑈 ∈ 𝐿 → ( 𝑈 ∩ ( Base ‘ 𝑅 ) ) = ( Base ‘ 𝐼 ) )
5	3 1	lidlss	⊢ ( 𝑈 ∈ 𝐿 → 𝑈 ⊆ ( Base ‘ 𝑅 ) )
6		df-ss	⊢ ( 𝑈 ⊆ ( Base ‘ 𝑅 ) ↔ ( 𝑈 ∩ ( Base ‘ 𝑅 ) ) = 𝑈 )
7	5 6	sylib	⊢ ( 𝑈 ∈ 𝐿 → ( 𝑈 ∩ ( Base ‘ 𝑅 ) ) = 𝑈 )
8	4 7	eqtr3d	⊢ ( 𝑈 ∈ 𝐿 → ( Base ‘ 𝐼 ) = 𝑈 )