Metamath Proof Explorer


Theorem lflvsdi2

Description: Reverse distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014)

Ref Expression
Hypotheses lfldi.v V = Base W
lfldi.r R = Scalar W
lfldi.k K = Base R
lfldi.p + ˙ = + R
lfldi.t · ˙ = R
lfldi.f F = LFnl W
lfldi.w φ W LMod
lfldi.x φ X K
lfldi2.y φ Y K
lfldi2.g φ G F
Assertion lflvsdi2 φ G · ˙ f V × X + ˙ f V × Y = G · ˙ f V × X + ˙ f G · ˙ f V × Y

Proof

Step Hyp Ref Expression
1 lfldi.v V = Base W
2 lfldi.r R = Scalar W
3 lfldi.k K = Base R
4 lfldi.p + ˙ = + R
5 lfldi.t · ˙ = R
6 lfldi.f F = LFnl W
7 lfldi.w φ W LMod
8 lfldi.x φ X K
9 lfldi2.y φ Y K
10 lfldi2.g φ G F
11 1 fvexi V V
12 11 a1i φ V V
13 2 3 1 6 lflf W LMod G F G : V K
14 7 10 13 syl2anc φ G : V K
15 fconst6g X K V × X : V K
16 8 15 syl φ V × X : V K
17 fconst6g Y K V × Y : V K
18 9 17 syl φ V × Y : V K
19 2 lmodring W LMod R Ring
20 7 19 syl φ R Ring
21 3 4 5 ringdi R Ring x K y K z K x · ˙ y + ˙ z = x · ˙ y + ˙ x · ˙ z
22 20 21 sylan φ x K y K z K x · ˙ y + ˙ z = x · ˙ y + ˙ x · ˙ z
23 12 14 16 18 22 caofdi φ G · ˙ f V × X + ˙ f V × Y = G · ˙ f V × X + ˙ f G · ˙ f V × Y