Metamath Proof Explorer


Theorem ldualvsval

Description: Value of scalar product operation value for the dual of a vector space. (Contributed by NM, 18-Oct-2014)

Ref Expression
Hypotheses ldualfvs.f F = LFnl W
ldualfvs.v V = Base W
ldualfvs.r R = Scalar W
ldualfvs.k K = Base R
ldualfvs.t × ˙ = R
ldualfvs.d D = LDual W
ldualfvs.s ˙ = D
ldualfvs.w φ W Y
ldualvs.x φ X K
ldualvs.g φ G F
ldualvs.a φ A V
Assertion ldualvsval φ X ˙ G A = G A × ˙ X

Proof

Step Hyp Ref Expression
1 ldualfvs.f F = LFnl W
2 ldualfvs.v V = Base W
3 ldualfvs.r R = Scalar W
4 ldualfvs.k K = Base R
5 ldualfvs.t × ˙ = R
6 ldualfvs.d D = LDual W
7 ldualfvs.s ˙ = D
8 ldualfvs.w φ W Y
9 ldualvs.x φ X K
10 ldualvs.g φ G F
11 ldualvs.a φ A V
12 1 2 3 4 5 6 7 8 9 10 ldualvs φ X ˙ G = G × ˙ f V × X
13 12 fveq1d φ X ˙ G A = G × ˙ f V × X A
14 2 fvexi V V
15 14 a1i φ V V
16 3 4 2 1 lflf W Y G F G : V K
17 8 10 16 syl2anc φ G : V K
18 17 ffnd φ G Fn V
19 eqidd φ A V G A = G A
20 15 9 18 19 ofc2 φ A V G × ˙ f V × X A = G A × ˙ X
21 11 20 mpdan φ G × ˙ f V × X A = G A × ˙ X
22 13 21 eqtrd φ X ˙ G A = G A × ˙ X