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 ( ( 𝑊𝑋𝐺𝐹 ) → 𝐺 : 𝑉𝐾 )