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 ˙ = 0 W
lss0cl.s S = LSubSp W
Assertion lssle0 W LMod X S X 0 ˙ X = 0 ˙

Proof

Step Hyp Ref Expression
1 lss0cl.z 0 ˙ = 0 W
2 lss0cl.s S = LSubSp W
3 1 2 lss0ss W LMod X S 0 ˙ X
4 3 biantrud W LMod X S X 0 ˙ X 0 ˙ 0 ˙ X
5 eqss X = 0 ˙ X 0 ˙ 0 ˙ X
6 4 5 bitr4di W LMod X S X 0 ˙ X = 0 ˙