This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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