Metamath Proof Explorer

Theorem hvsubdistr2

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

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

Proof

Step Hyp Ref Expression
1 hvmulcl ⊢ A ∈ ℂ ∧ C ∈ ℋ → A ⋅ ℎ C ∈ ℋ
2 1 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → A ⋅ ℎ C ∈ ℋ
3 hvmulcl ⊢ B ∈ ℂ ∧ C ∈ ℋ → B ⋅ ℎ C ∈ ℋ
4 3 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → B ⋅ ℎ C ∈ ℋ
5 hvsubval ⊢ A ⋅ ℎ C ∈ ℋ ∧ B ⋅ ℎ C ∈ ℋ → A ⋅ ℎ C - ℎ B ⋅ ℎ C = A ⋅ ℎ C + ℎ -1 ⋅ ℎ B ⋅ ℎ C
6 2 4 5 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → A ⋅ ℎ C - ℎ B ⋅ ℎ C = A ⋅ ℎ C + ℎ -1 ⋅ ℎ B ⋅ ℎ C
7 mulm1 ⊢ B ∈ ℂ → -1 ⁢ B = − B
8 7 oveq1d ⊢ B ∈ ℂ → -1 ⁢ B ⋅ ℎ C = − B ⋅ ℎ C
9 8 adantr ⊢ B ∈ ℂ ∧ C ∈ ℋ → -1 ⁢ B ⋅ ℎ C = − B ⋅ ℎ C
10 neg1cn ⊢ − 1 ∈ ℂ
11 ax-hvmulass ⊢ − 1 ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → -1 ⁢ B ⋅ ℎ C = -1 ⋅ ℎ B ⋅ ℎ C
12 10 11 mp3an1 ⊢ B ∈ ℂ ∧ C ∈ ℋ → -1 ⁢ B ⋅ ℎ C = -1 ⋅ ℎ B ⋅ ℎ C
13 9 12 eqtr3d ⊢ B ∈ ℂ ∧ C ∈ ℋ → − B ⋅ ℎ C = -1 ⋅ ℎ B ⋅ ℎ C
14 13 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → − B ⋅ ℎ C = -1 ⋅ ℎ B ⋅ ℎ C
15 14 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → A ⋅ ℎ C + ℎ − B ⋅ ℎ C = A ⋅ ℎ C + ℎ -1 ⋅ ℎ B ⋅ ℎ C
16 negcl ⊢ B ∈ ℂ → − B ∈ ℂ
17 ax-hvdistr2 ⊢ A ∈ ℂ ∧ − B ∈ ℂ ∧ C ∈ ℋ → A + − B ⋅ ℎ C = A ⋅ ℎ C + ℎ − B ⋅ ℎ C
18 16 17 syl3an2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → A + − B ⋅ ℎ C = A ⋅ ℎ C + ℎ − B ⋅ ℎ C
19 negsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B = A − B
20 19 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → A + − B = A − B
21 20 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → A + − B ⋅ ℎ C = A − B ⋅ ℎ C
22 18 21 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → A ⋅ ℎ C + ℎ − B ⋅ ℎ C = A − B ⋅ ℎ C
23 6 15 22 3eqtr2rd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → A − B ⋅ ℎ C = A ⋅ ℎ C - ℎ B ⋅ ℎ C