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

Metamath Proof Explorer

Theorem ldualsmul

Description: Scalar multiplication for the dual of a vector space. (Contributed by NM, 19-Oct-2014) (Revised by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses ldualsmul.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
ldualsmul.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
ldualsmul.t ⊢ · = ( .r ‘ 𝐹 )
ldualsmul.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
ldualsmul.r ⊢ 𝑅 = ( Scalar ‘ 𝐷 )
ldualsmul.m ⊢ ∙ = ( .r ‘ 𝑅 )
ldualsmul.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
ldualsmul.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
ldualsmul.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐾 )
Assertion ldualsmul ( 𝜑 → ( 𝑋 ∙ 𝑌 ) = ( 𝑌 · 𝑋 ) )

Proof

Step Hyp Ref Expression
1 ldualsmul.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 ldualsmul.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
3 ldualsmul.t ⊢ · = ( .r ‘ 𝐹 )
4 ldualsmul.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
5 ldualsmul.r ⊢ 𝑅 = ( Scalar ‘ 𝐷 )
6 ldualsmul.m ⊢ ∙ = ( .r ‘ 𝑅 )
7 ldualsmul.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
8 ldualsmul.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
9 ldualsmul.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐾 )
10 eqid ⊢ ( oppr ‘ 𝐹 ) = ( oppr ‘ 𝐹 )
11 1 10 4 5 7 ldualsca ⊢ ( 𝜑 → 𝑅 = ( oppr ‘ 𝐹 ) )
12 11 fveq2d ⊢ ( 𝜑 → ( .r ‘ 𝑅 ) = ( .r ‘ ( oppr ‘ 𝐹 ) ) )
13 6 12 eqtrid ⊢ ( 𝜑 → ∙ = ( .r ‘ ( oppr ‘ 𝐹 ) ) )
14 13 oveqd ⊢ ( 𝜑 → ( 𝑋 ∙ 𝑌 ) = ( 𝑋 ( .r ‘ ( oppr ‘ 𝐹 ) ) 𝑌 ) )
15 eqid ⊢ ( .r ‘ ( oppr ‘ 𝐹 ) ) = ( .r ‘ ( oppr ‘ 𝐹 ) )
16 2 3 10 15 opprmul ⊢ ( 𝑋 ( .r ‘ ( oppr ‘ 𝐹 ) ) 𝑌 ) = ( 𝑌 · 𝑋 )
17 14 16 eqtrdi ⊢ ( 𝜑 → ( 𝑋 ∙ 𝑌 ) = ( 𝑌 · 𝑋 ) )