# Metamath Proof Explorer

## Theorem lsmsp

Description: Subspace sum in terms of span. (Contributed by NM, 6-Feb-2014) (Proof shortened by Mario Carneiro, 21-Jun-2014)

Ref Expression
Hypotheses lsmsp.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
lsmsp.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
lsmsp.p
Assertion lsmsp

### Proof

Step Hyp Ref Expression
1 lsmsp.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
2 lsmsp.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
3 lsmsp.p
4 simp1 ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\to {W}\in \mathrm{LMod}$
5 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
6 5 1 lssss ${⊢}{T}\in {S}\to {T}\subseteq {\mathrm{Base}}_{{W}}$
7 6 3ad2ant2 ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\to {T}\subseteq {\mathrm{Base}}_{{W}}$
8 5 1 lssss ${⊢}{U}\in {S}\to {U}\subseteq {\mathrm{Base}}_{{W}}$
9 8 3ad2ant3 ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\to {U}\subseteq {\mathrm{Base}}_{{W}}$
10 7 9 unssd ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\to {T}\cup {U}\subseteq {\mathrm{Base}}_{{W}}$
11 5 2 lspssid ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\cup {U}\subseteq {\mathrm{Base}}_{{W}}\right)\to {T}\cup {U}\subseteq {N}\left({T}\cup {U}\right)$
12 4 10 11 syl2anc ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\to {T}\cup {U}\subseteq {N}\left({T}\cup {U}\right)$
13 12 unssad ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\to {T}\subseteq {N}\left({T}\cup {U}\right)$
14 12 unssbd ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\to {U}\subseteq {N}\left({T}\cup {U}\right)$
15 1 lsssssubg ${⊢}{W}\in \mathrm{LMod}\to {S}\subseteq \mathrm{SubGrp}\left({W}\right)$
16 15 3ad2ant1 ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\to {S}\subseteq \mathrm{SubGrp}\left({W}\right)$
17 simp2 ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\to {T}\in {S}$
18 16 17 sseldd ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\to {T}\in \mathrm{SubGrp}\left({W}\right)$
19 simp3 ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\to {U}\in {S}$
20 16 19 sseldd ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\to {U}\in \mathrm{SubGrp}\left({W}\right)$
21 5 1 2 lspcl ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\cup {U}\subseteq {\mathrm{Base}}_{{W}}\right)\to {N}\left({T}\cup {U}\right)\in {S}$
22 4 10 21 syl2anc ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\to {N}\left({T}\cup {U}\right)\in {S}$
23 16 22 sseldd ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\to {N}\left({T}\cup {U}\right)\in \mathrm{SubGrp}\left({W}\right)$
24 3 lsmlub
25 18 20 23 24 syl3anc
26 13 14 25 mpbi2and
27 1 3 lsmcl
28 3 lsmunss
29 18 20 28 syl2anc
30 1 2 lspssp
31 4 27 29 30 syl3anc
32 26 31 eqssd