Description: The zero subspace is the smallest subspace. (Contributed by NM, 3-Jun-2004) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | sh0le | ⊢ ( 𝐴 ∈ Sℋ → 0ℋ ⊆ 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ch0 | ⊢ 0ℋ = { 0ℎ } | |
2 | sh0 | ⊢ ( 𝐴 ∈ Sℋ → 0ℎ ∈ 𝐴 ) | |
3 | 2 | snssd | ⊢ ( 𝐴 ∈ Sℋ → { 0ℎ } ⊆ 𝐴 ) |
4 | 1 3 | eqsstrid | ⊢ ( 𝐴 ∈ Sℋ → 0ℋ ⊆ 𝐴 ) |