Metamath Proof Explorer

Theorem hvsubdistr1

Description: Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005) (New usage is discouraged.)

Ref Expression
Assertion hvsubdistr1 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ B - ℎ C = A ⋅ ℎ B - ℎ A ⋅ ℎ C

Proof

Step Hyp Ref Expression
1 neg1cn ⊢ − 1 ∈ ℂ
2 hvmulcl ⊢ − 1 ∈ ℂ ∧ C ∈ ℋ → -1 ⋅ ℎ C ∈ ℋ
3 1 2 mpan ⊢ C ∈ ℋ → -1 ⋅ ℎ C ∈ ℋ
4 ax-hvdistr1 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ -1 ⋅ ℎ C ∈ ℋ → A ⋅ ℎ B + ℎ -1 ⋅ ℎ C = A ⋅ ℎ B + ℎ A ⋅ ℎ -1 ⋅ ℎ C
5 3 4 syl3an3 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ B + ℎ -1 ⋅ ℎ C = A ⋅ ℎ B + ℎ A ⋅ ℎ -1 ⋅ ℎ C
6 hvmulcom ⊢ A ∈ ℂ ∧ − 1 ∈ ℂ ∧ C ∈ ℋ → A ⋅ ℎ -1 ⋅ ℎ C = -1 ⋅ ℎ A ⋅ ℎ C
7 1 6 mp3an2 ⊢ A ∈ ℂ ∧ C ∈ ℋ → A ⋅ ℎ -1 ⋅ ℎ C = -1 ⋅ ℎ A ⋅ ℎ C
8 7 oveq2d ⊢ A ∈ ℂ ∧ C ∈ ℋ → A ⋅ ℎ B + ℎ A ⋅ ℎ -1 ⋅ ℎ C = A ⋅ ℎ B + ℎ -1 ⋅ ℎ A ⋅ ℎ C
9 8 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ B + ℎ A ⋅ ℎ -1 ⋅ ℎ C = A ⋅ ℎ B + ℎ -1 ⋅ ℎ A ⋅ ℎ C
10 5 9 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ B + ℎ -1 ⋅ ℎ C = A ⋅ ℎ B + ℎ -1 ⋅ ℎ A ⋅ ℎ C
11 hvsubval ⊢ B ∈ ℋ ∧ C ∈ ℋ → B - ℎ C = B + ℎ -1 ⋅ ℎ C
12 11 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → B - ℎ C = B + ℎ -1 ⋅ ℎ C
13 12 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ B - ℎ C = A ⋅ ℎ B + ℎ -1 ⋅ ℎ C
14 hvmulcl ⊢ A ∈ ℂ ∧ B ∈ ℋ → A ⋅ ℎ B ∈ ℋ
15 14 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ B ∈ ℋ
16 hvmulcl ⊢ A ∈ ℂ ∧ C ∈ ℋ → A ⋅ ℎ C ∈ ℋ
17 16 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ C ∈ ℋ
18 hvsubval ⊢ A ⋅ ℎ B ∈ ℋ ∧ A ⋅ ℎ C ∈ ℋ → A ⋅ ℎ B - ℎ A ⋅ ℎ C = A ⋅ ℎ B + ℎ -1 ⋅ ℎ A ⋅ ℎ C
19 15 17 18 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ B - ℎ A ⋅ ℎ C = A ⋅ ℎ B + ℎ -1 ⋅ ℎ A ⋅ ℎ C
20 10 13 19 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ B - ℎ C = A ⋅ ℎ B - ℎ A ⋅ ℎ C