Metamath Proof Explorer


Theorem lflvsdi2a

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

Ref Expression
Hypotheses lfldi.v 𝑉 = ( Base ‘ 𝑊 )
lfldi.r 𝑅 = ( Scalar ‘ 𝑊 )
lfldi.k 𝐾 = ( Base ‘ 𝑅 )
lfldi.p + = ( +g𝑅 )
lfldi.t · = ( .r𝑅 )
lfldi.f 𝐹 = ( LFnl ‘ 𝑊 )
lfldi.w ( 𝜑𝑊 ∈ LMod )
lfldi.x ( 𝜑𝑋𝐾 )
lfldi2.y ( 𝜑𝑌𝐾 )
lfldi2.g ( 𝜑𝐺𝐹 )
Assertion lflvsdi2a ( 𝜑 → ( 𝐺f · ( 𝑉 × { ( 𝑋 + 𝑌 ) } ) ) = ( ( 𝐺f · ( 𝑉 × { 𝑋 } ) ) ∘f + ( 𝐺f · ( 𝑉 × { 𝑌 } ) ) ) )

Proof

Step Hyp Ref Expression
1 lfldi.v 𝑉 = ( Base ‘ 𝑊 )
2 lfldi.r 𝑅 = ( Scalar ‘ 𝑊 )
3 lfldi.k 𝐾 = ( Base ‘ 𝑅 )
4 lfldi.p + = ( +g𝑅 )
5 lfldi.t · = ( .r𝑅 )
6 lfldi.f 𝐹 = ( LFnl ‘ 𝑊 )
7 lfldi.w ( 𝜑𝑊 ∈ LMod )
8 lfldi.x ( 𝜑𝑋𝐾 )
9 lfldi2.y ( 𝜑𝑌𝐾 )
10 lfldi2.g ( 𝜑𝐺𝐹 )
11 1 fvexi 𝑉 ∈ V
12 11 a1i ( 𝜑𝑉 ∈ V )
13 12 8 9 ofc12 ( 𝜑 → ( ( 𝑉 × { 𝑋 } ) ∘f + ( 𝑉 × { 𝑌 } ) ) = ( 𝑉 × { ( 𝑋 + 𝑌 ) } ) )
14 13 oveq2d ( 𝜑 → ( 𝐺f · ( ( 𝑉 × { 𝑋 } ) ∘f + ( 𝑉 × { 𝑌 } ) ) ) = ( 𝐺f · ( 𝑉 × { ( 𝑋 + 𝑌 ) } ) ) )
15 1 2 3 4 5 6 7 8 9 10 lflvsdi2 ( 𝜑 → ( 𝐺f · ( ( 𝑉 × { 𝑋 } ) ∘f + ( 𝑉 × { 𝑌 } ) ) ) = ( ( 𝐺f · ( 𝑉 × { 𝑋 } ) ) ∘f + ( 𝐺f · ( 𝑉 × { 𝑌 } ) ) ) )
16 14 15 eqtr3d ( 𝜑 → ( 𝐺f · ( 𝑉 × { ( 𝑋 + 𝑌 ) } ) ) = ( ( 𝐺f · ( 𝑉 × { 𝑋 } ) ) ∘f + ( 𝐺f · ( 𝑉 × { 𝑌 } ) ) ) )