nmcexi

Description: Lemma for nmcopexi and nmcfnexi . The norm of a continuous linear Hilbert space operator or functional exists. Theorem 3.5(i) of Beran p. 99. (Contributed by Mario Carneiro, 17-Nov-2013) (Proof shortened by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmcex.1	$⊢ \exists y \in ℝ^{+} \forall z \in ℋ ({norm}_{ℎ} (z) < y \to N (T (z)) < 1)$
	nmcex.2	$⊢ S (T) = sup (\{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} ℝ^{*} <)$
	nmcex.3	$⊢ x \in ℋ \to N (T (x)) \in ℝ$
	nmcex.4	$⊢ N (T (0_{ℎ})) = 0$
	nmcex.5	$⊢ (\frac{y}{2} \in ℝ^{+} \land x \in ℋ) \to (\frac{y}{2}) N (T (x)) = N (T ((\frac{y}{2}) \cdot_{ℎ} x))$
Assertion	nmcexi	$⊢ S (T) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		nmcex.1	$⊢ \exists y \in ℝ^{+} \forall z \in ℋ ({norm}_{ℎ} (z) < y \to N (T (z)) < 1)$
2		nmcex.2	$⊢ S (T) = sup (\{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} ℝ^{*} <)$
3		nmcex.3	$⊢ x \in ℋ \to N (T (x)) \in ℝ$
4		nmcex.4	$⊢ N (T (0_{ℎ})) = 0$
5		nmcex.5	$⊢ (\frac{y}{2} \in ℝ^{+} \land x \in ℋ) \to (\frac{y}{2}) N (T (x)) = N (T ((\frac{y}{2}) \cdot_{ℎ} x))$
6		eleq1	$⊢ m = N (T (x)) \to (m \in ℝ \leftrightarrow N (T (x)) \in ℝ)$
7	3 6	syl5ibrcom	$⊢ x \in ℋ \to (m = N (T (x)) \to m \in ℝ)$
8	7	imp	$⊢ (x \in ℋ \land m = N (T (x))) \to m \in ℝ$
9	8	adantrl	$⊢ (x \in ℋ \land ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))) \to m \in ℝ$
10	9	rexlimiva	$⊢ \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x))) \to m \in ℝ$
11	10	abssi	$⊢ \{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} \subseteq ℝ$
12		ax-hv0cl	$⊢ 0_{ℎ} \in ℋ$
13		norm0	$⊢ {norm}_{ℎ} (0_{ℎ}) = 0$
14		0le1	$⊢ 0 \leq 1$
15	13 14	eqbrtri	$⊢ {norm}_{ℎ} (0_{ℎ}) \leq 1$
16	4	eqcomi	$⊢ 0 = N (T (0_{ℎ}))$
17	15 16	pm3.2i	$⊢ ({norm}_{ℎ} (0_{ℎ}) \leq 1 \land 0 = N (T (0_{ℎ})))$
18		fveq2	$⊢ x = 0_{ℎ} \to {norm}_{ℎ} (x) = {norm}_{ℎ} (0_{ℎ})$
19	18	breq1d	$⊢ x = 0_{ℎ} \to ({norm}_{ℎ} (x) \leq 1 \leftrightarrow {norm}_{ℎ} (0_{ℎ}) \leq 1)$
20		2fveq3	$⊢ x = 0_{ℎ} \to N (T (x)) = N (T (0_{ℎ}))$
21	20	eqeq2d	$⊢ x = 0_{ℎ} \to (0 = N (T (x)) \leftrightarrow 0 = N (T (0_{ℎ})))$
22	19 21	anbi12d	$⊢ x = 0_{ℎ} \to (({norm}_{ℎ} (x) \leq 1 \land 0 = N (T (x))) \leftrightarrow ({norm}_{ℎ} (0_{ℎ}) \leq 1 \land 0 = N (T (0_{ℎ}))))$
23	22	rspcev	$⊢ (0_{ℎ} \in ℋ \land ({norm}_{ℎ} (0_{ℎ}) \leq 1 \land 0 = N (T (0_{ℎ})))) \to \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land 0 = N (T (x)))$
24	12 17 23	mp2an	$⊢ \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land 0 = N (T (x)))$
25		c0ex	$⊢ 0 \in V$
26		eqeq1	$⊢ m = 0 \to (m = N (T (x)) \leftrightarrow 0 = N (T (x)))$
27	26	anbi2d	$⊢ m = 0 \to (({norm}_{ℎ} (x) \leq 1 \land m = N (T (x))) \leftrightarrow ({norm}_{ℎ} (x) \leq 1 \land 0 = N (T (x))))$
28	27	rexbidv	$⊢ m = 0 \to (\exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x))) \leftrightarrow \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land 0 = N (T (x))))$
29	25 28	elab	$⊢ 0 \in \{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} \leftrightarrow \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land 0 = N (T (x)))$
30	24 29	mpbir	$⊢ 0 \in \{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\}$
31	30	ne0ii	$⊢ \{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} \neq \emptyset$
32		2rp	$⊢ 2 \in ℝ^{+}$
33		rpdivcl	$⊢ (2 \in ℝ^{+} \land y \in ℝ^{+}) \to \frac{2}{y} \in ℝ^{+}$
34	32 33	mpan	$⊢ y \in ℝ^{+} \to \frac{2}{y} \in ℝ^{+}$
35	34	rpred	$⊢ y \in ℝ^{+} \to \frac{2}{y} \in ℝ$
36	35	adantr	$⊢ (y \in ℝ^{+} \land \forall z \in ℋ ({norm}_{ℎ} (z) < y \to N (T (z)) < 1)) \to \frac{2}{y} \in ℝ$
37		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
38	37	adantr	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to y \in ℝ$
39	38	rehalfcld	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to \frac{y}{2} \in ℝ$
40	39	recnd	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to \frac{y}{2} \in ℂ$
41		simprl	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to x \in ℋ$
42		hvmulcl	$⊢ (\frac{y}{2} \in ℂ \land x \in ℋ) \to (\frac{y}{2}) \cdot_{ℎ} x \in ℋ$
43	40 41 42	syl2anc	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to (\frac{y}{2}) \cdot_{ℎ} x \in ℋ$
44		normcl	$⊢ (\frac{y}{2}) \cdot_{ℎ} x \in ℋ \to {norm}_{ℎ} ((\frac{y}{2}) \cdot_{ℎ} x) \in ℝ$
45	43 44	syl	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to {norm}_{ℎ} ((\frac{y}{2}) \cdot_{ℎ} x) \in ℝ$
46		simprr	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to {norm}_{ℎ} (x) \leq 1$
47		normcl	$⊢ x \in ℋ \to {norm}_{ℎ} (x) \in ℝ$
48	47	ad2antrl	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to {norm}_{ℎ} (x) \in ℝ$
49		1red	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to 1 \in ℝ$
50		rphalfcl	$⊢ y \in ℝ^{+} \to \frac{y}{2} \in ℝ^{+}$
51	50	adantr	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to \frac{y}{2} \in ℝ^{+}$
52	48 49 51	lemul2d	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to ({norm}_{ℎ} (x) \leq 1 \leftrightarrow (\frac{y}{2}) {norm}_{ℎ} (x) \leq (\frac{y}{2}) \cdot 1)$
53	46 52	mpbid	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to (\frac{y}{2}) {norm}_{ℎ} (x) \leq (\frac{y}{2}) \cdot 1$
54		rpcn	$⊢ \frac{y}{2} \in ℝ^{+} \to \frac{y}{2} \in ℂ$
55		norm-iii	$⊢ (\frac{y}{2} \in ℂ \land x \in ℋ) \to {norm}_{ℎ} ((\frac{y}{2}) \cdot_{ℎ} x) = \|\frac{y}{2}\| {norm}_{ℎ} (x)$
56	54 55	sylan	$⊢ (\frac{y}{2} \in ℝ^{+} \land x \in ℋ) \to {norm}_{ℎ} ((\frac{y}{2}) \cdot_{ℎ} x) = \|\frac{y}{2}\| {norm}_{ℎ} (x)$
57		rpre	$⊢ \frac{y}{2} \in ℝ^{+} \to \frac{y}{2} \in ℝ$
58		rpge0	$⊢ \frac{y}{2} \in ℝ^{+} \to 0 \leq \frac{y}{2}$
59	57 58	absidd	$⊢ \frac{y}{2} \in ℝ^{+} \to \|\frac{y}{2}\| = \frac{y}{2}$
60	59	oveq1d	$⊢ \frac{y}{2} \in ℝ^{+} \to \|\frac{y}{2}\| {norm}_{ℎ} (x) = (\frac{y}{2}) {norm}_{ℎ} (x)$
61	60	adantr	$⊢ (\frac{y}{2} \in ℝ^{+} \land x \in ℋ) \to \|\frac{y}{2}\| {norm}_{ℎ} (x) = (\frac{y}{2}) {norm}_{ℎ} (x)$
62	56 61	eqtr2d	$⊢ (\frac{y}{2} \in ℝ^{+} \land x \in ℋ) \to (\frac{y}{2}) {norm}_{ℎ} (x) = {norm}_{ℎ} ((\frac{y}{2}) \cdot_{ℎ} x)$
63	51 41 62	syl2anc	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to (\frac{y}{2}) {norm}_{ℎ} (x) = {norm}_{ℎ} ((\frac{y}{2}) \cdot_{ℎ} x)$
64	40	mulid1d	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to (\frac{y}{2}) \cdot 1 = \frac{y}{2}$
65	53 63 64	3brtr3d	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to {norm}_{ℎ} ((\frac{y}{2}) \cdot_{ℎ} x) \leq \frac{y}{2}$
66		rphalflt	$⊢ y \in ℝ^{+} \to \frac{y}{2} < y$
67	66	adantr	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to \frac{y}{2} < y$
68	45 39 38 65 67	lelttrd	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to {norm}_{ℎ} ((\frac{y}{2}) \cdot_{ℎ} x) < y$
69		fveq2	$⊢ z = (\frac{y}{2}) \cdot_{ℎ} x \to {norm}_{ℎ} (z) = {norm}_{ℎ} ((\frac{y}{2}) \cdot_{ℎ} x)$
70	69	breq1d	$⊢ z = (\frac{y}{2}) \cdot_{ℎ} x \to ({norm}_{ℎ} (z) < y \leftrightarrow {norm}_{ℎ} ((\frac{y}{2}) \cdot_{ℎ} x) < y)$
71		2fveq3	$⊢ z = (\frac{y}{2}) \cdot_{ℎ} x \to N (T (z)) = N (T ((\frac{y}{2}) \cdot_{ℎ} x))$
72	71	breq1d	$⊢ z = (\frac{y}{2}) \cdot_{ℎ} x \to (N (T (z)) < 1 \leftrightarrow N (T ((\frac{y}{2}) \cdot_{ℎ} x)) < 1)$
73	70 72	imbi12d	$⊢ z = (\frac{y}{2}) \cdot_{ℎ} x \to (({norm}_{ℎ} (z) < y \to N (T (z)) < 1) \leftrightarrow ({norm}_{ℎ} ((\frac{y}{2}) \cdot_{ℎ} x) < y \to N (T ((\frac{y}{2}) \cdot_{ℎ} x)) < 1))$
74	73	rspcv	$⊢ (\frac{y}{2}) \cdot_{ℎ} x \in ℋ \to (\forall z \in ℋ ({norm}_{ℎ} (z) < y \to N (T (z)) < 1) \to ({norm}_{ℎ} ((\frac{y}{2}) \cdot_{ℎ} x) < y \to N (T ((\frac{y}{2}) \cdot_{ℎ} x)) < 1))$
75	43 74	syl	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to (\forall z \in ℋ ({norm}_{ℎ} (z) < y \to N (T (z)) < 1) \to ({norm}_{ℎ} ((\frac{y}{2}) \cdot_{ℎ} x) < y \to N (T ((\frac{y}{2}) \cdot_{ℎ} x)) < 1))$
76	68 75	mpid	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to (\forall z \in ℋ ({norm}_{ℎ} (z) < y \to N (T (z)) < 1) \to N (T ((\frac{y}{2}) \cdot_{ℎ} x)) < 1)$
77	3	ad2antrl	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to N (T (x)) \in ℝ$
78	77 49 51	ltmuldiv2d	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to ((\frac{y}{2}) N (T (x)) < 1 \leftrightarrow N (T (x)) < \frac{1}{\frac{y}{2}})$
79	51	rprecred	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to \frac{1}{\frac{y}{2}} \in ℝ$
80		ltle	$⊢ (N (T (x)) \in ℝ \land \frac{1}{\frac{y}{2}} \in ℝ) \to (N (T (x)) < \frac{1}{\frac{y}{2}} \to N (T (x)) \leq \frac{1}{\frac{y}{2}})$
81	77 79 80	syl2anc	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to (N (T (x)) < \frac{1}{\frac{y}{2}} \to N (T (x)) \leq \frac{1}{\frac{y}{2}})$
82	78 81	sylbid	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to ((\frac{y}{2}) N (T (x)) < 1 \to N (T (x)) \leq \frac{1}{\frac{y}{2}})$
83	51 41 5	syl2anc	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to (\frac{y}{2}) N (T (x)) = N (T ((\frac{y}{2}) \cdot_{ℎ} x))$
84	83	breq1d	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to ((\frac{y}{2}) N (T (x)) < 1 \leftrightarrow N (T ((\frac{y}{2}) \cdot_{ℎ} x)) < 1)$
85		rpcn	$⊢ y \in ℝ^{+} \to y \in ℂ$
86		rpne0	$⊢ y \in ℝ^{+} \to y \neq 0$
87		2cn	$⊢ 2 \in ℂ$
88		2ne0	$⊢ 2 \neq 0$
89		recdiv	$⊢ ((y \in ℂ \land y \neq 0) \land (2 \in ℂ \land 2 \neq 0)) \to \frac{1}{\frac{y}{2}} = \frac{2}{y}$
90	87 88 89	mpanr12	$⊢ (y \in ℂ \land y \neq 0) \to \frac{1}{\frac{y}{2}} = \frac{2}{y}$
91	85 86 90	syl2anc	$⊢ y \in ℝ^{+} \to \frac{1}{\frac{y}{2}} = \frac{2}{y}$
92	91	adantr	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to \frac{1}{\frac{y}{2}} = \frac{2}{y}$
93	92	breq2d	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to (N (T (x)) \leq \frac{1}{\frac{y}{2}} \leftrightarrow N (T (x)) \leq \frac{2}{y})$
94	82 84 93	3imtr3d	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to (N (T ((\frac{y}{2}) \cdot_{ℎ} x)) < 1 \to N (T (x)) \leq \frac{2}{y})$
95	76 94	syld	$⊢ (y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to (\forall z \in ℋ ({norm}_{ℎ} (z) < y \to N (T (z)) < 1) \to N (T (x)) \leq \frac{2}{y})$
96	95	imp	$⊢ ((y \in ℝ^{+} \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \land \forall z \in ℋ ({norm}_{ℎ} (z) < y \to N (T (z)) < 1)) \to N (T (x)) \leq \frac{2}{y}$
97	96	an32s	$⊢ ((y \in ℝ^{+} \land \forall z \in ℋ ({norm}_{ℎ} (z) < y \to N (T (z)) < 1)) \land (x \in ℋ \land {norm}_{ℎ} (x) \leq 1)) \to N (T (x)) \leq \frac{2}{y}$
98	97	anassrs	$⊢ (((y \in ℝ^{+} \land \forall z \in ℋ ({norm}_{ℎ} (z) < y \to N (T (z)) < 1)) \land x \in ℋ) \land {norm}_{ℎ} (x) \leq 1) \to N (T (x)) \leq \frac{2}{y}$
99		breq1	$⊢ n = N (T (x)) \to (n \leq \frac{2}{y} \leftrightarrow N (T (x)) \leq \frac{2}{y})$
100	98 99	syl5ibrcom	$⊢ (((y \in ℝ^{+} \land \forall z \in ℋ ({norm}_{ℎ} (z) < y \to N (T (z)) < 1)) \land x \in ℋ) \land {norm}_{ℎ} (x) \leq 1) \to (n = N (T (x)) \to n \leq \frac{2}{y})$
101	100	expimpd	$⊢ ((y \in ℝ^{+} \land \forall z \in ℋ ({norm}_{ℎ} (z) < y \to N (T (z)) < 1)) \land x \in ℋ) \to (({norm}_{ℎ} (x) \leq 1 \land n = N (T (x))) \to n \leq \frac{2}{y})$
102	101	rexlimdva	$⊢ (y \in ℝ^{+} \land \forall z \in ℋ ({norm}_{ℎ} (z) < y \to N (T (z)) < 1)) \to (\exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land n = N (T (x))) \to n \leq \frac{2}{y})$
103	102	alrimiv	$⊢ (y \in ℝ^{+} \land \forall z \in ℋ ({norm}_{ℎ} (z) < y \to N (T (z)) < 1)) \to \forall n (\exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land n = N (T (x))) \to n \leq \frac{2}{y})$
104		eqeq1	$⊢ m = n \to (m = N (T (x)) \leftrightarrow n = N (T (x)))$
105	104	anbi2d	$⊢ m = n \to (({norm}_{ℎ} (x) \leq 1 \land m = N (T (x))) \leftrightarrow ({norm}_{ℎ} (x) \leq 1 \land n = N (T (x))))$
106	105	rexbidv	$⊢ m = n \to (\exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x))) \leftrightarrow \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land n = N (T (x))))$
107	106	ralab	$⊢ \forall n \in \{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} n \leq z \leftrightarrow \forall n (\exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land n = N (T (x))) \to n \leq z)$
108		breq2	$⊢ z = \frac{2}{y} \to (n \leq z \leftrightarrow n \leq \frac{2}{y})$
109	108	imbi2d	$⊢ z = \frac{2}{y} \to ((\exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land n = N (T (x))) \to n \leq z) \leftrightarrow (\exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land n = N (T (x))) \to n \leq \frac{2}{y}))$
110	109	albidv	$⊢ z = \frac{2}{y} \to (\forall n (\exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land n = N (T (x))) \to n \leq z) \leftrightarrow \forall n (\exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land n = N (T (x))) \to n \leq \frac{2}{y}))$
111	107 110	syl5bb	$⊢ z = \frac{2}{y} \to (\forall n \in \{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} n \leq z \leftrightarrow \forall n (\exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land n = N (T (x))) \to n \leq \frac{2}{y}))$
112	111	rspcev	$⊢ (\frac{2}{y} \in ℝ \land \forall n (\exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land n = N (T (x))) \to n \leq \frac{2}{y})) \to \exists z \in ℝ \forall n \in \{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} n \leq z$
113	36 103 112	syl2anc	$⊢ (y \in ℝ^{+} \land \forall z \in ℋ ({norm}_{ℎ} (z) < y \to N (T (z)) < 1)) \to \exists z \in ℝ \forall n \in \{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} n \leq z$
114	113	rexlimiva	$⊢ \exists y \in ℝ^{+} \forall z \in ℋ ({norm}_{ℎ} (z) < y \to N (T (z)) < 1) \to \exists z \in ℝ \forall n \in \{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} n \leq z$
115	1 114	ax-mp	$⊢ \exists z \in ℝ \forall n \in \{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} n \leq z$
116		supxrre	$⊢ (\{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} \subseteq ℝ \land \{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} \neq \emptyset \land \exists z \in ℝ \forall n \in \{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} n \leq z) \to sup (\{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} ℝ^{*} <) = sup (\{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} ℝ <)$
117	11 31 115 116	mp3an	$⊢ sup (\{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} ℝ^{*} <) = sup (\{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} ℝ <)$
118	2 117	eqtri	$⊢ S (T) = sup (\{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} ℝ <)$
119		suprcl	$⊢ (\{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} \subseteq ℝ \land \{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} \neq \emptyset \land \exists z \in ℝ \forall n \in \{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} n \leq z) \to sup (\{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} ℝ <) \in ℝ$
120	11 31 115 119	mp3an	$⊢ sup (\{m \| \exists x \in ℋ ({norm}_{ℎ} (x) \leq 1 \land m = N (T (x)))\} ℝ <) \in ℝ$
121	118 120	eqeltri	$⊢ S (T) \in ℝ$

Metamath Proof Explorer

Theorem nmcexi

Proof