Theorem lsp0

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

	Ref	Expression
Hypotheses	lspsn0.z	$$⊢\underset{\dot{}}{0}=0_W$$
	lspsn0.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
Assertion	lsp0	$$⊢W\in \mathrm{LMod}\to N\left(\varnothing \right)=\left\{\underset{\dot{}}{0}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		lspsn0.z	$$⊢\underset{\dot{}}{0}=0_W$$
2		lspsn0.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
3		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
4	1 3	lsssn0	$$⊢W\in \mathrm{LMod}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LSubSp}\left(W\right)$$
5		0ss	$$⊢\varnothing \subseteq \left\{\underset{\dot{}}{0}\right\}$$
6	3 2	lspssp	$$⊢\left(W\in \mathrm{LMod}\wedge \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LSubSp}\left(W\right)\wedge \varnothing \subseteq \left\{\underset{\dot{}}{0}\right\}\right)\to N\left(\varnothing \right)\subseteq \left\{\underset{\dot{}}{0}\right\}$$
7	5 6	mp3an3	$$⊢\left(W\in \mathrm{LMod}\wedge \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LSubSp}\left(W\right)\right)\to N\left(\varnothing \right)\subseteq \left\{\underset{\dot{}}{0}\right\}$$
8	4 7	mpdan	$$⊢W\in \mathrm{LMod}\to N\left(\varnothing \right)\subseteq \left\{\underset{\dot{}}{0}\right\}$$
9		0ss	$$⊢\varnothing \subseteq {\mathrm{Base}}_W$$
10		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
11	10 3 2	lspcl	$$⊢\left(W\in \mathrm{LMod}\wedge \varnothing \subseteq {\mathrm{Base}}_W\right)\to N\left(\varnothing \right)\in \mathrm{LSubSp}\left(W\right)$$
12	9 11	mpan2	$$⊢W\in \mathrm{LMod}\to N\left(\varnothing \right)\in \mathrm{LSubSp}\left(W\right)$$
13	1 3	lss0ss	$$⊢\left(W\in \mathrm{LMod}\wedge N\left(\varnothing \right)\in \mathrm{LSubSp}\left(W\right)\right)\to \left\{\underset{\dot{}}{0}\right\}\subseteq N\left(\varnothing \right)$$
14	12 13	mpdan	$$⊢W\in \mathrm{LMod}\to \left\{\underset{\dot{}}{0}\right\}\subseteq N\left(\varnothing \right)$$
15	8 14	eqssd	$$⊢W\in \mathrm{LMod}\to N\left(\varnothing \right)=\left\{\underset{\dot{}}{0}\right\}$$