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

Metamath Proof Explorer

Theorem cphnm

Description: The square of the norm is the norm of an inner product in a subcomplex pre-Hilbert space. (Contributed 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	cphnm	$⊢ (W \in CPreHil \land A \in V) \to N (A) = \sqrt{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	cphnmfval	$⊢ W \in CPreHil \to N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x})$
5	4	fveq1d	$⊢ W \in CPreHil \to N (A) = (x \in V ⟼ \sqrt{x \underset{˙}{,} x}) (A)$
6		oveq12	$⊢ (x = A \land x = A) \to x \underset{˙}{,} x = A \underset{˙}{,} A$
7	6	anidms	$⊢ x = A \to x \underset{˙}{,} x = A \underset{˙}{,} A$
8	7	fveq2d	$⊢ x = A \to \sqrt{x \underset{˙}{,} x} = \sqrt{A \underset{˙}{,} A}$
9		eqid	$⊢ (x \in V ⟼ \sqrt{x \underset{˙}{,} x}) = (x \in V ⟼ \sqrt{x \underset{˙}{,} x})$
10		fvex	$⊢ \sqrt{A \underset{˙}{,} A} \in V$
11	8 9 10	fvmpt	$⊢ A \in V \to (x \in V ⟼ \sqrt{x \underset{˙}{,} x}) (A) = \sqrt{A \underset{˙}{,} A}$
12	5 11	sylan9eq	$⊢ (W \in CPreHil \land A \in V) \to N (A) = \sqrt{A \underset{˙}{,} A}$