Metamath Proof Explorer

Theorem cjsub

Description: Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005)

Ref Expression
Assertion cjsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ‾ = A ‾ − B ‾

Proof

Step Hyp Ref Expression
1 negcl ⊢ B ∈ ℂ → − B ∈ ℂ
2 cjadd ⊢ A ∈ ℂ ∧ − B ∈ ℂ → A + − B ‾ = A ‾ + − B ‾
3 1 2 sylan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B ‾ = A ‾ + − B ‾
4 negsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B = A − B
5 4 fveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B ‾ = A − B ‾
6 cjneg ⊢ B ∈ ℂ → − B ‾ = − B ‾
7 6 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ → − B ‾ = − B ‾
8 7 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ‾ + − B ‾ = A ‾ + − B ‾
9 cjcl ⊢ A ∈ ℂ → A ‾ ∈ ℂ
10 cjcl ⊢ B ∈ ℂ → B ‾ ∈ ℂ
11 negsub ⊢ A ‾ ∈ ℂ ∧ B ‾ ∈ ℂ → A ‾ + − B ‾ = A ‾ − B ‾
12 9 10 11 syl2an ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ‾ + − B ‾ = A ‾ − B ‾
13 8 12 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ‾ + − B ‾ = A ‾ − B ‾
14 3 5 13 3eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ‾ = A ‾ − B ‾