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