This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 · ( 𝑉 × { 𝑌 } ) ) ) )