Theorem lspun0

Description: The span of a union with the zero subspace. (Contributed by NM, 22-May-2015)

	Ref	Expression
Hypotheses	lspun0.v	$$⊢V={\mathrm{Base}}_W$$
	lspun0.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lspun0.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lspun0.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lspun0.x	$$⊢\phi \to X\subseteq V$$
Assertion	lspun0	$$⊢\phi \to N\left(X\cup \left\{\underset{\dot{}}{0}\right\}\right)=N\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		lspun0.v	$$⊢V={\mathrm{Base}}_W$$
2		lspun0.o	$$⊢\underset{\dot{}}{0}=0_W$$
3		lspun0.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
4		lspun0.w	$$⊢\phi \to W\in \mathrm{LMod}$$
5		lspun0.x	$$⊢\phi \to X\subseteq V$$
6	1 2	lmod0vcl	$$⊢W\in \mathrm{LMod}\to \underset{\dot{}}{0}\in V$$
7	4 6	syl	$$⊢\phi \to \underset{\dot{}}{0}\in V$$
8	7	snssd	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\subseteq V$$
9	1 3	lspun	$$⊢\left(W\in \mathrm{LMod}\wedge X\subseteq V\wedge \left\{\underset{\dot{}}{0}\right\}\subseteq V\right)\to N\left(X\cup \left\{\underset{\dot{}}{0}\right\}\right)=N\left(N\left(X\right)\cup N\left(\left\{\underset{\dot{}}{0}\right\}\right)\right)$$
10	4 5 8 9	syl3anc	$$⊢\phi \to N\left(X\cup \left\{\underset{\dot{}}{0}\right\}\right)=N\left(N\left(X\right)\cup N\left(\left\{\underset{\dot{}}{0}\right\}\right)\right)$$
11	2 3	lspsn0	$$⊢W\in \mathrm{LMod}\to N\left(\left\{\underset{\dot{}}{0}\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$
12	4 11	syl	$$⊢\phi \to N\left(\left\{\underset{\dot{}}{0}\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$
13	12	uneq2d	$$⊢\phi \to N\left(X\right)\cup N\left(\left\{\underset{\dot{}}{0}\right\}\right)=N\left(X\right)\cup \left\{\underset{\dot{}}{0}\right\}$$
14		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
15	1 14 3	lspcl	$$⊢\left(W\in \mathrm{LMod}\wedge X\subseteq V\right)\to N\left(X\right)\in \mathrm{LSubSp}\left(W\right)$$
16	4 5 15	syl2anc	$$⊢\phi \to N\left(X\right)\in \mathrm{LSubSp}\left(W\right)$$
17	2 14	lss0ss	$$⊢\left(W\in \mathrm{LMod}\wedge N\left(X\right)\in \mathrm{LSubSp}\left(W\right)\right)\to \left\{\underset{\dot{}}{0}\right\}\subseteq N\left(X\right)$$
18	4 16 17	syl2anc	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\subseteq N\left(X\right)$$
19		ssequn2	$$⊢\left\{\underset{\dot{}}{0}\right\}\subseteq N\left(X\right)\leftrightarrow N\left(X\right)\cup \left\{\underset{\dot{}}{0}\right\}=N\left(X\right)$$
20	18 19	sylib	$$⊢\phi \to N\left(X\right)\cup \left\{\underset{\dot{}}{0}\right\}=N\left(X\right)$$
21	13 20	eqtrd	$$⊢\phi \to N\left(X\right)\cup N\left(\left\{\underset{\dot{}}{0}\right\}\right)=N\left(X\right)$$
22	21	fveq2d	$$⊢\phi \to N\left(N\left(X\right)\cup N\left(\left\{\underset{\dot{}}{0}\right\}\right)\right)=N\left(N\left(X\right)\right)$$
23	1 3	lspidm	$$⊢\left(W\in \mathrm{LMod}\wedge X\subseteq V\right)\to N\left(N\left(X\right)\right)=N\left(X\right)$$
24	4 5 23	syl2anc	$$⊢\phi \to N\left(N\left(X\right)\right)=N\left(X\right)$$
25	22 24	eqtrd	$$⊢\phi \to N\left(N\left(X\right)\cup N\left(\left\{\underset{\dot{}}{0}\right\}\right)\right)=N\left(X\right)$$
26	10 25	eqtrd	$$⊢\phi \to N\left(X\cup \left\{\underset{\dot{}}{0}\right\}\right)=N\left(X\right)$$