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