Theorem ldualvsval

Description: Value of scalar product operation value for the dual of a vector space. (Contributed by NM, 18-Oct-2014)

	Ref	Expression
Hypotheses	ldualfvs.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	ldualfvs.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	ldualfvs.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
	ldualfvs.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	ldualfvs.t	⊢ × = ( .r ‘ 𝑅 )
	ldualfvs.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
	ldualfvs.s	⊢ ∙ = ( ·𝑠 ‘ 𝐷 )
	ldualfvs.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑌 )
	ldualvs.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
	ldualvs.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
	ldualvs.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	ldualvsval	⊢ ( 𝜑 → ( ( 𝑋 ∙ 𝐺 ) ‘ 𝐴 ) = ( ( 𝐺 ‘ 𝐴 ) × 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		ldualfvs.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2		ldualfvs.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
3		ldualfvs.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
4		ldualfvs.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
5		ldualfvs.t	⊢ × = ( .r ‘ 𝑅 )
6		ldualfvs.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
7		ldualfvs.s	⊢ ∙ = ( ·𝑠 ‘ 𝐷 )
8		ldualfvs.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑌 )
9		ldualvs.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
10		ldualvs.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
11		ldualvs.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
12	1 2 3 4 5 6 7 8 9 10	ldualvs	⊢ ( 𝜑 → ( 𝑋 ∙ 𝐺 ) = ( 𝐺 ∘f × ( 𝑉 × { 𝑋 } ) ) )
13	12	fveq1d	⊢ ( 𝜑 → ( ( 𝑋 ∙ 𝐺 ) ‘ 𝐴 ) = ( ( 𝐺 ∘f × ( 𝑉 × { 𝑋 } ) ) ‘ 𝐴 ) )
14	2	fvexi	⊢ 𝑉 ∈ V
15	14	a1i	⊢ ( 𝜑 → 𝑉 ∈ V )
16	3 4 2 1	lflf	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ 𝐾 )
17	8 10 16	syl2anc	⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ 𝐾 )
18	17	ffnd	⊢ ( 𝜑 → 𝐺 Fn 𝑉 )
19		eqidd	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐺 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) )
20	15 9 18 19	ofc2	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐺 ∘f × ( 𝑉 × { 𝑋 } ) ) ‘ 𝐴 ) = ( ( 𝐺 ‘ 𝐴 ) × 𝑋 ) )
21	11 20	mpdan	⊢ ( 𝜑 → ( ( 𝐺 ∘f × ( 𝑉 × { 𝑋 } ) ) ‘ 𝐴 ) = ( ( 𝐺 ‘ 𝐴 ) × 𝑋 ) )
22	13 21	eqtrd	⊢ ( 𝜑 → ( ( 𝑋 ∙ 𝐺 ) ‘ 𝐴 ) = ( ( 𝐺 ‘ 𝐴 ) × 𝑋 ) )