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

Metamath Proof Explorer

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 } ) = ( 𝑁 ‘ { 𝑋 } ) )