nmfn0

Description: The norm of the identically zero functional is zero. (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	nmfn0	$⊢ {norm}_{fn} (ℋ \times \{0\}) = 0$

Proof

Step	Hyp	Ref	Expression
1		0lnfn	$⊢ ℋ \times \{0\} \in LinFn$
2		lnfnf	$⊢ ℋ \times \{0\} \in LinFn \to (ℋ \times \{0\}) : ℋ ⟶ ℂ$
3		nmfnval	$⊢ (ℋ \times \{0\}) : ℋ ⟶ ℂ \to {norm}_{fn} (ℋ \times \{0\}) = sup (\{x \| \exists y \in ℋ ({norm}_{ℎ} (y) \leq 1 \land x = \|(ℋ \times \{0\}) (y)\|)\} ℝ^{*} <)$
4	1 2 3	mp2b	$⊢ {norm}_{fn} (ℋ \times \{0\}) = sup (\{x \| \exists y \in ℋ ({norm}_{ℎ} (y) \leq 1 \land x = \|(ℋ \times \{0\}) (y)\|)\} ℝ^{*} <)$
5		c0ex	$⊢ 0 \in V$
6	5	fvconst2	$⊢ y \in ℋ \to (ℋ \times \{0\}) (y) = 0$
7	6	fveq2d	$⊢ y \in ℋ \to \|(ℋ \times \{0\}) (y)\| = \|0\|$
8		abs0	$⊢ \|0\| = 0$
9	7 8	eqtrdi	$⊢ y \in ℋ \to \|(ℋ \times \{0\}) (y)\| = 0$
10	9	eqeq2d	$⊢ y \in ℋ \to (x = \|(ℋ \times \{0\}) (y)\| \leftrightarrow x = 0)$
11	10	anbi2d	$⊢ y \in ℋ \to (({norm}_{ℎ} (y) \leq 1 \land x = \|(ℋ \times \{0\}) (y)\|) \leftrightarrow ({norm}_{ℎ} (y) \leq 1 \land x = 0))$
12	11	rexbiia	$⊢ \exists y \in ℋ ({norm}_{ℎ} (y) \leq 1 \land x = \|(ℋ \times \{0\}) (y)\|) \leftrightarrow \exists y \in ℋ ({norm}_{ℎ} (y) \leq 1 \land x = 0)$
13		ax-hv0cl	$⊢ 0_{ℎ} \in ℋ$
14		0le1	$⊢ 0 \leq 1$
15		fveq2	$⊢ y = 0_{ℎ} \to {norm}_{ℎ} (y) = {norm}_{ℎ} (0_{ℎ})$
16		norm0	$⊢ {norm}_{ℎ} (0_{ℎ}) = 0$
17	15 16	eqtrdi	$⊢ y = 0_{ℎ} \to {norm}_{ℎ} (y) = 0$
18	17	breq1d	$⊢ y = 0_{ℎ} \to ({norm}_{ℎ} (y) \leq 1 \leftrightarrow 0 \leq 1)$
19	18	rspcev	$⊢ (0_{ℎ} \in ℋ \land 0 \leq 1) \to \exists y \in ℋ {norm}_{ℎ} (y) \leq 1$
20	13 14 19	mp2an	$⊢ \exists y \in ℋ {norm}_{ℎ} (y) \leq 1$
21		r19.41v	$⊢ \exists y \in ℋ ({norm}_{ℎ} (y) \leq 1 \land x = 0) \leftrightarrow (\exists y \in ℋ {norm}_{ℎ} (y) \leq 1 \land x = 0)$
22	20 21	mpbiran	$⊢ \exists y \in ℋ ({norm}_{ℎ} (y) \leq 1 \land x = 0) \leftrightarrow x = 0$
23	12 22	bitri	$⊢ \exists y \in ℋ ({norm}_{ℎ} (y) \leq 1 \land x = \|(ℋ \times \{0\}) (y)\|) \leftrightarrow x = 0$
24	23	abbii	$⊢ \{x \| \exists y \in ℋ ({norm}_{ℎ} (y) \leq 1 \land x = \|(ℋ \times \{0\}) (y)\|)\} = \{x \| x = 0\}$
25		df-sn	$⊢ \{0\} = \{x \| x = 0\}$
26	24 25	eqtr4i	$⊢ \{x \| \exists y \in ℋ ({norm}_{ℎ} (y) \leq 1 \land x = \|(ℋ \times \{0\}) (y)\|)\} = \{0\}$
27	26	supeq1i	$⊢ sup (\{x \| \exists y \in ℋ ({norm}_{ℎ} (y) \leq 1 \land x = \|(ℋ \times \{0\}) (y)\|)\} ℝ^{} <) = sup (\{0\} ℝ^{} <)$
28		xrltso	$⊢ < Or ℝ^{*}$
29		0xr	$⊢ 0 \in ℝ^{*}$
30		supsn	$⊢ (< Or ℝ^{} \land 0 \in ℝ^{}) \to sup (\{0\} ℝ^{*} <) = 0$
31	28 29 30	mp2an	$⊢ sup (\{0\} ℝ^{*} <) = 0$
32	4 27 31	3eqtri	$⊢ {norm}_{fn} (ℋ \times \{0\}) = 0$

Metamath Proof Explorer

Theorem nmfn0

Proof