Theorem hvnegdii

Description: Distribution of negative over subtraction. (Contributed by NM, 31-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hvnegdi.1	⊢ 𝐴 ∈ ℋ
	hvnegdi.2	⊢ 𝐵 ∈ ℋ
Assertion	hvnegdii	⊢ ( - 1 ·ℎ ( 𝐴 −ℎ 𝐵 ) ) = ( 𝐵 −ℎ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		hvnegdi.1	⊢ 𝐴 ∈ ℋ
2		hvnegdi.2	⊢ 𝐵 ∈ ℋ
3	1 2	hvsubvali	⊢ ( 𝐴 −ℎ 𝐵 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) )
4	3	oveq2i	⊢ ( - 1 ·ℎ ( 𝐴 −ℎ 𝐵 ) ) = ( - 1 ·ℎ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) )
5		neg1cn	⊢ - 1 ∈ ℂ
6	5 2	hvmulcli	⊢ ( - 1 ·ℎ 𝐵 ) ∈ ℋ
7	5 1 6	hvdistr1i	⊢ ( - 1 ·ℎ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( ( - 1 ·ℎ 𝐴 ) +ℎ ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) )
8		neg1mulneg1e1	⊢ ( - 1 · - 1 ) = 1
9	8	oveq1i	⊢ ( ( - 1 · - 1 ) ·ℎ 𝐵 ) = ( 1 ·ℎ 𝐵 )
10	5 5 2	hvmulassi	⊢ ( ( - 1 · - 1 ) ·ℎ 𝐵 ) = ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) )
11		ax-hvmulid	⊢ ( 𝐵 ∈ ℋ → ( 1 ·ℎ 𝐵 ) = 𝐵 )
12	2 11	ax-mp	⊢ ( 1 ·ℎ 𝐵 ) = 𝐵
13	9 10 12	3eqtr3i	⊢ ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) = 𝐵
14	13	oveq1i	⊢ ( ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) +ℎ ( - 1 ·ℎ 𝐴 ) ) = ( 𝐵 +ℎ ( - 1 ·ℎ 𝐴 ) )
15	5 1	hvmulcli	⊢ ( - 1 ·ℎ 𝐴 ) ∈ ℋ
16	5 6	hvmulcli	⊢ ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) ∈ ℋ
17	15 16	hvcomi	⊢ ( ( - 1 ·ℎ 𝐴 ) +ℎ ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) +ℎ ( - 1 ·ℎ 𝐴 ) )
18	2 1	hvsubvali	⊢ ( 𝐵 −ℎ 𝐴 ) = ( 𝐵 +ℎ ( - 1 ·ℎ 𝐴 ) )
19	14 17 18	3eqtr4i	⊢ ( ( - 1 ·ℎ 𝐴 ) +ℎ ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( 𝐵 −ℎ 𝐴 )
20	4 7 19	3eqtri	⊢ ( - 1 ·ℎ ( 𝐴 −ℎ 𝐵 ) ) = ( 𝐵 −ℎ 𝐴 )