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

Metamath Proof Explorer

Theorem nmsq

Description: The square of the norm is the norm of an inner product in a subcomplex pre-Hilbert space. Equation I4 of Ponnusamy p. 362. (Contributed by NM, 1-Feb-2007) (Revised by Mario Carneiro, 7-Oct-2015)

		Ref	Expression
	Hypotheses	nmsq.v	$⊢ V = {Base}_{W}$
		nmsq.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
		nmsq.n	$⊢ N = norm (W)$
	Assertion	nmsq	$⊢ (W \in CPreHil \land A \in V) \to {N (A)}^{2} = A \underset{˙}{,} A$

Proof

Step	Hyp	Ref	Expression
1		nmsq.v	$⊢ V = {Base}_{W}$
2		nmsq.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
3		nmsq.n	$⊢ N = norm (W)$
4	1 2 3	cphnm	$⊢ (W \in CPreHil \land A \in V) \to N (A) = \sqrt{A \underset{˙}{,} A}$
5	4	oveq1d	$⊢ (W \in CPreHil \land A \in V) \to {N (A)}^{2} = {\sqrt{A \underset{˙}{,} A}}^{2}$
6	1 2	cphipcl	$⊢ (W \in CPreHil \land A \in V \land A \in V) \to A \underset{˙}{,} A \in ℂ$
7	6	3anidm23	$⊢ (W \in CPreHil \land A \in V) \to A \underset{˙}{,} A \in ℂ$
8	7	sqsqrtd	$⊢ (W \in CPreHil \land A \in V) \to {\sqrt{A \underset{˙}{,} A}}^{2} = A \underset{˙}{,} A$
9	5 8	eqtrd	$⊢ (W \in CPreHil \land A \in V) \to {N (A)}^{2} = A \underset{˙}{,} A$