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 = LFnl (W)$
	ldualfvs.v	$⊢ V = {Base}_{W}$
	ldualfvs.r	$⊢ R = Scalar (W)$
	ldualfvs.k	$⊢ K = {Base}_{R}$
	ldualfvs.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
	ldualfvs.d	$⊢ D = LDual (W)$
	ldualfvs.s	$⊢ \underset{˙}{∙} = \cdot_{D}$
	ldualfvs.w	$⊢ φ \to W \in Y$
	ldualvs.x	$⊢ φ \to X \in K$
	ldualvs.g	$⊢ φ \to G \in F$
	ldualvs.a	$⊢ φ \to A \in V$
Assertion	ldualvsval	$⊢ φ \to (X \underset{˙}{∙} G) (A) = G (A) \underset{˙}{\times} X$

Step	Hyp	Ref	Expression
1		ldualfvs.f	$⊢ F = LFnl (W)$
2		ldualfvs.v	$⊢ V = {Base}_{W}$
3		ldualfvs.r	$⊢ R = Scalar (W)$
4		ldualfvs.k	$⊢ K = {Base}_{R}$
5		ldualfvs.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
6		ldualfvs.d	$⊢ D = LDual (W)$
7		ldualfvs.s	$⊢ \underset{˙}{∙} = \cdot_{D}$
8		ldualfvs.w	$⊢ φ \to W \in Y$
9		ldualvs.x	$⊢ φ \to X \in K$
10		ldualvs.g	$⊢ φ \to G \in F$
11		ldualvs.a	$⊢ φ \to A \in V$
12	1 2 3 4 5 6 7 8 9 10	ldualvs	$⊢ φ \to X \underset{˙}{∙} G = G {\underset{˙}{\times}}_{f} (V \times \{X\})$
13	12	fveq1d	$⊢ φ \to (X \underset{˙}{∙} G) (A) = (G {\underset{˙}{\times}}_{f} (V \times \{X\})) (A)$
14	2	fvexi	$⊢ V \in V$
15	14	a1i	$⊢ φ \to V \in V$
16	3 4 2 1	lflf	$⊢ (W \in Y \land G \in F) \to G : V ⟶ K$
17	8 10 16	syl2anc	$⊢ φ \to G : V ⟶ K$
18	17	ffnd	$⊢ φ \to G Fn V$
19		eqidd	$⊢ (φ \land A \in V) \to G (A) = G (A)$
20	15 9 18 19	ofc2	$⊢ (φ \land A \in V) \to (G {\underset{˙}{\times}}_{f} (V \times \{X\})) (A) = G (A) \underset{˙}{\times} X$
21	11 20	mpdan	$⊢ φ \to (G {\underset{˙}{\times}}_{f} (V \times \{X\})) (A) = G (A) \underset{˙}{\times} X$
22	13 21	eqtrd	$⊢ φ \to (X \underset{˙}{∙} G) (A) = G (A) \underset{˙}{\times} X$

Metamath Proof Explorer