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

Metamath Proof Explorer

Theorem lflf

Description: A linear functional is a function from vectors to scalars. ( lnfnfi analog.) (Contributed by NM, 15-Apr-2014)

Ref Expression
Hypotheses lflf.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
lflf.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
lflf.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lflf.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
Assertion lflf ( ( 𝑊 ∈ 𝑋 ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ 𝐾 )

Proof

Step Hyp Ref Expression
1 lflf.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
2 lflf.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
3 lflf.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
4 lflf.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
5 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
6 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
7 eqid ⊢ ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 )
8 eqid ⊢ ( .r ‘ 𝐷 ) = ( .r ‘ 𝐷 )
9 3 5 1 6 2 7 8 4 islfl ⊢ ( 𝑊 ∈ 𝑋 → ( 𝐺 ∈ 𝐹 ↔ ( 𝐺 : 𝑉 ⟶ 𝐾 ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑦 ) ) ) ) )
10 9 simprbda ⊢ ( ( 𝑊 ∈ 𝑋 ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ 𝐾 )