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	syl5eq	⊢ ( 𝜑 → ∙ = ( .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	⊢ ( 𝜑 → ( 𝑋 ∙ 𝑌 ) = ( 𝑌 · 𝑋 ) )