Theorem lsmsp2

Description: Subspace sum of spans of subsets is the span of their union. ( spanuni analog.) (Contributed by NM, 22-Feb-2014) (Revised by Mario Carneiro, 21-Jun-2014)

	Ref	Expression
Hypotheses	lsmsp2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lsmsp2.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lsmsp2.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
Assertion	lsmsp2	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → ( ( 𝑁 ‘ 𝑇 ) ⊕ ( 𝑁 ‘ 𝑈 ) ) = ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lsmsp2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lsmsp2.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3		lsmsp2.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
4		simp1	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → 𝑊 ∈ LMod )
5		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
6	1 5 2	lspcl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑇 ) ∈ ( LSubSp ‘ 𝑊 ) )
7	6	3adant3	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑇 ) ∈ ( LSubSp ‘ 𝑊 ) )
8	1 5 2	lspcl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑈 ) ∈ ( LSubSp ‘ 𝑊 ) )
9	8	3adant2	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑈 ) ∈ ( LSubSp ‘ 𝑊 ) )
10	5 2 3	lsmsp	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ 𝑇 ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝑁 ‘ 𝑈 ) ∈ ( LSubSp ‘ 𝑊 ) ) → ( ( 𝑁 ‘ 𝑇 ) ⊕ ( 𝑁 ‘ 𝑈 ) ) = ( 𝑁 ‘ ( ( 𝑁 ‘ 𝑇 ) ∪ ( 𝑁 ‘ 𝑈 ) ) ) )
11	4 7 9 10	syl3anc	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → ( ( 𝑁 ‘ 𝑇 ) ⊕ ( 𝑁 ‘ 𝑈 ) ) = ( 𝑁 ‘ ( ( 𝑁 ‘ 𝑇 ) ∪ ( 𝑁 ‘ 𝑈 ) ) ) )
12	1 2	lspun	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) = ( 𝑁 ‘ ( ( 𝑁 ‘ 𝑇 ) ∪ ( 𝑁 ‘ 𝑈 ) ) ) )
13	11 12	eqtr4d	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → ( ( 𝑁 ‘ 𝑇 ) ⊕ ( 𝑁 ‘ 𝑈 ) ) = ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )