Metamath Proof Explorer


Theorem shle0

Description: No subspace is smaller than the zero subspace. (Contributed by NM, 24-Nov-2004) (New usage is discouraged.)

Ref Expression
Assertion shle0 A S A 0 A = 0

Proof

Step Hyp Ref Expression
1 sh0le A S 0 A
2 1 biantrud A S A 0 A 0 0 A
3 eqss A = 0 A 0 0 A
4 2 3 bitr4di A S A 0 A = 0