Theorem hvaddcani

Description: Cancellation law for vector addition. (Contributed by NM, 11-Sep-1999) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		hvnegdi.1	⊢ 𝐴 ∈ ℋ
2		hvnegdi.2	⊢ 𝐵 ∈ ℋ
3		hvaddcan.3	⊢ 𝐶 ∈ ℋ
4		oveq1	⊢ ( ( 𝐴 +ℎ 𝐵 ) = ( 𝐴 +ℎ 𝐶 ) → ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( - 1 ·ℎ 𝐴 ) ) = ( ( 𝐴 +ℎ 𝐶 ) +ℎ ( - 1 ·ℎ 𝐴 ) ) )
5		neg1cn	⊢ - 1 ∈ ℂ
6	5 1	hvmulcli	⊢ ( - 1 ·ℎ 𝐴 ) ∈ ℋ
7	1 2 6	hvadd32i	⊢ ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( - 1 ·ℎ 𝐴 ) ) = ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐴 ) ) +ℎ 𝐵 )
8	1	hvnegidi	⊢ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐴 ) ) = 0ℎ
9	8	oveq1i	⊢ ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐴 ) ) +ℎ 𝐵 ) = ( 0ℎ +ℎ 𝐵 )
10	2	hvaddlidi	⊢ ( 0ℎ +ℎ 𝐵 ) = 𝐵
11	7 9 10	3eqtri	⊢ ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( - 1 ·ℎ 𝐴 ) ) = 𝐵
12	1 3 6	hvadd32i	⊢ ( ( 𝐴 +ℎ 𝐶 ) +ℎ ( - 1 ·ℎ 𝐴 ) ) = ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐴 ) ) +ℎ 𝐶 )
13	8	oveq1i	⊢ ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐴 ) ) +ℎ 𝐶 ) = ( 0ℎ +ℎ 𝐶 )
14	3	hvaddlidi	⊢ ( 0ℎ +ℎ 𝐶 ) = 𝐶
15	12 13 14	3eqtri	⊢ ( ( 𝐴 +ℎ 𝐶 ) +ℎ ( - 1 ·ℎ 𝐴 ) ) = 𝐶
16	4 11 15	3eqtr3g	⊢ ( ( 𝐴 +ℎ 𝐵 ) = ( 𝐴 +ℎ 𝐶 ) → 𝐵 = 𝐶 )
17		oveq2	⊢ ( 𝐵 = 𝐶 → ( 𝐴 +ℎ 𝐵 ) = ( 𝐴 +ℎ 𝐶 ) )
18	16 17	impbii	⊢ ( ( 𝐴 +ℎ 𝐵 ) = ( 𝐴 +ℎ 𝐶 ) ↔ 𝐵 = 𝐶 )