Metamath Proof Explorer


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 } ) )