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 
|- V = ( Base ` W )
lspss.n 
|- N = ( LSpan ` W )
Assertion lspun 
|- ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> ( N ` ( T u. U ) ) = ( N ` ( ( N ` T ) u. ( N ` U ) ) ) )

Proof

Step Hyp Ref Expression
1 lspss.v 
 |-  V = ( Base ` W )
2 lspss.n 
 |-  N = ( LSpan ` W )
3 simp1 
 |-  ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> W e. LMod )
4 simp2 
 |-  ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> T C_ V )
5 simp3 
 |-  ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> U C_ V )
6 4 5 unssd 
 |-  ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> ( T u. U ) C_ V )
7 ssun1 
 |-  T C_ ( T u. U )
8 7 a1i 
 |-  ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> T C_ ( T u. U ) )
9 1 2 lspss 
 |-  ( ( W e. LMod /\ ( T u. U ) C_ V /\ T C_ ( T u. U ) ) -> ( N ` T ) C_ ( N ` ( T u. U ) ) )
10 3 6 8 9 syl3anc 
 |-  ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> ( N ` T ) C_ ( N ` ( T u. U ) ) )
11 ssun2 
 |-  U C_ ( T u. U )
12 11 a1i 
 |-  ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> U C_ ( T u. U ) )
13 1 2 lspss 
 |-  ( ( W e. LMod /\ ( T u. U ) C_ V /\ U C_ ( T u. U ) ) -> ( N ` U ) C_ ( N ` ( T u. U ) ) )
14 3 6 12 13 syl3anc 
 |-  ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> ( N ` U ) C_ ( N ` ( T u. U ) ) )
15 10 14 unssd 
 |-  ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> ( ( N ` T ) u. ( N ` U ) ) C_ ( N ` ( T u. U ) ) )
16 1 2 lspssv 
 |-  ( ( W e. LMod /\ ( T u. U ) C_ V ) -> ( N ` ( T u. U ) ) C_ V )
17 3 6 16 syl2anc 
 |-  ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> ( N ` ( T u. U ) ) C_ V )
18 15 17 sstrd 
 |-  ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> ( ( N ` T ) u. ( N ` U ) ) C_ V )
19 1 2 lspssid 
 |-  ( ( W e. LMod /\ T C_ V ) -> T C_ ( N ` T ) )
20 3 4 19 syl2anc 
 |-  ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> T C_ ( N ` T ) )
21 1 2 lspssid 
 |-  ( ( W e. LMod /\ U C_ V ) -> U C_ ( N ` U ) )
22 unss12 
 |-  ( ( T C_ ( N ` T ) /\ U C_ ( N ` U ) ) -> ( T u. U ) C_ ( ( N ` T ) u. ( N ` U ) ) )
23 20 21 22 3imp3i2an 
 |-  ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> ( T u. U ) C_ ( ( N ` T ) u. ( N ` U ) ) )
24 1 2 lspss 
 |-  ( ( W e. LMod /\ ( ( N ` T ) u. ( N ` U ) ) C_ V /\ ( T u. U ) C_ ( ( N ` T ) u. ( N ` U ) ) ) -> ( N ` ( T u. U ) ) C_ ( N ` ( ( N ` T ) u. ( N ` U ) ) ) )
25 3 18 23 24 syl3anc 
 |-  ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> ( N ` ( T u. U ) ) C_ ( N ` ( ( N ` T ) u. ( N ` U ) ) ) )
26 1 2 lspss 
 |-  ( ( W e. LMod /\ ( N ` ( T u. U ) ) C_ V /\ ( ( N ` T ) u. ( N ` U ) ) C_ ( N ` ( T u. U ) ) ) -> ( N ` ( ( N ` T ) u. ( N ` U ) ) ) C_ ( N ` ( N ` ( T u. U ) ) ) )
27 3 17 15 26 syl3anc 
 |-  ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> ( N ` ( ( N ` T ) u. ( N ` U ) ) ) C_ ( N ` ( N ` ( T u. U ) ) ) )
28 1 2 lspidm 
 |-  ( ( W e. LMod /\ ( T u. U ) C_ V ) -> ( N ` ( N ` ( T u. U ) ) ) = ( N ` ( T u. U ) ) )
29 3 6 28 syl2anc 
 |-  ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> ( N ` ( N ` ( T u. U ) ) ) = ( N ` ( T u. U ) ) )
30 27 29 sseqtrd 
 |-  ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> ( N ` ( ( N ` T ) u. ( N ` U ) ) ) C_ ( N ` ( T u. U ) ) )
31 25 30 eqssd 
 |-  ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> ( N ` ( T u. U ) ) = ( N ` ( ( N ` T ) u. ( N ` U ) ) ) )