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 ) ) ) )