# Metamath Proof Explorer

Description: The span of a vector sum is included in the span of its arguments. (Contributed by NM, 22-Feb-2014) (Proof shortened by Mario Carneiro, 21-Jun-2014)

Ref Expression
Hypotheses lspvadd.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
lspvadd.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$

### Proof

Step Hyp Ref Expression
1 lspvadd.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
3 lspvadd.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
4 eqid ${⊢}\mathrm{LSubSp}\left({W}\right)=\mathrm{LSubSp}\left({W}\right)$
5 simp1 ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {V}\wedge {Y}\in {V}\right)\to {W}\in \mathrm{LMod}$
6 prssi ${⊢}\left({X}\in {V}\wedge {Y}\in {V}\right)\to \left\{{X},{Y}\right\}\subseteq {V}$
7 6 3adant1 ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {V}\wedge {Y}\in {V}\right)\to \left\{{X},{Y}\right\}\subseteq {V}$
8 1 4 3 lspcl ${⊢}\left({W}\in \mathrm{LMod}\wedge \left\{{X},{Y}\right\}\subseteq {V}\right)\to {N}\left(\left\{{X},{Y}\right\}\right)\in \mathrm{LSubSp}\left({W}\right)$
9 5 7 8 syl2anc ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {V}\wedge {Y}\in {V}\right)\to {N}\left(\left\{{X},{Y}\right\}\right)\in \mathrm{LSubSp}\left({W}\right)$
10 1 3 lspssid ${⊢}\left({W}\in \mathrm{LMod}\wedge \left\{{X},{Y}\right\}\subseteq {V}\right)\to \left\{{X},{Y}\right\}\subseteq {N}\left(\left\{{X},{Y}\right\}\right)$
11 5 7 10 syl2anc ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {V}\wedge {Y}\in {V}\right)\to \left\{{X},{Y}\right\}\subseteq {N}\left(\left\{{X},{Y}\right\}\right)$
12 prssg ${⊢}\left({X}\in {V}\wedge {Y}\in {V}\right)\to \left(\left({X}\in {N}\left(\left\{{X},{Y}\right\}\right)\wedge {Y}\in {N}\left(\left\{{X},{Y}\right\}\right)\right)↔\left\{{X},{Y}\right\}\subseteq {N}\left(\left\{{X},{Y}\right\}\right)\right)$
13 12 3adant1 ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {V}\wedge {Y}\in {V}\right)\to \left(\left({X}\in {N}\left(\left\{{X},{Y}\right\}\right)\wedge {Y}\in {N}\left(\left\{{X},{Y}\right\}\right)\right)↔\left\{{X},{Y}\right\}\subseteq {N}\left(\left\{{X},{Y}\right\}\right)\right)$
14 11 13 mpbird ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {V}\wedge {Y}\in {V}\right)\to \left({X}\in {N}\left(\left\{{X},{Y}\right\}\right)\wedge {Y}\in {N}\left(\left\{{X},{Y}\right\}\right)\right)$
15 2 4 lssvacl
16 5 9 14 15 syl21anc
17 4 3 5 9 16 lspsnel5a