cjsub

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

		Ref	Expression
	Assertion	cjsub	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{A - B} = \overline{A} - \overline{B}$

Step	Hyp	Ref	Expression
1		negcl	$⊢ B \in ℂ \to - B \in ℂ$
2		cjadd	$⊢ (A \in ℂ \land - B \in ℂ) \to \overline{A + (- B)} = \overline{A} + \overline{- B}$
3	1 2	sylan2	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{A + (- B)} = \overline{A} + \overline{- B}$
4		negsub	$⊢ (A \in ℂ \land B \in ℂ) \to A + (- B) = A - B$
5	4	fveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{A + (- B)} = \overline{A - B}$
6		cjneg	$⊢ B \in ℂ \to \overline{- B} = - \overline{B}$
7	6	adantl	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{- B} = - \overline{B}$
8	7	oveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{A} + \overline{- B} = \overline{A} + (- \overline{B})$
9		cjcl	$⊢ A \in ℂ \to \overline{A} \in ℂ$
10		cjcl	$⊢ B \in ℂ \to \overline{B} \in ℂ$
11		negsub	$⊢ (\overline{A} \in ℂ \land \overline{B} \in ℂ) \to \overline{A} + (- \overline{B}) = \overline{A} - \overline{B}$
12	9 10 11	syl2an	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{A} + (- \overline{B}) = \overline{A} - \overline{B}$
13	8 12	eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{A} + \overline{- B} = \overline{A} - \overline{B}$
14	3 5 13	3eqtr3d	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{A - B} = \overline{A} - \overline{B}$

Metamath Proof Explorer