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	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	ldualfvs.v	$$⊢V={\mathrm{Base}}_W$$
	ldualfvs.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
	ldualfvs.k	$$⊢K={\mathrm{Base}}_R$$
	ldualfvs.t	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
	ldualfvs.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualfvs.s	$$⊢\underset{\dot{}}{\bullet }={\cdot }_D$$
	ldualfvs.w	$$⊢\phi \to W\in Y$$
	ldualvs.x	$$⊢\phi \to X\in K$$
	ldualvs.g	$$⊢\phi \to G\in F$$
	ldualvs.a	$$⊢\phi \to A\in V$$
Assertion	ldualvsval	$$⊢\phi \to \left(X\underset{\dot{}}{\bullet }G\right)\left(A\right)=G\left(A\right)\underset{\dot{}}{\times }X$$

Proof

Step	Hyp	Ref	Expression
1		ldualfvs.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
2		ldualfvs.v	$$⊢V={\mathrm{Base}}_W$$
3		ldualfvs.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
4		ldualfvs.k	$$⊢K={\mathrm{Base}}_R$$
5		ldualfvs.t	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
6		ldualfvs.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
7		ldualfvs.s	$$⊢\underset{\dot{}}{\bullet }={\cdot }_D$$
8		ldualfvs.w	$$⊢\phi \to W\in Y$$
9		ldualvs.x	$$⊢\phi \to X\in K$$
10		ldualvs.g	$$⊢\phi \to G\in F$$
11		ldualvs.a	$$⊢\phi \to A\in V$$
12	1 2 3 4 5 6 7 8 9 10	ldualvs	$$⊢\phi \to X\underset{\dot{}}{\bullet }G=G{\underset{\dot{}}{\times }}_f\left(V\times \left\{X\right\}\right)$$
13	12	fveq1d	$$⊢\phi \to \left(X\underset{\dot{}}{\bullet }G\right)\left(A\right)=\left(G{\underset{\dot{}}{\times }}_f\left(V\times \left\{X\right\}\right)\right)\left(A\right)$$
14	2	fvexi	$$⊢V\in \mathrm{V}$$
15	14	a1i	$$⊢\phi \to V\in \mathrm{V}$$
16	3 4 2 1	lflf	$$⊢\left(W\in Y\wedge G\in F\right)\to G:V⟶K$$
17	8 10 16	syl2anc	$$⊢\phi \to G:V⟶K$$
18	17	ffnd	$$⊢\phi \to GFnV$$
19		eqidd	$$⊢\left(\phi \wedge A\in V\right)\to G\left(A\right)=G\left(A\right)$$
20	15 9 18 19	ofc2	$$⊢\left(\phi \wedge A\in V\right)\to \left(G{\underset{\dot{}}{\times }}_f\left(V\times \left\{X\right\}\right)\right)\left(A\right)=G\left(A\right)\underset{\dot{}}{\times }X$$
21	11 20	mpdan	$$⊢\phi \to \left(G{\underset{\dot{}}{\times }}_f\left(V\times \left\{X\right\}\right)\right)\left(A\right)=G\left(A\right)\underset{\dot{}}{\times }X$$
22	13 21	eqtrd	$$⊢\phi \to \left(X\underset{\dot{}}{\bullet }G\right)\left(A\right)=G\left(A\right)\underset{\dot{}}{\times }X$$