Metamath Proof Explorer

Theorem ldualvsdi2

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

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

Proof

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