Description: The zero subspace is included in every subspace. ( sh0le analog.) (Contributed by NM, 27-Mar-2014) (Revised by Mario Carneiro, 19-Jun-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | lss0cl.z | |- .0. = ( 0g ` W ) |
|
| lss0cl.s | |- S = ( LSubSp ` W ) |
||
| Assertion | lss0ss | |- ( ( W e. LMod /\ X e. S ) -> { .0. } C_ X ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lss0cl.z | |- .0. = ( 0g ` W ) |
|
| 2 | lss0cl.s | |- S = ( LSubSp ` W ) |
|
| 3 | 1 2 | lss0cl | |- ( ( W e. LMod /\ X e. S ) -> .0. e. X ) |
| 4 | 3 | snssd | |- ( ( W e. LMod /\ X e. S ) -> { .0. } C_ X ) |