cphnmf

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	cphnmf	$⊢ W \in CPreHil \to N : V ⟶ K$

Proof

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	cphnmfval	$⊢ W \in CPreHil \to N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x})$
7		simpl	$⊢ (W \in CPreHil \land x \in V) \to W \in CPreHil$
8		cphphl	$⊢ W \in CPreHil \to W \in PreHil$
9	8	adantr	$⊢ (W \in CPreHil \land x \in V) \to W \in PreHil$
10		simpr	$⊢ (W \in CPreHil \land x \in V) \to x \in V$
11	4 2 1 5	ipcl	$⊢ (W \in PreHil \land x \in V \land x \in V) \to x \underset{˙}{,} x \in K$
12	9 10 10 11	syl3anc	$⊢ (W \in CPreHil \land x \in V) \to x \underset{˙}{,} x \in K$
13	1 2 3	nmsq	$⊢ (W \in CPreHil \land x \in V) \to {N (x)}^{2} = x \underset{˙}{,} x$
14		cphngp	$⊢ W \in CPreHil \to W \in NrmGrp$
15	1 3	nmcl	$⊢ (W \in NrmGrp \land x \in V) \to N (x) \in ℝ$
16	14 15	sylan	$⊢ (W \in CPreHil \land x \in V) \to N (x) \in ℝ$
17	16	resqcld	$⊢ (W \in CPreHil \land x \in V) \to {N (x)}^{2} \in ℝ$
18	13 17	eqeltrrd	$⊢ (W \in CPreHil \land x \in V) \to x \underset{˙}{,} x \in ℝ$
19	16	sqge0d	$⊢ (W \in CPreHil \land x \in V) \to 0 \leq {N (x)}^{2}$
20	19 13	breqtrd	$⊢ (W \in CPreHil \land x \in V) \to 0 \leq x \underset{˙}{,} x$
21	4 5	cphsqrtcl	$⊢ (W \in CPreHil \land (x \underset{˙}{,} x \in K \land x \underset{˙}{,} x \in ℝ \land 0 \leq x \underset{˙}{,} x)) \to \sqrt{x \underset{˙}{,} x} \in K$
22	7 12 18 20 21	syl13anc	$⊢ (W \in CPreHil \land x \in V) \to \sqrt{x \underset{˙}{,} x} \in K$
23	6 22	fmpt3d	$⊢ W \in CPreHil \to N : V ⟶ K$

Metamath Proof Explorer

Theorem cphnmf

Proof