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	⊢ 𝐿 = ( LIdeal ‘ 𝑅 )
	lidlabl.i	⊢ 𝐼 = ( 𝑅 ↾s 𝑈 )
Assertion	lidlssbas	⊢ ( 𝑈 ∈ 𝐿 → ( Base ‘ 𝐼 ) ⊆ ( 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		inss2	⊢ ( 𝑈 ∩ ( Base ‘ 𝑅 ) ) ⊆ ( Base ‘ 𝑅 )
6	4 5	eqsstrrdi	⊢ ( 𝑈 ∈ 𝐿 → ( Base ‘ 𝐼 ) ⊆ ( Base ‘ 𝑅 ) )