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

Metamath Proof Explorer

Theorem ldualvsass2

Description: Associative law for scalar product operation, using operations from the dual space. (Contributed by NM, 20-Oct-2014)

Ref Expression
Hypotheses ldualvsass2.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
ldualvsass2.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
ldualvsass2.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
ldualvsass2.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
ldualvsass2.q ⊢ 𝑄 = ( Scalar ‘ 𝐷 )
ldualvsass2.t ⊢ × = ( .r ‘ 𝑄 )
ldualvsass2.s ⊢ · = ( ·𝑠 ‘ 𝐷 )
ldualvsass2.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
ldualvsass2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
ldualvsass2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐾 )
ldualvsass2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion ldualvsass2 ( 𝜑 → ( ( 𝑋 × 𝑌 ) · 𝐺 ) = ( 𝑋 · ( 𝑌 · 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 ldualvsass2.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2 ldualvsass2.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
3 ldualvsass2.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
4 ldualvsass2.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
5 ldualvsass2.q ⊢ 𝑄 = ( Scalar ‘ 𝐷 )
6 ldualvsass2.t ⊢ × = ( .r ‘ 𝑄 )
7 ldualvsass2.s ⊢ · = ( ·𝑠 ‘ 𝐷 )
8 ldualvsass2.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
9 ldualvsass2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
10 ldualvsass2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐾 )
11 ldualvsass2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
12 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
13 2 3 12 4 5 6 8 9 10 ldualsmul ⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) = ( 𝑌 ( .r ‘ 𝑅 ) 𝑋 ) )
14 13 oveq1d ⊢ ( 𝜑 → ( ( 𝑋 × 𝑌 ) · 𝐺 ) = ( ( 𝑌 ( .r ‘ 𝑅 ) 𝑋 ) · 𝐺 ) )
15 1 2 3 12 4 7 8 9 10 11 ldualvsass ⊢ ( 𝜑 → ( ( 𝑌 ( .r ‘ 𝑅 ) 𝑋 ) · 𝐺 ) = ( 𝑋 · ( 𝑌 · 𝐺 ) ) )
16 14 15 eqtrd ⊢ ( 𝜑 → ( ( 𝑋 × 𝑌 ) · 𝐺 ) = ( 𝑋 · ( 𝑌 · 𝐺 ) ) )