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