Metamath Proof Explorer


Theorem ldual1

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

Ref Expression
Hypotheses ldual1.r R = Scalar W
ldual1.u 1 ˙ = 1 R
ldual1.d D = LDual W
ldual1.s S = Scalar D
ldual1.i I = 1 S
ldual1.w φ W LMod
Assertion ldual1 φ I = 1 ˙

Proof

Step Hyp Ref Expression
1 ldual1.r R = Scalar W
2 ldual1.u 1 ˙ = 1 R
3 ldual1.d D = LDual W
4 ldual1.s S = Scalar D
5 ldual1.i I = 1 S
6 ldual1.w φ W LMod
7 eqid opp r R = opp r R
8 1 7 3 4 6 ldualsca φ S = opp r R
9 8 fveq2d φ 1 S = 1 opp r R
10 7 2 oppr1 1 ˙ = 1 opp r R
11 9 5 10 3eqtr4g φ I = 1 ˙