Theorem 0ellsp

Description: Zero is in all spans. (Contributed by Thierry Arnoux, 8-May-2023)

	Ref	Expression
Hypotheses	0ellsp.1	$$⊢\underset{\dot{}}{0}=0_W$$
	0ellsp.b	$$⊢B={\mathrm{Base}}_W$$
	0ellsp.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
Assertion	0ellsp	$$⊢\left(W\in \mathrm{LMod}\wedge S\subseteq B\right)\to \underset{\dot{}}{0}\in N\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		0ellsp.1	$$⊢\underset{\dot{}}{0}=0_W$$
2		0ellsp.b	$$⊢B={\mathrm{Base}}_W$$
3		0ellsp.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
4		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
5	2 4 3	lspcl	$$⊢\left(W\in \mathrm{LMod}\wedge S\subseteq B\right)\to N\left(S\right)\in \mathrm{LSubSp}\left(W\right)$$
6	1 4	lss0cl	$$⊢\left(W\in \mathrm{LMod}\wedge N\left(S\right)\in \mathrm{LSubSp}\left(W\right)\right)\to \underset{\dot{}}{0}\in N\left(S\right)$$
7	5 6	syldan	$$⊢\left(W\in \mathrm{LMod}\wedge S\subseteq B\right)\to \underset{\dot{}}{0}\in N\left(S\right)$$