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)

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

Metamath Proof Explorer