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	⊢ ( 𝜑 → ( 𝑇 ⊕ 𝑈 ) ⊆ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )

Metamath Proof Explorer

Theorem lsmssspx

Proof