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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lsppr0.z	⊢ 0 = ( 0g ‘ 𝑊 )
	lsppr0.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lsppr0.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lsppr0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	lsppr0	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 0 } ) = ( 𝑁 ‘ { 𝑋 } ) )

Proof

Step	Hyp	Ref	Expression
1		lsppr0.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lsppr0.z	⊢ 0 = ( 0g ‘ 𝑊 )
3		lsppr0.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4		lsppr0.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
5		lsppr0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
6		eqid	⊢ ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
7	1 2	lmod0vcl	⊢ ( 𝑊 ∈ LMod → 0 ∈ 𝑉 )
8	4 7	syl	⊢ ( 𝜑 → 0 ∈ 𝑉 )
9	1 3 6 4 5 8	lsmpr	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 0 } ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 0 } ) ) )
10	2 3	lspsn0	⊢ ( 𝑊 ∈ LMod → ( 𝑁 ‘ { 0 } ) = { 0 } )
11	4 10	syl	⊢ ( 𝜑 → ( 𝑁 ‘ { 0 } ) = { 0 } )
12	11	oveq2d	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 0 } ) ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) { 0 } ) )
13	1 3	lspsnsubg	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
14	4 5 13	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
15	2 6	lsm01	⊢ ( ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) { 0 } ) = ( 𝑁 ‘ { 𝑋 } ) )
16	14 15	syl	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) { 0 } ) = ( 𝑁 ‘ { 𝑋 } ) )
17	9 12 16	3eqtrd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 0 } ) = ( 𝑁 ‘ { 𝑋 } ) )