Theorem lflvsdi2a

Description: Reverse distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 21-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	lflvsdi2a	⊢ ( 𝜑 → ( 𝐺 ∘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	12 8 9	ofc12	⊢ ( 𝜑 → ( ( 𝑉 × { 𝑋 } ) ∘f + ( 𝑉 × { 𝑌 } ) ) = ( 𝑉 × { ( 𝑋 + 𝑌 ) } ) )
14	13	oveq2d	⊢ ( 𝜑 → ( 𝐺 ∘f · ( ( 𝑉 × { 𝑋 } ) ∘f + ( 𝑉 × { 𝑌 } ) ) ) = ( 𝐺 ∘f · ( 𝑉 × { ( 𝑋 + 𝑌 ) } ) ) )
15	1 2 3 4 5 6 7 8 9 10	lflvsdi2	⊢ ( 𝜑 → ( 𝐺 ∘f · ( ( 𝑉 × { 𝑋 } ) ∘f + ( 𝑉 × { 𝑌 } ) ) ) = ( ( 𝐺 ∘f · ( 𝑉 × { 𝑋 } ) ) ∘f + ( 𝐺 ∘f · ( 𝑉 × { 𝑌 } ) ) ) )
16	14 15	eqtr3d	⊢ ( 𝜑 → ( 𝐺 ∘f · ( 𝑉 × { ( 𝑋 + 𝑌 ) } ) ) = ( ( 𝐺 ∘f · ( 𝑉 × { 𝑋 } ) ) ∘f + ( 𝐺 ∘f · ( 𝑉 × { 𝑌 } ) ) ) )