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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 − 𝐵 ) ·ℎ 𝐶 ) = ( ( 𝐴 ·ℎ 𝐶 ) −ℎ ( 𝐵 ·ℎ 𝐶 ) ) )

Proof

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