Metamath Proof Explorer


Theorem lcdvsval

Description: Value of scalar product operation value for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015)

Ref Expression
Hypotheses lcdvsval.h H = LHyp K
lcdvsval.u U = DVecH K W
lcdvsval.v V = Base U
lcdvsval.s S = Scalar U
lcdvsval.r R = Base S
lcdvsval.t · ˙ = S
lcdvsval.c C = LCDual K W
lcdvsval.f F = Base C
lcdvsval.m ˙ = C
lcdvsval.k φ K HL W H
lcdvsval.x φ X R
lcdvsval.g φ G F
lcdvsval.a φ A V
Assertion lcdvsval φ X ˙ G A = G A · ˙ X

Proof

Step Hyp Ref Expression
1 lcdvsval.h H = LHyp K
2 lcdvsval.u U = DVecH K W
3 lcdvsval.v V = Base U
4 lcdvsval.s S = Scalar U
5 lcdvsval.r R = Base S
6 lcdvsval.t · ˙ = S
7 lcdvsval.c C = LCDual K W
8 lcdvsval.f F = Base C
9 lcdvsval.m ˙ = C
10 lcdvsval.k φ K HL W H
11 lcdvsval.x φ X R
12 lcdvsval.g φ G F
13 lcdvsval.a φ A V
14 eqid LDual U = LDual U
15 eqid LDual U = LDual U
16 1 2 14 15 7 9 10 lcdvs φ ˙ = LDual U
17 16 oveqd φ X ˙ G = X LDual U G
18 17 fveq1d φ X ˙ G A = X LDual U G A
19 eqid LFnl U = LFnl U
20 1 2 10 dvhlmod φ U LMod
21 1 7 8 2 19 10 12 lcdvbaselfl φ G LFnl U
22 19 3 4 5 6 14 15 20 11 21 13 ldualvsval φ X LDual U G A = G A · ˙ X
23 18 22 eqtrd φ X ˙ G A = G A · ˙ X