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

Metamath Proof Explorer

Theorem hvsubadd

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

		Ref	Expression
	Assertion	hvsubadd	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 −_ℎ 𝐵 ) = 𝐶 ↔ ( 𝐵 +_ℎ 𝐶 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → ( 𝐴 −_ℎ 𝐵 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) −_ℎ 𝐵 ) )
2	1	eqeq1d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → ( ( 𝐴 −_ℎ 𝐵 ) = 𝐶 ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) −_ℎ 𝐵 ) = 𝐶 ) )
3		eqeq2	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → ( ( 𝐵 +_ℎ 𝐶 ) = 𝐴 ↔ ( 𝐵 +_ℎ 𝐶 ) = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) )
4	2 3	bibi12d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → ( ( ( 𝐴 −_ℎ 𝐵 ) = 𝐶 ↔ ( 𝐵 +_ℎ 𝐶 ) = 𝐴 ) ↔ ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) −_ℎ 𝐵 ) = 𝐶 ↔ ( 𝐵 +_ℎ 𝐶 ) = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) )
5		oveq2	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) → ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) −_ℎ 𝐵 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) −_ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) )
6	5	eqeq1d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) → ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) −_ℎ 𝐵 ) = 𝐶 ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) −_ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) = 𝐶 ) )
7		oveq1	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) → ( 𝐵 +_ℎ 𝐶 ) = ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) +_ℎ 𝐶 ) )
8	7	eqeq1d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) → ( ( 𝐵 +_ℎ 𝐶 ) = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ↔ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) +_ℎ 𝐶 ) = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) )
9	6 8	bibi12d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) → ( ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) −_ℎ 𝐵 ) = 𝐶 ↔ ( 𝐵 +_ℎ 𝐶 ) = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ↔ ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) −_ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) = 𝐶 ↔ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) +_ℎ 𝐶 ) = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) )
10		eqeq2	⊢ ( 𝐶 = if ( 𝐶 ∈ ℋ , 𝐶 , 0_ℎ ) → ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) −_ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) = 𝐶 ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) −_ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) = if ( 𝐶 ∈ ℋ , 𝐶 , 0_ℎ ) ) )
11		oveq2	⊢ ( 𝐶 = if ( 𝐶 ∈ ℋ , 𝐶 , 0_ℎ ) → ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) +_ℎ 𝐶 ) = ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) +_ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0_ℎ ) ) )
12	11	eqeq1d	⊢ ( 𝐶 = if ( 𝐶 ∈ ℋ , 𝐶 , 0_ℎ ) → ( ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) +_ℎ 𝐶 ) = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ↔ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) +_ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0_ℎ ) ) = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) )
13	10 12	bibi12d	⊢ ( 𝐶 = if ( 𝐶 ∈ ℋ , 𝐶 , 0_ℎ ) → ( ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) −_ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) = 𝐶 ↔ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) +_ℎ 𝐶 ) = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ↔ ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) −_ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) = if ( 𝐶 ∈ ℋ , 𝐶 , 0_ℎ ) ↔ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) +_ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0_ℎ ) ) = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) ) )
14		ifhvhv0	⊢ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ∈ ℋ
15		ifhvhv0	⊢ if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ∈ ℋ
16		ifhvhv0	⊢ if ( 𝐶 ∈ ℋ , 𝐶 , 0_ℎ ) ∈ ℋ
17	14 15 16	hvsubaddi	⊢ ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) −_ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) = if ( 𝐶 ∈ ℋ , 𝐶 , 0_ℎ ) ↔ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) +_ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0_ℎ ) ) = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) )
18	4 9 13 17	dedth3h	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 −_ℎ 𝐵 ) = 𝐶 ↔ ( 𝐵 +_ℎ 𝐶 ) = 𝐴 ) )