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

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 ⊢ 𝑉 = ( 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 lflvsdi2 ( 𝜑 → ( 𝐺 ∘f · ( ( 𝑉 × { 𝑋 } ) ∘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 2 3 1 6 lflf ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ 𝐾 )
14 7 10 13 syl2anc ⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ 𝐾 )
15 fconst6g ⊢ ( 𝑋 ∈ 𝐾 → ( 𝑉 × { 𝑋 } ) : 𝑉 ⟶ 𝐾 )
16 8 15 syl ⊢ ( 𝜑 → ( 𝑉 × { 𝑋 } ) : 𝑉 ⟶ 𝐾 )
17 fconst6g ⊢ ( 𝑌 ∈ 𝐾 → ( 𝑉 × { 𝑌 } ) : 𝑉 ⟶ 𝐾 )
18 9 17 syl ⊢ ( 𝜑 → ( 𝑉 × { 𝑌 } ) : 𝑉 ⟶ 𝐾 )
19 2 lmodring ⊢ ( 𝑊 ∈ LMod → 𝑅 ∈ Ring )
20 7 19 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
21 3 4 5 ringdi ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
22 20 21 sylan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
23 12 14 16 18 22 caofdi ⊢ ( 𝜑 → ( 𝐺 ∘f · ( ( 𝑉 × { 𝑋 } ) ∘f + ( 𝑉 × { 𝑌 } ) ) ) = ( ( 𝐺 ∘f · ( 𝑉 × { 𝑋 } ) ) ∘f + ( 𝐺 ∘f · ( 𝑉 × { 𝑌 } ) ) ) )