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

Metamath Proof Explorer

Theorem ellspsni

Description: A scalar product with a vector belongs to the span of its singleton. ( spansnmul analog.) (Contributed by NM, 2-Jul-2014)

Ref Expression
Hypotheses lspsnvsel.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspsnvsel.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
lspsnvsel.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lspsnvsel.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
lspsnvsel.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lspsnvsel.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lspsnvsel.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
lspsnvsel.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion ellspsni ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ ( 𝑁 ‘ { 𝑋 } ) )

Proof

Step Hyp Ref Expression
1 lspsnvsel.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspsnvsel.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
3 lspsnvsel.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 lspsnvsel.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
5 lspsnvsel.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
6 lspsnvsel.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
7 lspsnvsel.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
8 lspsnvsel.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
9 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
10 1 9 5 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
11 6 8 10 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
12 1 5 lspsnid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
13 6 8 12 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
14 3 2 4 9 lssvscl ⊢ ( ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) ) ∧ ( 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ) → ( 𝐴 · 𝑋 ) ∈ ( 𝑁 ‘ { 𝑋 } ) )
15 6 11 7 13 14 syl22anc ⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ ( 𝑁 ‘ { 𝑋 } ) )