Theorem lflcl

Description: A linear functional value is a scalar. (Contributed by NM, 15-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		lflf.d	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
2		lflf.k	⊢ 𝐾 = ( Base ‘ 𝐷 )
3		lflf.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
4		lflf.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
5	1 2 3 4	lflf	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ 𝐾 )
6	5	3adant3	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → 𝐺 : 𝑉 ⟶ 𝐾 )
7		simp3	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
8	6 7	ffvelrnd	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑋 ) ∈ 𝐾 )