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

Metamath Proof Explorer

Theorem cphnmfval

Description: The value of the norm in a subcomplex pre-Hilbert space is the square root of the inner product of a vector with itself. (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	cphnmfval	$⊢ W \in CPreHil \to N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x})$

Proof

Step	Hyp	Ref	Expression
1		nmsq.v	$⊢ V = {Base}_{W}$
2		nmsq.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
3		nmsq.n	$⊢ N = norm (W)$
4		eqid	$⊢ Scalar (W) = Scalar (W)$
5		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
6	1 2 3 4 5	iscph	$⊢ W \in CPreHil \leftrightarrow ((W \in PreHil \land W \in NrmMod \land Scalar (W) = ℂ_{fld} ↾_{𝑠} {Base}_{Scalar (W)}) \land \sqrt [{Base}_{Scalar (W)} \cap [0, +∞)] \subseteq {Base}_{Scalar (W)} \land N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x}))$
7	6	simp3bi	$⊢ W \in CPreHil \to N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x})$