# Metamath Proof Explorer

## Theorem lsmcl

Description: The sum of two subspaces is a subspace. (Contributed by NM, 4-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

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

### Proof

Step Hyp Ref Expression
1 lsmcl.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
2 lsmcl.p
3 lmodabl ${⊢}{W}\in \mathrm{LMod}\to {W}\in \mathrm{Abel}$
4 3 3ad2ant1 ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\to {W}\in \mathrm{Abel}$
5 1 lsssubg ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\right)\to {T}\in \mathrm{SubGrp}\left({W}\right)$
6 5 3adant3 ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\to {T}\in \mathrm{SubGrp}\left({W}\right)$
7 1 lsssubg ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {U}\in \mathrm{SubGrp}\left({W}\right)$
8 7 3adant2 ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\to {U}\in \mathrm{SubGrp}\left({W}\right)$
9 2 lsmsubg2
10 4 6 8 9 syl3anc
11 eqid ${⊢}{+}_{{W}}={+}_{{W}}$
12 11 2 lsmelval
13 6 8 12 syl2anc
15 simpll1 ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({d}\in {T}\wedge {e}\in {U}\right)\right)\to {W}\in \mathrm{LMod}$
16 simplr ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({d}\in {T}\wedge {e}\in {U}\right)\right)\to {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
17 simpll2 ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({d}\in {T}\wedge {e}\in {U}\right)\right)\to {T}\in {S}$
18 simprl ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({d}\in {T}\wedge {e}\in {U}\right)\right)\to {d}\in {T}$
19 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
20 19 1 lssel ${⊢}\left({T}\in {S}\wedge {d}\in {T}\right)\to {d}\in {\mathrm{Base}}_{{W}}$
21 17 18 20 syl2anc ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({d}\in {T}\wedge {e}\in {U}\right)\right)\to {d}\in {\mathrm{Base}}_{{W}}$
22 simpll3 ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({d}\in {T}\wedge {e}\in {U}\right)\right)\to {U}\in {S}$
23 simprr ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({d}\in {T}\wedge {e}\in {U}\right)\right)\to {e}\in {U}$
24 19 1 lssel ${⊢}\left({U}\in {S}\wedge {e}\in {U}\right)\to {e}\in {\mathrm{Base}}_{{W}}$
25 22 23 24 syl2anc ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({d}\in {T}\wedge {e}\in {U}\right)\right)\to {e}\in {\mathrm{Base}}_{{W}}$
26 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
27 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
28 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
29 19 11 26 27 28 lmodvsdi ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {d}\in {\mathrm{Base}}_{{W}}\wedge {e}\in {\mathrm{Base}}_{{W}}\right)\right)\to {a}{\cdot }_{{W}}\left({d}{+}_{{W}}{e}\right)=\left({a}{\cdot }_{{W}}{d}\right){+}_{{W}}\left({a}{\cdot }_{{W}}{e}\right)$
30 15 16 21 25 29 syl13anc ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({d}\in {T}\wedge {e}\in {U}\right)\right)\to {a}{\cdot }_{{W}}\left({d}{+}_{{W}}{e}\right)=\left({a}{\cdot }_{{W}}{d}\right){+}_{{W}}\left({a}{\cdot }_{{W}}{e}\right)$
31 15 17 5 syl2anc ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({d}\in {T}\wedge {e}\in {U}\right)\right)\to {T}\in \mathrm{SubGrp}\left({W}\right)$
32 15 22 7 syl2anc ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({d}\in {T}\wedge {e}\in {U}\right)\right)\to {U}\in \mathrm{SubGrp}\left({W}\right)$
33 26 27 28 1 lssvscl ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\right)\wedge \left({a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {d}\in {T}\right)\right)\to {a}{\cdot }_{{W}}{d}\in {T}$
34 15 17 16 18 33 syl22anc ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({d}\in {T}\wedge {e}\in {U}\right)\right)\to {a}{\cdot }_{{W}}{d}\in {T}$
35 26 27 28 1 lssvscl ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {e}\in {U}\right)\right)\to {a}{\cdot }_{{W}}{e}\in {U}$
36 15 22 16 23 35 syl22anc ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({d}\in {T}\wedge {e}\in {U}\right)\right)\to {a}{\cdot }_{{W}}{e}\in {U}$
37 11 2 lsmelvali
38 31 32 34 36 37 syl22anc
39 30 38 eqeltrd
40 oveq2 ${⊢}{u}={d}{+}_{{W}}{e}\to {a}{\cdot }_{{W}}{u}={a}{\cdot }_{{W}}\left({d}{+}_{{W}}{e}\right)$
41 40 eleq1d
42 39 41 syl5ibrcom
43 42 rexlimdvva
44 14 43 sylbid
45 44 impr
46 45 ralrimivva
47 26 28 19 27 1 islss4