Theorem ldualvsdi1

Description: Distributive law for scalar product operation, using operations from the dual space. (Contributed by NM, 21-Oct-2014)

	Ref	Expression
Hypotheses	ldualvsdi1.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	ldualvsdi1.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
	ldualvsdi1.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	ldualvsdi1.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
	ldualvsdi1.p	⊢ + = ( +g ‘ 𝐷 )
	ldualvsdi1.s	⊢ · = ( ·𝑠 ‘ 𝐷 )
	ldualvsdi1.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	ldualvsdi1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
	ldualvsdi1.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
	ldualvsdi1.h	⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
Assertion	ldualvsdi1	⊢ ( 𝜑 → ( 𝑋 · ( 𝐺 + 𝐻 ) ) = ( ( 𝑋 · 𝐺 ) + ( 𝑋 · 𝐻 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ldualvsdi1.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2		ldualvsdi1.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
3		ldualvsdi1.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		ldualvsdi1.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
5		ldualvsdi1.p	⊢ + = ( +g ‘ 𝐷 )
6		ldualvsdi1.s	⊢ · = ( ·𝑠 ‘ 𝐷 )
7		ldualvsdi1.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
8		ldualvsdi1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
9		ldualvsdi1.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
10		ldualvsdi1.h	⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
11		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
12		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
13	1 11 2 3 12 4 6 7 8 9	ldualvs	⊢ ( 𝜑 → ( 𝑋 · 𝐺 ) = ( 𝐺 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑋 } ) ) )
14	1 11 2 3 12 4 6 7 8 10	ldualvs	⊢ ( 𝜑 → ( 𝑋 · 𝐻 ) = ( 𝐻 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑋 } ) ) )
15	13 14	oveq12d	⊢ ( 𝜑 → ( ( 𝑋 · 𝐺 ) ∘f ( +g ‘ 𝑅 ) ( 𝑋 · 𝐻 ) ) = ( ( 𝐺 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑋 } ) ) ∘f ( +g ‘ 𝑅 ) ( 𝐻 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑋 } ) ) ) )
16		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
17	1 2 3 4 6 7 8 9	ldualvscl	⊢ ( 𝜑 → ( 𝑋 · 𝐺 ) ∈ 𝐹 )
18	1 2 3 4 6 7 8 10	ldualvscl	⊢ ( 𝜑 → ( 𝑋 · 𝐻 ) ∈ 𝐹 )
19	1 2 16 4 5 7 17 18	ldualvadd	⊢ ( 𝜑 → ( ( 𝑋 · 𝐺 ) + ( 𝑋 · 𝐻 ) ) = ( ( 𝑋 · 𝐺 ) ∘f ( +g ‘ 𝑅 ) ( 𝑋 · 𝐻 ) ) )
20	1 4 5 7 9 10	ldualvaddcl	⊢ ( 𝜑 → ( 𝐺 + 𝐻 ) ∈ 𝐹 )
21	1 11 2 3 12 4 6 7 8 20	ldualvs	⊢ ( 𝜑 → ( 𝑋 · ( 𝐺 + 𝐻 ) ) = ( ( 𝐺 + 𝐻 ) ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑋 } ) ) )
22	1 2 16 4 5 7 9 10	ldualvadd	⊢ ( 𝜑 → ( 𝐺 + 𝐻 ) = ( 𝐺 ∘f ( +g ‘ 𝑅 ) 𝐻 ) )
23	22	oveq1d	⊢ ( 𝜑 → ( ( 𝐺 + 𝐻 ) ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑋 } ) ) = ( ( 𝐺 ∘f ( +g ‘ 𝑅 ) 𝐻 ) ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑋 } ) ) )
24	11 2 3 16 12 1 7 8 9 10	lflvsdi1	⊢ ( 𝜑 → ( ( 𝐺 ∘f ( +g ‘ 𝑅 ) 𝐻 ) ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑋 } ) ) = ( ( 𝐺 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑋 } ) ) ∘f ( +g ‘ 𝑅 ) ( 𝐻 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑋 } ) ) ) )
25	21 23 24	3eqtrd	⊢ ( 𝜑 → ( 𝑋 · ( 𝐺 + 𝐻 ) ) = ( ( 𝐺 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑋 } ) ) ∘f ( +g ‘ 𝑅 ) ( 𝐻 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑋 } ) ) ) )
26	15 19 25	3eqtr4rd	⊢ ( 𝜑 → ( 𝑋 · ( 𝐺 + 𝐻 ) ) = ( ( 𝑋 · 𝐺 ) + ( 𝑋 · 𝐻 ) ) )