Theorem lsppr0

Description: The span of a vector paired with zero equals the span of the singleton of the vector. (Contributed by NM, 29-Aug-2014)

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

Proof

Step	Hyp	Ref	Expression
1		lsppr0.v	|- V = ( Base ` W )
2		lsppr0.z	|- .0. = ( 0g ` W )
3		lsppr0.n	|- N = ( LSpan ` W )
4		lsppr0.w	|- ( ph -> W e. LMod )
5		lsppr0.x	|- ( ph -> X e. V )
6		eqid	|- ( LSSum ` W ) = ( LSSum ` W )
7	1 2	lmod0vcl	|- ( W e. LMod -> .0. e. V )
8	4 7	syl	|- ( ph -> .0. e. V )
9	1 3 6 4 5 8	lsmpr	|- ( ph -> ( N ` { X , .0. } ) = ( ( N ` { X } ) ( LSSum ` W ) ( N ` { .0. } ) ) )
10	2 3	lspsn0	|- ( W e. LMod -> ( N ` { .0. } ) = { .0. } )
11	4 10	syl	|- ( ph -> ( N ` { .0. } ) = { .0. } )
12	11	oveq2d	|- ( ph -> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { .0. } ) ) = ( ( N ` { X } ) ( LSSum ` W ) { .0. } ) )
13	1 3	lspsnsubg	|- ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( SubGrp ` W ) )
14	4 5 13	syl2anc	|- ( ph -> ( N ` { X } ) e. ( SubGrp ` W ) )
15	2 6	lsm01	|- ( ( N ` { X } ) e. ( SubGrp ` W ) -> ( ( N ` { X } ) ( LSSum ` W ) { .0. } ) = ( N ` { X } ) )
16	14 15	syl	|- ( ph -> ( ( N ` { X } ) ( LSSum ` W ) { .0. } ) = ( N ` { X } ) )
17	9 12 16	3eqtrd	|- ( ph -> ( N ` { X , .0. } ) = ( N ` { X } ) )