Description: The span of the empty set is the zero subspace. Remark 11.6.e of Schechter p. 276. (Contributed by NM, 3-Jun-2004) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | span0 | |- ( span ` (/) ) = 0H |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | h0elsh | |- 0H e. SH |
|
| 2 | 1 | shssii | |- 0H C_ ~H |
| 3 | 0ss | |- (/) C_ 0H |
|
| 4 | spanss | |- ( ( 0H C_ ~H /\ (/) C_ 0H ) -> ( span ` (/) ) C_ ( span ` 0H ) ) |
|
| 5 | 2 3 4 | mp2an | |- ( span ` (/) ) C_ ( span ` 0H ) |
| 6 | spanid | |- ( 0H e. SH -> ( span ` 0H ) = 0H ) |
|
| 7 | 1 6 | ax-mp | |- ( span ` 0H ) = 0H |
| 8 | 5 7 | sseqtri | |- ( span ` (/) ) C_ 0H |
| 9 | 0ss | |- (/) C_ ~H |
|
| 10 | spancl | |- ( (/) C_ ~H -> ( span ` (/) ) e. SH ) |
|
| 11 | 9 10 | ax-mp | |- ( span ` (/) ) e. SH |
| 12 | sh0le | |- ( ( span ` (/) ) e. SH -> 0H C_ ( span ` (/) ) ) |
|
| 13 | 11 12 | ax-mp | |- 0H C_ ( span ` (/) ) |
| 14 | 8 13 | eqssi | |- ( span ` (/) ) = 0H |