Metamath Proof Explorer


Theorem lsp0

Description: Span of the empty set. (Contributed by Mario Carneiro, 5-Sep-2014)

Ref Expression
Hypotheses lspsn0.z 0 ˙ = 0 W
lspsn0.n N = LSpan W
Assertion lsp0 W LMod N = 0 ˙

Proof

Step Hyp Ref Expression
1 lspsn0.z 0 ˙ = 0 W
2 lspsn0.n N = LSpan W
3 eqid LSubSp W = LSubSp W
4 1 3 lsssn0 W LMod 0 ˙ LSubSp W
5 0ss 0 ˙
6 3 2 lspssp W LMod 0 ˙ LSubSp W 0 ˙ N 0 ˙
7 5 6 mp3an3 W LMod 0 ˙ LSubSp W N 0 ˙
8 4 7 mpdan W LMod N 0 ˙
9 0ss Base W
10 eqid Base W = Base W
11 10 3 2 lspcl W LMod Base W N LSubSp W
12 9 11 mpan2 W LMod N LSubSp W
13 1 3 lss0ss W LMod N LSubSp W 0 ˙ N
14 12 13 mpdan W LMod 0 ˙ N
15 8 14 eqssd W LMod N = 0 ˙