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

Metamath Proof Explorer

Theorem lflvsass

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

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

Proof

Step Hyp Ref Expression
1 lflass.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lflass.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
3 lflass.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
4 lflass.t ⊢ · = ( .r ‘ 𝑅 )
5 lflass.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
6 lflass.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
7 lflass.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
8 lflass.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐾 )
9 lflass.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
10 1 fvexi ⊢ 𝑉 ∈ V
11 10 a1i ⊢ ( 𝜑 → 𝑉 ∈ V )
12 2 3 1 5 lflf ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ 𝐾 )
13 6 9 12 syl2anc ⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ 𝐾 )
14 fconst6g ⊢ ( 𝑋 ∈ 𝐾 → ( 𝑉 × { 𝑋 } ) : 𝑉 ⟶ 𝐾 )
15 7 14 syl ⊢ ( 𝜑 → ( 𝑉 × { 𝑋 } ) : 𝑉 ⟶ 𝐾 )
16 fconst6g ⊢ ( 𝑌 ∈ 𝐾 → ( 𝑉 × { 𝑌 } ) : 𝑉 ⟶ 𝐾 )
17 8 16 syl ⊢ ( 𝜑 → ( 𝑉 × { 𝑌 } ) : 𝑉 ⟶ 𝐾 )
18 2 lmodring ⊢ ( 𝑊 ∈ LMod → 𝑅 ∈ Ring )
19 6 18 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
20 3 4 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
21 19 20 sylan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
22 11 13 15 17 21 caofass ⊢ ( 𝜑 → ( ( 𝐺 ∘f · ( 𝑉 × { 𝑋 } ) ) ∘f · ( 𝑉 × { 𝑌 } ) ) = ( 𝐺 ∘f · ( ( 𝑉 × { 𝑋 } ) ∘f · ( 𝑉 × { 𝑌 } ) ) ) )
23 11 7 8 ofc12 ⊢ ( 𝜑 → ( ( 𝑉 × { 𝑋 } ) ∘f · ( 𝑉 × { 𝑌 } ) ) = ( 𝑉 × { ( 𝑋 · 𝑌 ) } ) )
24 23 oveq2d ⊢ ( 𝜑 → ( 𝐺 ∘f · ( ( 𝑉 × { 𝑋 } ) ∘f · ( 𝑉 × { 𝑌 } ) ) ) = ( 𝐺 ∘f · ( 𝑉 × { ( 𝑋 · 𝑌 ) } ) ) )
25 22 24 eqtr2d ⊢ ( 𝜑 → ( 𝐺 ∘f · ( 𝑉 × { ( 𝑋 · 𝑌 ) } ) ) = ( ( 𝐺 ∘f · ( 𝑉 × { 𝑋 } ) ) ∘f · ( 𝑉 × { 𝑌 } ) ) )