Theorem lssle0

Description: No subspace is smaller than the zero subspace. ( shle0 analog.) (Contributed by NM, 20-Apr-2014) (Revised by Mario Carneiro, 19-Jun-2014)

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

Proof

Step	Hyp	Ref	Expression
1		lss0cl.z	⊢ 0 = ( 0g ‘ 𝑊 )
2		lss0cl.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3	1 2	lss0ss	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) → { 0 } ⊆ 𝑋 )
4	3	biantrud	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 ⊆ { 0 } ↔ ( 𝑋 ⊆ { 0 } ∧ { 0 } ⊆ 𝑋 ) ) )
5		eqss	⊢ ( 𝑋 = { 0 } ↔ ( 𝑋 ⊆ { 0 } ∧ { 0 } ⊆ 𝑋 ) )
6	4 5	bitr4di	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 ⊆ { 0 } ↔ 𝑋 = { 0 } ) )