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

Metamath Proof Explorer

Theorem cjsub

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

Ref Expression
Assertion cjsub ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 − 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 negcl ⊢ ( 𝐵 ∈ ℂ → - 𝐵 ∈ ℂ )
2 cjadd ⊢ ( ( 𝐴 ∈ ℂ ∧ - 𝐵 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 + - 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) + ( ∗ ‘ - 𝐵 ) ) )
3 1 2 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 + - 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) + ( ∗ ‘ - 𝐵 ) ) )
4 negsub ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + - 𝐵 ) = ( 𝐴 − 𝐵 ) )
5 4 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 + - 𝐵 ) ) = ( ∗ ‘ ( 𝐴 − 𝐵 ) ) )
6 cjneg ⊢ ( 𝐵 ∈ ℂ → ( ∗ ‘ - 𝐵 ) = - ( ∗ ‘ 𝐵 ) )
7 6 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ - 𝐵 ) = - ( ∗ ‘ 𝐵 ) )
8 7 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ∗ ‘ 𝐴 ) + ( ∗ ‘ - 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) + - ( ∗ ‘ 𝐵 ) ) )
9 cjcl ⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) ∈ ℂ )
10 cjcl ⊢ ( 𝐵 ∈ ℂ → ( ∗ ‘ 𝐵 ) ∈ ℂ )
11 negsub ⊢ ( ( ( ∗ ‘ 𝐴 ) ∈ ℂ ∧ ( ∗ ‘ 𝐵 ) ∈ ℂ ) → ( ( ∗ ‘ 𝐴 ) + - ( ∗ ‘ 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐵 ) ) )
12 9 10 11 syl2an ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ∗ ‘ 𝐴 ) + - ( ∗ ‘ 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐵 ) ) )
13 8 12 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ∗ ‘ 𝐴 ) + ( ∗ ‘ - 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐵 ) ) )
14 3 5 13 3eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 − 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐵 ) ) )