Theorem lflvsass

Description: Associative law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014)

	Ref	Expression
Hypotheses	lflass.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lflass.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
	lflass.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	lflass.t	⊢ · = ( .r ‘ 𝑅 )
	lflass.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	lflass.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lflass.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
	lflass.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐾 )
	lflass.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion	lflvsass	⊢ ( 𝜑 → ( 𝐺 ∘f · ( 𝑉 × { ( 𝑋 · 𝑌 ) } ) ) = ( ( 𝐺 ∘f · ( 𝑉 × { 𝑋 } ) ) ∘f · ( 𝑉 × { 𝑌 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		lflass.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lflass.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
3		lflass.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		lflass.t	⊢ · = ( .r ‘ 𝑅 )
5		lflass.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
6		lflass.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
7		lflass.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
8		lflass.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐾 )
9		lflass.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
10	1	fvexi	⊢ 𝑉 ∈ V
11	10	a1i	⊢ ( 𝜑 → 𝑉 ∈ V )
12	2 3 1 5	lflf	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ 𝐾 )
13	6 9 12	syl2anc	⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ 𝐾 )
14		fconst6g	⊢ ( 𝑋 ∈ 𝐾 → ( 𝑉 × { 𝑋 } ) : 𝑉 ⟶ 𝐾 )
15	7 14	syl	⊢ ( 𝜑 → ( 𝑉 × { 𝑋 } ) : 𝑉 ⟶ 𝐾 )
16		fconst6g	⊢ ( 𝑌 ∈ 𝐾 → ( 𝑉 × { 𝑌 } ) : 𝑉 ⟶ 𝐾 )
17	8 16	syl	⊢ ( 𝜑 → ( 𝑉 × { 𝑌 } ) : 𝑉 ⟶ 𝐾 )
18	2	lmodring	⊢ ( 𝑊 ∈ LMod → 𝑅 ∈ Ring )
19	6 18	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
20	3 4	ringass	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
21	19 20	sylan	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
22	11 13 15 17 21	caofass	⊢ ( 𝜑 → ( ( 𝐺 ∘f · ( 𝑉 × { 𝑋 } ) ) ∘f · ( 𝑉 × { 𝑌 } ) ) = ( 𝐺 ∘f · ( ( 𝑉 × { 𝑋 } ) ∘f · ( 𝑉 × { 𝑌 } ) ) ) )
23	11 7 8	ofc12	⊢ ( 𝜑 → ( ( 𝑉 × { 𝑋 } ) ∘f · ( 𝑉 × { 𝑌 } ) ) = ( 𝑉 × { ( 𝑋 · 𝑌 ) } ) )
24	23	oveq2d	⊢ ( 𝜑 → ( 𝐺 ∘f · ( ( 𝑉 × { 𝑋 } ) ∘f · ( 𝑉 × { 𝑌 } ) ) ) = ( 𝐺 ∘f · ( 𝑉 × { ( 𝑋 · 𝑌 ) } ) ) )
25	22 24	eqtr2d	⊢ ( 𝜑 → ( 𝐺 ∘f · ( 𝑉 × { ( 𝑋 · 𝑌 ) } ) ) = ( ( 𝐺 ∘f · ( 𝑉 × { 𝑋 } ) ) ∘f · ( 𝑉 × { 𝑌 } ) ) )