Metamath Proof Explorer

Theorem clmsubdir

Description: Scalar multiplication distributive law for subtraction. ( lmodsubdir analog.) (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses clmsubdir.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
clmsubdir.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
clmsubdir.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
clmsubdir.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
clmsubdir.m ⊢ − = ( -g ‘ 𝑊 )
clmsubdir.w ⊢ ( 𝜑 → 𝑊 ∈ ℂMod )
clmsubdir.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
clmsubdir.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
clmsubdir.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion clmsubdir ( 𝜑 → ( ( 𝐴 − 𝐵 ) · 𝑋 ) = ( ( 𝐴 · 𝑋 ) − ( 𝐵 · 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 clmsubdir.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 clmsubdir.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
3 clmsubdir.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 clmsubdir.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
5 clmsubdir.m ⊢ − = ( -g ‘ 𝑊 )
6 clmsubdir.w ⊢ ( 𝜑 → 𝑊 ∈ ℂMod )
7 clmsubdir.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
8 clmsubdir.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
9 clmsubdir.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10 3 4 clmsub ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) )
11 6 7 8 10 syl3anc ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) )
12 11 oveq1d ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) · 𝑋 ) = ( ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) · 𝑋 ) )
13 eqid ⊢ ( -g ‘ 𝐹 ) = ( -g ‘ 𝐹 )
14 clmlmod ⊢ ( 𝑊 ∈ ℂMod → 𝑊 ∈ LMod )
15 6 14 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
16 1 2 3 4 5 13 15 7 8 9 lmodsubdir ⊢ ( 𝜑 → ( ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) · 𝑋 ) = ( ( 𝐴 · 𝑋 ) − ( 𝐵 · 𝑋 ) ) )
17 12 16 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) · 𝑋 ) = ( ( 𝐴 · 𝑋 ) − ( 𝐵 · 𝑋 ) ) )