Theorem ldualvs

Description: Scalar product operation value (which is a functional) 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	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion	ldualvs	⊢ ( 𝜑 → ( 𝑋 ∙ 𝐺 ) = ( 𝐺 ∘f × ( 𝑉 × { 𝑋 } ) ) )

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		eqid	⊢ ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) = ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) )
12	1 2 3 4 5 6 7 8 11	ldualfvs	⊢ ( 𝜑 → ∙ = ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) )
13	12	oveqd	⊢ ( 𝜑 → ( 𝑋 ∙ 𝐺 ) = ( 𝑋 ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) 𝐺 ) )
14		sneq	⊢ ( 𝑘 = 𝑋 → { 𝑘 } = { 𝑋 } )
15	14	xpeq2d	⊢ ( 𝑘 = 𝑋 → ( 𝑉 × { 𝑘 } ) = ( 𝑉 × { 𝑋 } ) )
16	15	oveq2d	⊢ ( 𝑘 = 𝑋 → ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) = ( 𝑓 ∘f × ( 𝑉 × { 𝑋 } ) ) )
17		oveq1	⊢ ( 𝑓 = 𝐺 → ( 𝑓 ∘f × ( 𝑉 × { 𝑋 } ) ) = ( 𝐺 ∘f × ( 𝑉 × { 𝑋 } ) ) )
18		ovex	⊢ ( 𝐺 ∘f × ( 𝑉 × { 𝑋 } ) ) ∈ V
19	16 17 11 18	ovmpo	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝐺 ∈ 𝐹 ) → ( 𝑋 ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) 𝐺 ) = ( 𝐺 ∘f × ( 𝑉 × { 𝑋 } ) ) )
20	9 10 19	syl2anc	⊢ ( 𝜑 → ( 𝑋 ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) 𝐺 ) = ( 𝐺 ∘f × ( 𝑉 × { 𝑋 } ) ) )
21	13 20	eqtrd	⊢ ( 𝜑 → ( 𝑋 ∙ 𝐺 ) = ( 𝐺 ∘f × ( 𝑉 × { 𝑋 } ) ) )