Metamath Proof Explorer

Theorem lsmssspx

Description: Subspace sum (in its extended domain) is a subset of the span of the union of its arguments. (Contributed by NM, 6-Aug-2014)

Ref Expression
Hypotheses lsmsp2.v 
|- V = ( Base ` W )
lsmsp2.n 
|- N = ( LSpan ` W )
lsmsp2.p 
|- .(+) = ( LSSum ` W )
lsmssspx.t 
|- ( ph -> T C_ V )
lsmssspx.u 
|- ( ph -> U C_ V )
lsmssspx.w 
|- ( ph -> W e. LMod )
Assertion lsmssspx 
|- ( ph -> ( T .(+) U ) C_ ( N ` ( T u. U ) ) )

Proof

Step Hyp Ref Expression
1 lsmsp2.v 
 |-  V = ( Base ` W )
2 lsmsp2.n 
 |-  N = ( LSpan ` W )
3 lsmsp2.p 
 |-  .(+) = ( LSSum ` W )
4 lsmssspx.t 
 |-  ( ph -> T C_ V )
5 lsmssspx.u 
 |-  ( ph -> U C_ V )
6 lsmssspx.w 
 |-  ( ph -> W e. LMod )
7 1 2 lspssv 
 |-  ( ( W e. LMod /\ T C_ V ) -> ( N ` T ) C_ V )
8 6 4 7 syl2anc 
 |-  ( ph -> ( N ` T ) C_ V )
9 1 2 lspssid 
 |-  ( ( W e. LMod /\ T C_ V ) -> T C_ ( N ` T ) )
10 6 4 9 syl2anc 
 |-  ( ph -> T C_ ( N ` T ) )
11 1 3 lsmless1x 
 |-  ( ( ( W e. LMod /\ ( N ` T ) C_ V /\ U C_ V ) /\ T C_ ( N ` T ) ) -> ( T .(+) U ) C_ ( ( N ` T ) .(+) U ) )
12 6 8 5 10 11 syl31anc 
 |-  ( ph -> ( T .(+) U ) C_ ( ( N ` T ) .(+) U ) )
13 1 2 lspssv 
 |-  ( ( W e. LMod /\ U C_ V ) -> ( N ` U ) C_ V )
14 6 5 13 syl2anc 
 |-  ( ph -> ( N ` U ) C_ V )
15 1 2 lspssid 
 |-  ( ( W e. LMod /\ U C_ V ) -> U C_ ( N ` U ) )
16 6 5 15 syl2anc 
 |-  ( ph -> U C_ ( N ` U ) )
17 1 3 lsmless2x 
 |-  ( ( ( W e. LMod /\ ( N ` T ) C_ V /\ ( N ` U ) C_ V ) /\ U C_ ( N ` U ) ) -> ( ( N ` T ) .(+) U ) C_ ( ( N ` T ) .(+) ( N ` U ) ) )
18 6 8 14 16 17 syl31anc 
 |-  ( ph -> ( ( N ` T ) .(+) U ) C_ ( ( N ` T ) .(+) ( N ` U ) ) )
19 12 18 sstrd 
 |-  ( ph -> ( T .(+) U ) C_ ( ( N ` T ) .(+) ( N ` U ) ) )
20 1 2 3 lsmsp2 
 |-  ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> ( ( N ` T ) .(+) ( N ` U ) ) = ( N ` ( T u. U ) ) )
21 6 4 5 20 syl3anc 
 |-  ( ph -> ( ( N ` T ) .(+) ( N ` U ) ) = ( N ` ( T u. U ) ) )
22 19 21 sseqtrd 
 |-  ( ph -> ( T .(+) U ) C_ ( N ` ( T u. U ) ) )