Metamath Proof Explorer

Theorem lsmsp

Description: Subspace sum in terms of span. (Contributed by NM, 6-Feb-2014) (Proof shortened by Mario Carneiro, 21-Jun-2014)

Ref Expression
Hypotheses lsmsp.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lsmsp.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lsmsp.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
Assertion lsmsp ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑇 ⊕ 𝑈 ) = ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 lsmsp.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2 lsmsp.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3 lsmsp.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
4 simp1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → 𝑊 ∈ LMod )
5 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
6 5 1 lssss ⊢ ( 𝑇 ∈ 𝑆 → 𝑇 ⊆ ( Base ‘ 𝑊 ) )
7 6 3ad2ant2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → 𝑇 ⊆ ( Base ‘ 𝑊 ) )
8 5 1 lssss ⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
9 8 3ad2ant3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
10 7 9 unssd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑇 ∪ 𝑈 ) ⊆ ( Base ‘ 𝑊 ) )
11 5 2 lspssid ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑇 ∪ 𝑈 ) ⊆ ( Base ‘ 𝑊 ) ) → ( 𝑇 ∪ 𝑈 ) ⊆ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )
12 4 10 11 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑇 ∪ 𝑈 ) ⊆ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )
13 12 unssad ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → 𝑇 ⊆ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )
14 12 unssbd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ⊆ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )
15 1 lsssssubg ⊢ ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
16 15 3ad2ant1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
17 simp2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → 𝑇 ∈ 𝑆 )
18 16 17 sseldd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
19 simp3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ∈ 𝑆 )
20 16 19 sseldd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
21 5 1 2 lspcl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑇 ∪ 𝑈 ) ⊆ ( Base ‘ 𝑊 ) ) → ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ∈ 𝑆 )
22 4 10 21 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ∈ 𝑆 )
23 16 22 sseldd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ∈ ( SubGrp ‘ 𝑊 ) )
24 3 lsmlub ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ∈ ( SubGrp ‘ 𝑊 ) ) → ( ( 𝑇 ⊆ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ∧ 𝑈 ⊆ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ) ↔ ( 𝑇 ⊕ 𝑈 ) ⊆ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ) )
25 18 20 23 24 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( ( 𝑇 ⊆ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ∧ 𝑈 ⊆ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ) ↔ ( 𝑇 ⊕ 𝑈 ) ⊆ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ) )
26 13 14 25 mpbi2and ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑇 ⊕ 𝑈 ) ⊆ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )
27 1 3 lsmcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑇 ⊕ 𝑈 ) ∈ 𝑆 )
28 3 lsmunss ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑇 ∪ 𝑈 ) ⊆ ( 𝑇 ⊕ 𝑈 ) )
29 18 20 28 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑇 ∪ 𝑈 ) ⊆ ( 𝑇 ⊕ 𝑈 ) )
30 1 2 lspssp ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑇 ⊕ 𝑈 ) ∈ 𝑆 ∧ ( 𝑇 ∪ 𝑈 ) ⊆ ( 𝑇 ⊕ 𝑈 ) ) → ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ⊆ ( 𝑇 ⊕ 𝑈 ) )
31 4 27 29 30 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ⊆ ( 𝑇 ⊕ 𝑈 ) )
32 26 31 eqssd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑇 ⊕ 𝑈 ) = ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )