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