Theorem lss0ss

Description: The zero subspace is included in every subspace. ( sh0le analog.) (Contributed by NM, 27-Mar-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lss0cl.z	⊢ 0 = ( 0g ‘ 𝑊 )
	lss0cl.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion	lss0ss	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) → { 0 } ⊆ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		lss0cl.z	⊢ 0 = ( 0g ‘ 𝑊 )
2		lss0cl.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3	1 2	lss0cl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) → 0 ∈ 𝑋 )
4	3	snssd	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) → { 0 } ⊆ 𝑋 )