Theorem ldualvsass

Description: Associative law for scalar product operation. (Contributed by NM, 20-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		ldualvsass.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2		ldualvsass.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
3		ldualvsass.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		ldualvsass.t	⊢ × = ( .r ‘ 𝑅 )
5		ldualvsass.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
6		ldualvsass.s	⊢ · = ( ·𝑠 ‘ 𝐷 )
7		ldualvsass.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
8		ldualvsass.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
9		ldualvsass.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐾 )
10		ldualvsass.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
11		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
12	11 2 3 4 1 7 9 8 10	lflvsass	⊢ ( 𝜑 → ( 𝐺 ∘f × ( ( Base ‘ 𝑊 ) × { ( 𝑌 × 𝑋 ) } ) ) = ( ( 𝐺 ∘f × ( ( Base ‘ 𝑊 ) × { 𝑌 } ) ) ∘f × ( ( Base ‘ 𝑊 ) × { 𝑋 } ) ) )
13	2	lmodring	⊢ ( 𝑊 ∈ LMod → 𝑅 ∈ Ring )
14	7 13	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
15	3 4	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐾 ∧ 𝑋 ∈ 𝐾 ) → ( 𝑌 × 𝑋 ) ∈ 𝐾 )
16	14 9 8 15	syl3anc	⊢ ( 𝜑 → ( 𝑌 × 𝑋 ) ∈ 𝐾 )
17	1 11 2 3 4 5 6 7 16 10	ldualvs	⊢ ( 𝜑 → ( ( 𝑌 × 𝑋 ) · 𝐺 ) = ( 𝐺 ∘f × ( ( Base ‘ 𝑊 ) × { ( 𝑌 × 𝑋 ) } ) ) )
18	11 2 3 4 1 7 10 9	lflvscl	⊢ ( 𝜑 → ( 𝐺 ∘f × ( ( Base ‘ 𝑊 ) × { 𝑌 } ) ) ∈ 𝐹 )
19	1 11 2 3 4 5 6 7 8 18	ldualvs	⊢ ( 𝜑 → ( 𝑋 · ( 𝐺 ∘f × ( ( Base ‘ 𝑊 ) × { 𝑌 } ) ) ) = ( ( 𝐺 ∘f × ( ( Base ‘ 𝑊 ) × { 𝑌 } ) ) ∘f × ( ( Base ‘ 𝑊 ) × { 𝑋 } ) ) )
20	12 17 19	3eqtr4d	⊢ ( 𝜑 → ( ( 𝑌 × 𝑋 ) · 𝐺 ) = ( 𝑋 · ( 𝐺 ∘f × ( ( Base ‘ 𝑊 ) × { 𝑌 } ) ) ) )
21	1 11 2 3 4 5 6 7 9 10	ldualvs	⊢ ( 𝜑 → ( 𝑌 · 𝐺 ) = ( 𝐺 ∘f × ( ( Base ‘ 𝑊 ) × { 𝑌 } ) ) )
22	21	oveq2d	⊢ ( 𝜑 → ( 𝑋 · ( 𝑌 · 𝐺 ) ) = ( 𝑋 · ( 𝐺 ∘f × ( ( Base ‘ 𝑊 ) × { 𝑌 } ) ) ) )
23	20 22	eqtr4d	⊢ ( 𝜑 → ( ( 𝑌 × 𝑋 ) · 𝐺 ) = ( 𝑋 · ( 𝑌 · 𝐺 ) ) )