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	⊢ ( 𝜑 → ( ( 𝑋 × 𝑌 ) · 𝐺 ) = ( 𝑋 · ( 𝑌 · 𝐺 ) ) )