Metamath Proof Explorer

Theorem lsmssspx

Description: Subspace sum (in its extended domain) is a subset of the span of the union of its arguments. (Contributed by NM, 6-Aug-2014)

Ref Expression
Hypotheses lsmsp2.v ⊢ V = Base W
lsmsp2.n ⊢ N = LSpan ⁡ W
lsmsp2.p ⊢ ⊕ ˙ = LSSum ⁡ W
lsmssspx.t ⊢ φ → T ⊆ V
lsmssspx.u ⊢ φ → U ⊆ V
lsmssspx.w ⊢ φ → W ∈ LMod
Assertion lsmssspx ⊢ φ → T ⊕ ˙ U ⊆ N ⁡ T ∪ U

Proof

Step Hyp Ref Expression
1 lsmsp2.v ⊢ V = Base W
2 lsmsp2.n ⊢ N = LSpan ⁡ W
3 lsmsp2.p ⊢ ⊕ ˙ = LSSum ⁡ W
4 lsmssspx.t ⊢ φ → T ⊆ V
5 lsmssspx.u ⊢ φ → U ⊆ V
6 lsmssspx.w ⊢ φ → W ∈ LMod
7 1 2 lspssv ⊢ W ∈ LMod ∧ T ⊆ V → N ⁡ T ⊆ V
8 6 4 7 syl2anc ⊢ φ → N ⁡ T ⊆ V
9 1 2 lspssid ⊢ W ∈ LMod ∧ T ⊆ V → T ⊆ N ⁡ T
10 6 4 9 syl2anc ⊢ φ → T ⊆ N ⁡ T
11 1 3 lsmless1x ⊢ W ∈ LMod ∧ N ⁡ T ⊆ V ∧ U ⊆ V ∧ T ⊆ N ⁡ T → T ⊕ ˙ U ⊆ N ⁡ T ⊕ ˙ U
12 6 8 5 10 11 syl31anc ⊢ φ → T ⊕ ˙ U ⊆ N ⁡ T ⊕ ˙ U
13 1 2 lspssv ⊢ W ∈ LMod ∧ U ⊆ V → N ⁡ U ⊆ V
14 6 5 13 syl2anc ⊢ φ → N ⁡ U ⊆ V
15 1 2 lspssid ⊢ W ∈ LMod ∧ U ⊆ V → U ⊆ N ⁡ U
16 6 5 15 syl2anc ⊢ φ → U ⊆ N ⁡ U
17 1 3 lsmless2x ⊢ W ∈ LMod ∧ N ⁡ T ⊆ V ∧ N ⁡ U ⊆ V ∧ U ⊆ N ⁡ U → N ⁡ T ⊕ ˙ U ⊆ N ⁡ T ⊕ ˙ N ⁡ U
18 6 8 14 16 17 syl31anc ⊢ φ → N ⁡ T ⊕ ˙ U ⊆ N ⁡ T ⊕ ˙ N ⁡ U
19 12 18 sstrd ⊢ φ → T ⊕ ˙ U ⊆ N ⁡ T ⊕ ˙ N ⁡ U
20 1 2 3 lsmsp2 ⊢ W ∈ LMod ∧ T ⊆ V ∧ U ⊆ V → N ⁡ T ⊕ ˙ N ⁡ U = N ⁡ T ∪ U
21 6 4 5 20 syl3anc ⊢ φ → N ⁡ T ⊕ ˙ N ⁡ U = N ⁡ T ∪ U
22 19 21 sseqtrd ⊢ φ → T ⊕ ˙ U ⊆ N ⁡ T ∪ U