Theorem lsppr0

Description: The span of a vector paired with zero equals the span of the singleton of the vector. (Contributed by NM, 29-Aug-2014)

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

Proof

Step	Hyp	Ref	Expression
1		lsppr0.v	$$⊢V={\mathrm{Base}}_W$$
2		lsppr0.z	$$⊢\underset{\dot{}}{0}=0_W$$
3		lsppr0.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
4		lsppr0.w	$$⊢\phi \to W\in \mathrm{LMod}$$
5		lsppr0.x	$$⊢\phi \to X\in V$$
6		eqid	$$⊢\mathrm{LSSum}\left(W\right)=\mathrm{LSSum}\left(W\right)$$
7	1 2	lmod0vcl	$$⊢W\in \mathrm{LMod}\to \underset{\dot{}}{0}\in V$$
8	4 7	syl	$$⊢\phi \to \underset{\dot{}}{0}\in V$$
9	1 3 6 4 5 8	lsmpr	$$⊢\phi \to N\left(\left\{X,\underset{\dot{}}{0}\right\}\right)=N\left(\left\{X\right\}\right)\mathrm{LSSum}\left(W\right)N\left(\left\{\underset{\dot{}}{0}\right\}\right)$$
10	2 3	lspsn0	$$⊢W\in \mathrm{LMod}\to N\left(\left\{\underset{\dot{}}{0}\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$
11	4 10	syl	$$⊢\phi \to N\left(\left\{\underset{\dot{}}{0}\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$
12	11	oveq2d	$$⊢\phi \to N\left(\left\{X\right\}\right)\mathrm{LSSum}\left(W\right)N\left(\left\{\underset{\dot{}}{0}\right\}\right)=N\left(\left\{X\right\}\right)\mathrm{LSSum}\left(W\right)\left\{\underset{\dot{}}{0}\right\}$$
13	1 3	lspsnsubg	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to N\left(\left\{X\right\}\right)\in \mathrm{SubGrp}\left(W\right)$$
14	4 5 13	syl2anc	$$⊢\phi \to N\left(\left\{X\right\}\right)\in \mathrm{SubGrp}\left(W\right)$$
15	2 6	lsm01	$$⊢N\left(\left\{X\right\}\right)\in \mathrm{SubGrp}\left(W\right)\to N\left(\left\{X\right\}\right)\mathrm{LSSum}\left(W\right)\left\{\underset{\dot{}}{0}\right\}=N\left(\left\{X\right\}\right)$$
16	14 15	syl	$$⊢\phi \to N\left(\left\{X\right\}\right)\mathrm{LSSum}\left(W\right)\left\{\underset{\dot{}}{0}\right\}=N\left(\left\{X\right\}\right)$$
17	9 12 16	3eqtrd	$$⊢\phi \to N\left(\left\{X,\underset{\dot{}}{0}\right\}\right)=N\left(\left\{X\right\}\right)$$