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

Metamath Proof Explorer

Theorem abscj

Description: The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of Gleason p. 133. (Contributed by NM, 28-Apr-2005)

		Ref	Expression
	Assertion	abscj	$⊢ A \in ℂ \to \|\overline{A}\| = \|A\|$

Proof

Step	Hyp	Ref	Expression
1		cjcl	$⊢ A \in ℂ \to \overline{A} \in ℂ$
2		absval	$⊢ \overline{A} \in ℂ \to \|\overline{A}\| = \sqrt{\overline{A} \overline{\overline{A}}}$
3	1 2	syl	$⊢ A \in ℂ \to \|\overline{A}\| = \sqrt{\overline{A} \overline{\overline{A}}}$
4		mulcom	$⊢ (A \in ℂ \land \overline{A} \in ℂ) \to A \overline{A} = \overline{A} A$
5	1 4	mpdan	$⊢ A \in ℂ \to A \overline{A} = \overline{A} A$
6		cjcj	$⊢ A \in ℂ \to \overline{\overline{A}} = A$
7	6	oveq2d	$⊢ A \in ℂ \to \overline{A} \overline{\overline{A}} = \overline{A} A$
8	5 7	eqtr4d	$⊢ A \in ℂ \to A \overline{A} = \overline{A} \overline{\overline{A}}$
9	8	fveq2d	$⊢ A \in ℂ \to \sqrt{A \overline{A}} = \sqrt{\overline{A} \overline{\overline{A}}}$
10	3 9	eqtr4d	$⊢ A \in ℂ \to \|\overline{A}\| = \sqrt{A \overline{A}}$
11		absval	$⊢ A \in ℂ \to \|A\| = \sqrt{A \overline{A}}$
12	10 11	eqtr4d	$⊢ A \in ℂ \to \|\overline{A}\| = \|A\|$