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