Metamath Proof Explorer


Theorem lcdneg

Description: The unit scalar of the closed kernel dual of a vector space. (Contributed by NM, 11-Jun-2015)

Ref Expression
Hypotheses lcdneg.h H = LHyp K
lcdneg.u U = DVecH K W
lcdneg.r R = Scalar U
lcdneg.m M = inv g R
lcdneg.c C = LCDual K W
lcdneg.s S = Scalar C
lcdneg.n N = inv g S
lcdneg.k φ K HL W H
Assertion lcdneg φ N = M

Proof

Step Hyp Ref Expression
1 lcdneg.h H = LHyp K
2 lcdneg.u U = DVecH K W
3 lcdneg.r R = Scalar U
4 lcdneg.m M = inv g R
5 lcdneg.c C = LCDual K W
6 lcdneg.s S = Scalar C
7 lcdneg.n N = inv g S
8 lcdneg.k φ K HL W H
9 eqid opp r R = opp r R
10 1 2 3 9 5 6 8 lcdsca φ S = opp r R
11 10 fveq2d φ inv g S = inv g opp r R
12 9 4 opprneg M = inv g opp r R
13 11 7 12 3eqtr4g φ N = M