This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lspun0

Description: The span of a union with the zero subspace. (Contributed by NM, 22-May-2015)

Ref Expression
Hypotheses lspun0.v 
|- V = ( Base ` W )
lspun0.o 
|- .0. = ( 0g ` W )
lspun0.n 
|- N = ( LSpan ` W )
lspun0.w 
|- ( ph -> W e. LMod )
lspun0.x 
|- ( ph -> X C_ V )
Assertion lspun0 
|- ( ph -> ( N ` ( X u. { .0. } ) ) = ( N ` X ) )

Proof

Step Hyp Ref Expression
1 lspun0.v 
 |-  V = ( Base ` W )
2 lspun0.o 
 |-  .0. = ( 0g ` W )
3 lspun0.n 
 |-  N = ( LSpan ` W )
4 lspun0.w 
 |-  ( ph -> W e. LMod )
5 lspun0.x 
 |-  ( ph -> X C_ V )
6 1 2 lmod0vcl 
 |-  ( W e. LMod -> .0. e. V )
7 4 6 syl 
 |-  ( ph -> .0. e. V )
8 7 snssd 
 |-  ( ph -> { .0. } C_ V )
9 1 3 lspun 
 |-  ( ( W e. LMod /\ X C_ V /\ { .0. } C_ V ) -> ( N ` ( X u. { .0. } ) ) = ( N ` ( ( N ` X ) u. ( N ` { .0. } ) ) ) )
10 4 5 8 9 syl3anc 
 |-  ( ph -> ( N ` ( X u. { .0. } ) ) = ( N ` ( ( N ` X ) u. ( N ` { .0. } ) ) ) )
11 2 3 lspsn0 
 |-  ( W e. LMod -> ( N ` { .0. } ) = { .0. } )
12 4 11 syl 
 |-  ( ph -> ( N ` { .0. } ) = { .0. } )
13 12 uneq2d 
 |-  ( ph -> ( ( N ` X ) u. ( N ` { .0. } ) ) = ( ( N ` X ) u. { .0. } ) )
14 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
15 1 14 3 lspcl 
 |-  ( ( W e. LMod /\ X C_ V ) -> ( N ` X ) e. ( LSubSp ` W ) )
16 4 5 15 syl2anc 
 |-  ( ph -> ( N ` X ) e. ( LSubSp ` W ) )
17 2 14 lss0ss 
 |-  ( ( W e. LMod /\ ( N ` X ) e. ( LSubSp ` W ) ) -> { .0. } C_ ( N ` X ) )
18 4 16 17 syl2anc 
 |-  ( ph -> { .0. } C_ ( N ` X ) )
19 ssequn2 
 |-  ( { .0. } C_ ( N ` X ) <-> ( ( N ` X ) u. { .0. } ) = ( N ` X ) )
20 18 19 sylib 
 |-  ( ph -> ( ( N ` X ) u. { .0. } ) = ( N ` X ) )
21 13 20 eqtrd 
 |-  ( ph -> ( ( N ` X ) u. ( N ` { .0. } ) ) = ( N ` X ) )
22 21 fveq2d 
 |-  ( ph -> ( N ` ( ( N ` X ) u. ( N ` { .0. } ) ) ) = ( N ` ( N ` X ) ) )
23 1 3 lspidm 
 |-  ( ( W e. LMod /\ X C_ V ) -> ( N ` ( N ` X ) ) = ( N ` X ) )
24 4 5 23 syl2anc 
 |-  ( ph -> ( N ` ( N ` X ) ) = ( N ` X ) )
25 22 24 eqtrd 
 |-  ( ph -> ( N ` ( ( N ` X ) u. ( N ` { .0. } ) ) ) = ( N ` X ) )
26 10 25 eqtrd 
 |-  ( ph -> ( N ` ( X u. { .0. } ) ) = ( N ` X ) )