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 𝐻 = ( LHyp ‘ 𝐾 )
lcdneg.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lcdneg.r 𝑅 = ( Scalar ‘ 𝑈 )
lcdneg.m 𝑀 = ( invg𝑅 )
lcdneg.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
lcdneg.s 𝑆 = ( Scalar ‘ 𝐶 )
lcdneg.n 𝑁 = ( invg𝑆 )
lcdneg.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
Assertion lcdneg ( 𝜑𝑁 = 𝑀 )

Proof

Step Hyp Ref Expression
1 lcdneg.h 𝐻 = ( LHyp ‘ 𝐾 )
2 lcdneg.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 lcdneg.r 𝑅 = ( Scalar ‘ 𝑈 )
4 lcdneg.m 𝑀 = ( invg𝑅 )
5 lcdneg.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6 lcdneg.s 𝑆 = ( Scalar ‘ 𝐶 )
7 lcdneg.n 𝑁 = ( invg𝑆 )
8 lcdneg.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
9 eqid ( oppr𝑅 ) = ( oppr𝑅 )
10 1 2 3 9 5 6 8 lcdsca ( 𝜑𝑆 = ( oppr𝑅 ) )
11 10 fveq2d ( 𝜑 → ( invg𝑆 ) = ( invg ‘ ( oppr𝑅 ) ) )
12 9 4 opprneg 𝑀 = ( invg ‘ ( oppr𝑅 ) )
13 11 7 12 3eqtr4g ( 𝜑𝑁 = 𝑀 )