This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ldualelvbase

Description: Utility theorem for converting a functional to a vector of the dual space in order to use standard vector theorems. (Contributed by NM, 6-Jan-2015)

	Ref	Expression
Hypotheses	ldualelvbase.f	$⊢ F = LFnl (W)$
	ldualelvbase.d	$⊢ D = LDual (W)$
	ldualelvbase.v	$⊢ V = {Base}_{D}$
	ldualelvbase.w	$⊢ φ \to W \in X$
	ldualelvbase.g	$⊢ φ \to G \in F$
Assertion	ldualelvbase	$⊢ φ \to G \in V$

Proof

Step	Hyp	Ref	Expression
1		ldualelvbase.f	$⊢ F = LFnl (W)$
2		ldualelvbase.d	$⊢ D = LDual (W)$
3		ldualelvbase.v	$⊢ V = {Base}_{D}$
4		ldualelvbase.w	$⊢ φ \to W \in X$
5		ldualelvbase.g	$⊢ φ \to G \in F$
6	1 2 3 4	ldualvbase	$⊢ φ \to V = F$
7	5 6	eleqtrrd	$⊢ φ \to G \in V$