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

Metamath Proof Explorer

Theorem subsub2

Description: Law for double subtraction. (Contributed by NM, 30-Jun-2005) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 subcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
2 1 3adant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
3 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℂ )
4 simp3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
5 simp2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℂ )
6 subcl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
7 4 5 6 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
8 2 3 7 add12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 − 𝐶 ) + ( 𝐴 + ( 𝐶 − 𝐵 ) ) ) = ( 𝐴 + ( ( 𝐵 − 𝐶 ) + ( 𝐶 − 𝐵 ) ) ) )
9 npncan2 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 − 𝐶 ) + ( 𝐶 − 𝐵 ) ) = 0 )
10 9 3adant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 − 𝐶 ) + ( 𝐶 − 𝐵 ) ) = 0 )
11 10 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 + ( ( 𝐵 − 𝐶 ) + ( 𝐶 − 𝐵 ) ) ) = ( 𝐴 + 0 ) )
12 3 addridd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 + 0 ) = 𝐴 )
13 8 11 12 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 − 𝐶 ) + ( 𝐴 + ( 𝐶 − 𝐵 ) ) ) = 𝐴 )
14 3 7 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 + ( 𝐶 − 𝐵 ) ) ∈ ℂ )
15 subadd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 − 𝐶 ) ∈ ℂ ∧ ( 𝐴 + ( 𝐶 − 𝐵 ) ) ∈ ℂ ) → ( ( 𝐴 − ( 𝐵 − 𝐶 ) ) = ( 𝐴 + ( 𝐶 − 𝐵 ) ) ↔ ( ( 𝐵 − 𝐶 ) + ( 𝐴 + ( 𝐶 − 𝐵 ) ) ) = 𝐴 ) )
16 3 2 14 15 syl3anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − ( 𝐵 − 𝐶 ) ) = ( 𝐴 + ( 𝐶 − 𝐵 ) ) ↔ ( ( 𝐵 − 𝐶 ) + ( 𝐴 + ( 𝐶 − 𝐵 ) ) ) = 𝐴 ) )
17 13 16 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 − ( 𝐵 − 𝐶 ) ) = ( 𝐴 + ( 𝐶 − 𝐵 ) ) )