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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
lsmsp2.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lsmsp2.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
lsmssspx.t ⊢ ( 𝜑 → 𝑇 ⊆ 𝑉 )
lsmssspx.u ⊢ ( 𝜑 → 𝑈 ⊆ 𝑉 )
lsmssspx.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
Assertion lsmssspx ( 𝜑 → ( 𝑇 ⊕ 𝑈 ) ⊆ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 lsmsp2.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lsmsp2.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3 lsmsp2.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
4 lsmssspx.t ⊢ ( 𝜑 → 𝑇 ⊆ 𝑉 )
5 lsmssspx.u ⊢ ( 𝜑 → 𝑈 ⊆ 𝑉 )
6 lsmssspx.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
7 1 2 lspssv ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑇 ) ⊆ 𝑉 )
8 6 4 7 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑇 ) ⊆ 𝑉 )
9 1 2 lspssid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ) → 𝑇 ⊆ ( 𝑁 ‘ 𝑇 ) )
10 6 4 9 syl2anc ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑁 ‘ 𝑇 ) )
11 1 3 lsmless1x ⊢ ( ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ 𝑇 ) ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) ∧ 𝑇 ⊆ ( 𝑁 ‘ 𝑇 ) ) → ( 𝑇 ⊕ 𝑈 ) ⊆ ( ( 𝑁 ‘ 𝑇 ) ⊕ 𝑈 ) )
12 6 8 5 10 11 syl31anc ⊢ ( 𝜑 → ( 𝑇 ⊕ 𝑈 ) ⊆ ( ( 𝑁 ‘ 𝑇 ) ⊕ 𝑈 ) )
13 1 2 lspssv ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑈 ) ⊆ 𝑉 )
14 6 5 13 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑈 ) ⊆ 𝑉 )
15 1 2 lspssid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ) → 𝑈 ⊆ ( 𝑁 ‘ 𝑈 ) )
16 6 5 15 syl2anc ⊢ ( 𝜑 → 𝑈 ⊆ ( 𝑁 ‘ 𝑈 ) )
17 1 3 lsmless2x ⊢ ( ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ 𝑇 ) ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝑈 ) ⊆ 𝑉 ) ∧ 𝑈 ⊆ ( 𝑁 ‘ 𝑈 ) ) → ( ( 𝑁 ‘ 𝑇 ) ⊕ 𝑈 ) ⊆ ( ( 𝑁 ‘ 𝑇 ) ⊕ ( 𝑁 ‘ 𝑈 ) ) )
18 6 8 14 16 17 syl31anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑇 ) ⊕ 𝑈 ) ⊆ ( ( 𝑁 ‘ 𝑇 ) ⊕ ( 𝑁 ‘ 𝑈 ) ) )
19 12 18 sstrd ⊢ ( 𝜑 → ( 𝑇 ⊕ 𝑈 ) ⊆ ( ( 𝑁 ‘ 𝑇 ) ⊕ ( 𝑁 ‘ 𝑈 ) ) )
20 1 2 3 lsmsp2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → ( ( 𝑁 ‘ 𝑇 ) ⊕ ( 𝑁 ‘ 𝑈 ) ) = ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )
21 6 4 5 20 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑇 ) ⊕ ( 𝑁 ‘ 𝑈 ) ) = ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )
22 19 21 sseqtrd ⊢ ( 𝜑 → ( 𝑇 ⊕ 𝑈 ) ⊆ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )