This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑋 · ( 𝐺 + 𝐻 ) ) = ( ( 𝑋 · 𝐺 ) + ( 𝑋 · 𝐻 ) ) )