Theorem lflvsdi1

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

	Ref	Expression
Hypotheses	lfldi.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lfldi.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
	lfldi.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	lfldi.p	⊢ + = ( +g ‘ 𝑅 )
	lfldi.t	⊢ · = ( .r ‘ 𝑅 )
	lfldi.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	lfldi.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lfldi.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
	lfldi1.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
	lfldi1.h	⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
Assertion	lflvsdi1	⊢ ( 𝜑 → ( ( 𝐺 ∘f + 𝐻 ) ∘f · ( 𝑉 × { 𝑋 } ) ) = ( ( 𝐺 ∘f · ( 𝑉 × { 𝑋 } ) ) ∘f + ( 𝐻 ∘f · ( 𝑉 × { 𝑋 } ) ) ) )

Proof

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