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	$⊢ 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$
Assertion	ldualvs	$⊢ φ \to X \underset{˙}{∙} G = G {\underset{˙}{\times}}_{f} (V \times \{X\})$

Proof

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		eqid	$⊢ (k \in K, f \in F ⟼ f {\underset{˙}{\times}}_{f} (V \times \{k\})) = (k \in K, f \in F ⟼ f {\underset{˙}{\times}}_{f} (V \times \{k\}))$
12	1 2 3 4 5 6 7 8 11	ldualfvs	$⊢ φ \to \underset{˙}{∙} = (k \in K, f \in F ⟼ f {\underset{˙}{\times}}_{f} (V \times \{k\}))$
13	12	oveqd	$⊢ φ \to X \underset{˙}{∙} G = X (k \in K, f \in F ⟼ f {\underset{˙}{\times}}_{f} (V \times \{k\})) G$
14		sneq	$⊢ k = X \to \{k\} = \{X\}$
15	14	xpeq2d	$⊢ k = X \to V \times \{k\} = V \times \{X\}$
16	15	oveq2d	$⊢ k = X \to f {\underset{˙}{\times}}_{f} (V \times \{k\}) = f {\underset{˙}{\times}}_{f} (V \times \{X\})$
17		oveq1	$⊢ f = G \to f {\underset{˙}{\times}}_{f} (V \times \{X\}) = G {\underset{˙}{\times}}_{f} (V \times \{X\})$
18		ovex	$⊢ G {\underset{˙}{\times}}_{f} (V \times \{X\}) \in V$
19	16 17 11 18	ovmpo	$⊢ (X \in K \land G \in F) \to X (k \in K, f \in F ⟼ f {\underset{˙}{\times}}_{f} (V \times \{k\})) G = G {\underset{˙}{\times}}_{f} (V \times \{X\})$
20	9 10 19	syl2anc	$⊢ φ \to X (k \in K, f \in F ⟼ f {\underset{˙}{\times}}_{f} (V \times \{k\})) G = G {\underset{˙}{\times}}_{f} (V \times \{X\})$
21	13 20	eqtrd	$⊢ φ \to X \underset{˙}{∙} G = G {\underset{˙}{\times}}_{f} (V \times \{X\})$

Metamath Proof Explorer

Theorem ldualvs

Proof