Theorem lflvsdi2

Description: Reverse 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	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
	lfldi2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐾 )
	lfldi2.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion	lflvsdi2	⊢ ( 𝜑 → ( 𝐺 ∘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		lfldi2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐾 )
10		lfldi2.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
11	1	fvexi	⊢ 𝑉 ∈ V
12	11	a1i	⊢ ( 𝜑 → 𝑉 ∈ V )
13	2 3 1 6	lflf	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ 𝐾 )
14	7 10 13	syl2anc	⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ 𝐾 )
15		fconst6g	⊢ ( 𝑋 ∈ 𝐾 → ( 𝑉 × { 𝑋 } ) : 𝑉 ⟶ 𝐾 )
16	8 15	syl	⊢ ( 𝜑 → ( 𝑉 × { 𝑋 } ) : 𝑉 ⟶ 𝐾 )
17		fconst6g	⊢ ( 𝑌 ∈ 𝐾 → ( 𝑉 × { 𝑌 } ) : 𝑉 ⟶ 𝐾 )
18	9 17	syl	⊢ ( 𝜑 → ( 𝑉 × { 𝑌 } ) : 𝑉 ⟶ 𝐾 )
19	2	lmodring	⊢ ( 𝑊 ∈ LMod → 𝑅 ∈ Ring )
20	7 19	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
21	3 4 5	ringdi	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
22	20 21	sylan	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
23	12 14 16 18 22	caofdi	⊢ ( 𝜑 → ( 𝐺 ∘f · ( ( 𝑉 × { 𝑋 } ) ∘f + ( 𝑉 × { 𝑌 } ) ) ) = ( ( 𝐺 ∘f · ( 𝑉 × { 𝑋 } ) ) ∘f + ( 𝐺 ∘f · ( 𝑉 × { 𝑌 } ) ) ) )