Metamath Proof Explorer


Theorem ldualvsass2

Description: Associative law for scalar product operation, using operations from the dual space. (Contributed by NM, 20-Oct-2014)

Ref Expression
Hypotheses ldualvsass2.f F = LFnl W
ldualvsass2.r R = Scalar W
ldualvsass2.k K = Base R
ldualvsass2.d D = LDual W
ldualvsass2.q Q = Scalar D
ldualvsass2.t × ˙ = Q
ldualvsass2.s · ˙ = D
ldualvsass2.w φ W LMod
ldualvsass2.x φ X K
ldualvsass2.y φ Y K
ldualvsass2.g φ G F
Assertion ldualvsass2 φ X × ˙ Y · ˙ G = X · ˙ Y · ˙ G

Proof

Step Hyp Ref Expression
1 ldualvsass2.f F = LFnl W
2 ldualvsass2.r R = Scalar W
3 ldualvsass2.k K = Base R
4 ldualvsass2.d D = LDual W
5 ldualvsass2.q Q = Scalar D
6 ldualvsass2.t × ˙ = Q
7 ldualvsass2.s · ˙ = D
8 ldualvsass2.w φ W LMod
9 ldualvsass2.x φ X K
10 ldualvsass2.y φ Y K
11 ldualvsass2.g φ G F
12 eqid R = R
13 2 3 12 4 5 6 8 9 10 ldualsmul φ X × ˙ Y = Y R X
14 13 oveq1d φ X × ˙ Y · ˙ G = Y R X · ˙ G
15 1 2 3 12 4 7 8 9 10 11 ldualvsass φ Y R X · ˙ G = X · ˙ Y · ˙ G
16 14 15 eqtrd φ X × ˙ Y · ˙ G = X · ˙ Y · ˙ G