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 ⊢ D = Scalar ⁡ W
lflf.k ⊢ K = Base D
lflf.v ⊢ V = Base W
lflf.f ⊢ F = LFnl ⁡ W
Assertion lflf ⊢ W ∈ X ∧ G ∈ F → G : V ⟶ K

Proof

Step Hyp Ref Expression
1 lflf.d ⊢ D = Scalar ⁡ W
2 lflf.k ⊢ K = Base D
3 lflf.v ⊢ V = Base W
4 lflf.f ⊢ F = LFnl ⁡ W
5 eqid ⊢ + W = + W
6 eqid ⊢ ⋅ W = ⋅ W
7 eqid ⊢ + D = + D
8 eqid ⊢ ⋅ D = ⋅ D
9 3 5 1 6 2 7 8 4 islfl ⊢ W ∈ X → G ∈ F ↔ G : V ⟶ K ∧ ∀ r ∈ K ∀ x ∈ V ∀ y ∈ V G ⁡ r ⋅ W x + W y = r ⋅ D G ⁡ x + D G ⁡ y
10 9 simprbda ⊢ W ∈ X ∧ G ∈ F → G : V ⟶ K