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

Metamath Proof Explorer

Theorem ldual1

Description: The unit scalar of the dual of a vector space. (Contributed by NM, 26-Feb-2015)

Step	Hyp	Ref	Expression
1		ldual1.r	$⊢ R = Scalar (W)$
2		ldual1.u	$⊢ \underset{˙}{1} = 1_{R}$
3		ldual1.d	$⊢ D = LDual (W)$
4		ldual1.s	$⊢ S = Scalar (D)$
5		ldual1.i	$⊢ I = 1_{S}$
6		ldual1.w	$⊢ φ \to W \in LMod$
7		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
8	1 7 3 4 6	ldualsca	$⊢ φ \to S = {opp}_{r} (R)$
9	8	fveq2d	$⊢ φ \to 1_{S} = 1_{{opp}_{r} (R)}$
10	7 2	oppr1	$⊢ \underset{˙}{1} = 1_{{opp}_{r} (R)}$
11	9 5 10	3eqtr4g	$⊢ φ \to I = \underset{˙}{1}$