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

Metamath Proof Explorer

Theorem cphnmcl

Description: The norm of a vector is a member of the scalar field in a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 9-Oct-2015)

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

Step	Hyp	Ref	Expression
1		nmsq.v	$⊢ V = {Base}_{W}$
2		nmsq.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
3		nmsq.n	$⊢ N = norm (W)$
4		cphnmcl.f	$⊢ F = Scalar (W)$
5		cphnmcl.k	$⊢ K = {Base}_{F}$
6	1 2 3 4 5	cphnmf	$⊢ W \in CPreHil \to N : V ⟶ K$
7	6	ffvelcdmda	$⊢ (W \in CPreHil \land A \in V) \to N (A) \in K$