Metamath Proof Explorer

Theorem lspun

Description: The span of union is the span of the union of spans. (Contributed by NM, 22-Feb-2014) (Revised by Mario Carneiro, 19-Jun-2014)

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

Proof

Step Hyp Ref Expression
1 lspss.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspss.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3 simp1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → 𝑊 ∈ LMod )
4 simp2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → 𝑇 ⊆ 𝑉 )
5 simp3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → 𝑈 ⊆ 𝑉 )
6 4 5 unssd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑇 ∪ 𝑈 ) ⊆ 𝑉 )
7 ssun1 ⊢ 𝑇 ⊆ ( 𝑇 ∪ 𝑈 )
8 7 a1i ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → 𝑇 ⊆ ( 𝑇 ∪ 𝑈 ) )
9 1 2 lspss ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑇 ∪ 𝑈 ) ⊆ 𝑉 ∧ 𝑇 ⊆ ( 𝑇 ∪ 𝑈 ) ) → ( 𝑁 ‘ 𝑇 ) ⊆ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )
10 3 6 8 9 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑇 ) ⊆ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )
11 ssun2 ⊢ 𝑈 ⊆ ( 𝑇 ∪ 𝑈 )
12 11 a1i ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → 𝑈 ⊆ ( 𝑇 ∪ 𝑈 ) )
13 1 2 lspss ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑇 ∪ 𝑈 ) ⊆ 𝑉 ∧ 𝑈 ⊆ ( 𝑇 ∪ 𝑈 ) ) → ( 𝑁 ‘ 𝑈 ) ⊆ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )
14 3 6 12 13 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑈 ) ⊆ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )
15 10 14 unssd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → ( ( 𝑁 ‘ 𝑇 ) ∪ ( 𝑁 ‘ 𝑈 ) ) ⊆ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )
16 1 2 lspssv ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑇 ∪ 𝑈 ) ⊆ 𝑉 ) → ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ⊆ 𝑉 )
17 3 6 16 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ⊆ 𝑉 )
18 15 17 sstrd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → ( ( 𝑁 ‘ 𝑇 ) ∪ ( 𝑁 ‘ 𝑈 ) ) ⊆ 𝑉 )
19 1 2 lspssid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ) → 𝑇 ⊆ ( 𝑁 ‘ 𝑇 ) )
20 3 4 19 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → 𝑇 ⊆ ( 𝑁 ‘ 𝑇 ) )
21 1 2 lspssid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ) → 𝑈 ⊆ ( 𝑁 ‘ 𝑈 ) )
22 unss12 ⊢ ( ( 𝑇 ⊆ ( 𝑁 ‘ 𝑇 ) ∧ 𝑈 ⊆ ( 𝑁 ‘ 𝑈 ) ) → ( 𝑇 ∪ 𝑈 ) ⊆ ( ( 𝑁 ‘ 𝑇 ) ∪ ( 𝑁 ‘ 𝑈 ) ) )
23 20 21 22 3imp3i2an ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑇 ∪ 𝑈 ) ⊆ ( ( 𝑁 ‘ 𝑇 ) ∪ ( 𝑁 ‘ 𝑈 ) ) )
24 1 2 lspss ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑁 ‘ 𝑇 ) ∪ ( 𝑁 ‘ 𝑈 ) ) ⊆ 𝑉 ∧ ( 𝑇 ∪ 𝑈 ) ⊆ ( ( 𝑁 ‘ 𝑇 ) ∪ ( 𝑁 ‘ 𝑈 ) ) ) → ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ⊆ ( 𝑁 ‘ ( ( 𝑁 ‘ 𝑇 ) ∪ ( 𝑁 ‘ 𝑈 ) ) ) )
25 3 18 23 24 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ⊆ ( 𝑁 ‘ ( ( 𝑁 ‘ 𝑇 ) ∪ ( 𝑁 ‘ 𝑈 ) ) ) )
26 1 2 lspss ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ⊆ 𝑉 ∧ ( ( 𝑁 ‘ 𝑇 ) ∪ ( 𝑁 ‘ 𝑈 ) ) ⊆ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ) → ( 𝑁 ‘ ( ( 𝑁 ‘ 𝑇 ) ∪ ( 𝑁 ‘ 𝑈 ) ) ) ⊆ ( 𝑁 ‘ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ) )
27 3 17 15 26 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑁 ‘ ( ( 𝑁 ‘ 𝑇 ) ∪ ( 𝑁 ‘ 𝑈 ) ) ) ⊆ ( 𝑁 ‘ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ) )
28 1 2 lspidm ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑇 ∪ 𝑈 ) ⊆ 𝑉 ) → ( 𝑁 ‘ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ) = ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )
29 3 6 28 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑁 ‘ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) ) = ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )
30 27 29 sseqtrd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑁 ‘ ( ( 𝑁 ‘ 𝑇 ) ∪ ( 𝑁 ‘ 𝑈 ) ) ) ⊆ ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) )
31 25 30 eqssd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑁 ‘ ( 𝑇 ∪ 𝑈 ) ) = ( 𝑁 ‘ ( ( 𝑁 ‘ 𝑇 ) ∪ ( 𝑁 ‘ 𝑈 ) ) ) )