Metamath Proof Explorer


Theorem ldualvsass

Description: Associative law for scalar product operation. (Contributed by NM, 20-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 ldualvsass.f F = LFnl W
2 ldualvsass.r R = Scalar W
3 ldualvsass.k K = Base R
4 ldualvsass.t × ˙ = R
5 ldualvsass.d D = LDual W
6 ldualvsass.s · ˙ = D
7 ldualvsass.w φ W LMod
8 ldualvsass.x φ X K
9 ldualvsass.y φ Y K
10 ldualvsass.g φ G F
11 eqid Base W = Base W
12 11 2 3 4 1 7 9 8 10 lflvsass φ G × ˙ f Base W × Y × ˙ X = G × ˙ f Base W × Y × ˙ f Base W × X
13 2 lmodring W LMod R Ring
14 7 13 syl φ R Ring
15 3 4 ringcl R Ring Y K X K Y × ˙ X K
16 14 9 8 15 syl3anc φ Y × ˙ X K
17 1 11 2 3 4 5 6 7 16 10 ldualvs φ Y × ˙ X · ˙ G = G × ˙ f Base W × Y × ˙ X
18 11 2 3 4 1 7 10 9 lflvscl φ G × ˙ f Base W × Y F
19 1 11 2 3 4 5 6 7 8 18 ldualvs φ X · ˙ G × ˙ f Base W × Y = G × ˙ f Base W × Y × ˙ f Base W × X
20 12 17 19 3eqtr4d φ Y × ˙ X · ˙ G = X · ˙ G × ˙ f Base W × Y
21 1 11 2 3 4 5 6 7 9 10 ldualvs φ Y · ˙ G = G × ˙ f Base W × Y
22 21 oveq2d φ X · ˙ Y · ˙ G = X · ˙ G × ˙ f Base W × Y
23 20 22 eqtr4d φ Y × ˙ X · ˙ G = X · ˙ Y · ˙ G