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

Metamath Proof Explorer

Theorem fsumcj

Description: The complex conjugate of a sum. (Contributed by Paul Chapman, 9-Nov-2007) (Revised by Mario Carneiro, 25-Jul-2014)

	Ref	Expression
Hypotheses	fsumre.1	$⊢ φ \to A \in Fin$
	fsumre.2	$⊢ (φ \land k \in A) \to B \in ℂ$
Assertion	fsumcj	$⊢ φ \to \overline{\sum_{k \in A} B} = \sum_{k \in A} \overline{B}$

Step	Hyp	Ref	Expression
1		fsumre.1	$⊢ φ \to A \in Fin$
2		fsumre.2	$⊢ (φ \land k \in A) \to B \in ℂ$
3		cjf	$⊢ * : ℂ ⟶ ℂ$
4		cjadd	$⊢ (x \in ℂ \land y \in ℂ) \to \overline{x + y} = \overline{x} + \overline{y}$
5	1 2 3 4	fsumrelem	$⊢ φ \to \overline{\sum_{k \in A} B} = \sum_{k \in A} \overline{B}$