Theorem lidlss

Description: An ideal is a subset of the base set. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	lidlss.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	lidlss.i	⊢ 𝐼 = ( LIdeal ‘ 𝑊 )
Assertion	lidlss	⊢ ( 𝑈 ∈ 𝐼 → 𝑈 ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		lidlss.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		lidlss.i	⊢ 𝐼 = ( LIdeal ‘ 𝑊 )
3		rlmbas	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ ( ringLMod ‘ 𝑊 ) )
4	1 3	eqtri	⊢ 𝐵 = ( Base ‘ ( ringLMod ‘ 𝑊 ) )
5		lidlval	⊢ ( LIdeal ‘ 𝑊 ) = ( LSubSp ‘ ( ringLMod ‘ 𝑊 ) )
6	2 5	eqtri	⊢ 𝐼 = ( LSubSp ‘ ( ringLMod ‘ 𝑊 ) )
7	4 6	lssss	⊢ ( 𝑈 ∈ 𝐼 → 𝑈 ⊆ 𝐵 )