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