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

Metamath Proof Explorer

Theorem cnambpcma

Description: ((a-b)+c)-a = c-a holds for complex numbers a,b,c. (Contributed by Alexander van der Vekens, 23-Mar-2018)

Ref Expression
Assertion cnambpcma ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 − 𝐵 ) + 𝐶 ) − 𝐴 ) = ( 𝐶 − 𝐵 ) )

Proof

Step Hyp Ref Expression
1 subcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
2 1 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
3 simp3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
4 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℂ )
5 2 3 4 addsubd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 − 𝐵 ) + 𝐶 ) − 𝐴 ) = ( ( ( 𝐴 − 𝐵 ) − 𝐴 ) + 𝐶 ) )
6 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
7 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
8 6 7 6 3jca ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
9 8 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
10 sub32 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) − 𝐴 ) = ( ( 𝐴 − 𝐴 ) − 𝐵 ) )
11 9 10 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) − 𝐴 ) = ( ( 𝐴 − 𝐴 ) − 𝐵 ) )
12 11 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 − 𝐵 ) − 𝐴 ) + 𝐶 ) = ( ( ( 𝐴 − 𝐴 ) − 𝐵 ) + 𝐶 ) )
13 subcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝐴 − 𝐴 ) ∈ ℂ )
14 13 anidms ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − 𝐴 ) ∈ ℂ )
15 14 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 − 𝐴 ) ∈ ℂ )
16 simp2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℂ )
17 15 16 3 subadd23d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 − 𝐴 ) − 𝐵 ) + 𝐶 ) = ( ( 𝐴 − 𝐴 ) + ( 𝐶 − 𝐵 ) ) )
18 subid ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − 𝐴 ) = 0 )
19 18 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 − 𝐴 ) + ( 𝐶 − 𝐵 ) ) = ( 0 + ( 𝐶 − 𝐵 ) ) )
20 19 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐴 ) + ( 𝐶 − 𝐵 ) ) = ( 0 + ( 𝐶 − 𝐵 ) ) )
21 subcl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
22 21 ancoms ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
23 22 addlidd ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 0 + ( 𝐶 − 𝐵 ) ) = ( 𝐶 − 𝐵 ) )
24 23 3adant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 0 + ( 𝐶 − 𝐵 ) ) = ( 𝐶 − 𝐵 ) )
25 17 20 24 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 − 𝐴 ) − 𝐵 ) + 𝐶 ) = ( 𝐶 − 𝐵 ) )
26 5 12 25 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 − 𝐵 ) + 𝐶 ) − 𝐴 ) = ( 𝐶 − 𝐵 ) )