Theorem hvsubaddi

Description: Relationship between vector subtraction and addition. (Contributed by NM, 11-Sep-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hvnegdi.1	⊢ 𝐴 ∈ ℋ
	hvnegdi.2	⊢ 𝐵 ∈ ℋ
	hvaddcan.3	⊢ 𝐶 ∈ ℋ
Assertion	hvsubaddi	⊢ ( ( 𝐴 −ℎ 𝐵 ) = 𝐶 ↔ ( 𝐵 +ℎ 𝐶 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		hvnegdi.1	⊢ 𝐴 ∈ ℋ
2		hvnegdi.2	⊢ 𝐵 ∈ ℋ
3		hvaddcan.3	⊢ 𝐶 ∈ ℋ
4	1 2	hvsubvali	⊢ ( 𝐴 −ℎ 𝐵 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) )
5	4	eqeq1i	⊢ ( ( 𝐴 −ℎ 𝐵 ) = 𝐶 ↔ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) = 𝐶 )
6		neg1cn	⊢ - 1 ∈ ℂ
7	6 2	hvmulcli	⊢ ( - 1 ·ℎ 𝐵 ) ∈ ℋ
8	2 1 7	hvadd12i	⊢ ( 𝐵 +ℎ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( 𝐴 +ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) )
9	2	hvnegidi	⊢ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) = 0ℎ
10	9	oveq2i	⊢ ( 𝐴 +ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( 𝐴 +ℎ 0ℎ )
11		ax-hvaddid	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 +ℎ 0ℎ ) = 𝐴 )
12	1 11	ax-mp	⊢ ( 𝐴 +ℎ 0ℎ ) = 𝐴
13	8 10 12	3eqtri	⊢ ( 𝐵 +ℎ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = 𝐴
14	13	eqeq1i	⊢ ( ( 𝐵 +ℎ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( 𝐵 +ℎ 𝐶 ) ↔ 𝐴 = ( 𝐵 +ℎ 𝐶 ) )
15	1 7	hvaddcli	⊢ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ∈ ℋ
16	2 15 3	hvaddcani	⊢ ( ( 𝐵 +ℎ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( 𝐵 +ℎ 𝐶 ) ↔ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) = 𝐶 )
17		eqcom	⊢ ( 𝐴 = ( 𝐵 +ℎ 𝐶 ) ↔ ( 𝐵 +ℎ 𝐶 ) = 𝐴 )
18	14 16 17	3bitr3i	⊢ ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) = 𝐶 ↔ ( 𝐵 +ℎ 𝐶 ) = 𝐴 )
19	5 18	bitri	⊢ ( ( 𝐴 −ℎ 𝐵 ) = 𝐶 ↔ ( 𝐵 +ℎ 𝐶 ) = 𝐴 )