htthlem

Description: Lemma for htth . The collection K , which consists of functions F ( z ) ( w ) = <. w | T ( z ) >. = <. T ( w ) | z >. for each z in the unit ball, is a collection of bounded linear functions by ipblnfi , so by the Uniform Boundedness theorem ubth , there is a uniform bound y on || F ( x ) || for all x in the unit ball. Then | T ( x ) | ^ 2 = <. T ( x ) | T ( x ) >. = F ( x ) ( T ( x ) ) <_ y | T ( x ) | , so | T ( x ) | <_ y and T is bounded. (Contributed by NM, 11-Jan-2008) (Revised by Mario Carneiro, 23-Aug-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	htth.1	$⊢ X = BaseSet (U)$
	htth.2	$⊢ P = \cdot_{𝑖OLD} (U)$
	htth.3	$⊢ L = U LnOp U$
	htth.4	$⊢ B = U BLnOp U$
	htthlem.5	$⊢ N = {norm}_{CV} (U)$
	htthlem.6	$⊢ U \in {CHil}_{OLD}$
	htthlem.7	$⊢ W = ⟨⟨+ \times⟩, abs⟩$
	htthlem.8	$⊢ φ \to T \in L$
	htthlem.9	$⊢ φ \to \forall x \in X \forall y \in X x P T (y) = T (x) P y$
	htthlem.10	$⊢ F = (z \in X ⟼ (w \in X ⟼ w P T (z)))$
	htthlem.11	$⊢ K = F [\{z \in X \| N (z) \leq 1\}]$
Assertion	htthlem	$⊢ φ \to T \in B$

Proof

Step	Hyp	Ref	Expression
1		htth.1	$⊢ X = BaseSet (U)$
2		htth.2	$⊢ P = \cdot_{𝑖OLD} (U)$
3		htth.3	$⊢ L = U LnOp U$
4		htth.4	$⊢ B = U BLnOp U$
5		htthlem.5	$⊢ N = {norm}_{CV} (U)$
6		htthlem.6	$⊢ U \in {CHil}_{OLD}$
7		htthlem.7	$⊢ W = ⟨⟨+ \times⟩, abs⟩$
8		htthlem.8	$⊢ φ \to T \in L$
9		htthlem.9	$⊢ φ \to \forall x \in X \forall y \in X x P T (y) = T (x) P y$
10		htthlem.10	$⊢ F = (z \in X ⟼ (w \in X ⟼ w P T (z)))$
11		htthlem.11	$⊢ K = F [\{z \in X \| N (z) \leq 1\}]$
12	6	hlnvi	$⊢ U \in NrmCVec$
13	1 1 3	lnof	$⊢ (U \in NrmCVec \land U \in NrmCVec \land T \in L) \to T : X ⟶ X$
14	12 12 13	mp3an12	$⊢ T \in L \to T : X ⟶ X$
15	8 14	syl	$⊢ φ \to T : X ⟶ X$
16	15	ffvelcdmda	$⊢ (φ \land x \in X) \to T (x) \in X$
17	1 5	nvcl	$⊢ (U \in NrmCVec \land T (x) \in X) \to N (T (x)) \in ℝ$
18	12 16 17	sylancr	$⊢ (φ \land x \in X) \to N (T (x)) \in ℝ$
19	15	ffvelcdmda	$⊢ (φ \land z \in X) \to T (z) \in X$
20		hlph	$⊢ U \in {CHil}_{OLD} \to U \in {CPreHil}_{OLD}$
21	6 20	ax-mp	$⊢ U \in {CPreHil}_{OLD}$
22		eqid	$⊢ U BLnOp W = U BLnOp W$
23		eqid	$⊢ (w \in X ⟼ w P T (z)) = (w \in X ⟼ w P T (z))$
24	1 2 21 7 22 23	ipblnfi	$⊢ T (z) \in X \to (w \in X ⟼ w P T (z)) \in (U BLnOp W)$
25	19 24	syl	$⊢ (φ \land z \in X) \to (w \in X ⟼ w P T (z)) \in (U BLnOp W)$
26	25 10	fmptd	$⊢ φ \to F : X ⟶ U BLnOp W$
27	26	ffund	$⊢ φ \to Fun F$
28	27	adantr	$⊢ (φ \land x \in X) \to Fun F$
29		id	$⊢ w \in K \to w \in K$
30	29 11	eleqtrdi	$⊢ w \in K \to w \in F [\{z \in X \| N (z) \leq 1\}]$
31		fvelima	$⊢ (Fun F \land w \in F [\{z \in X \| N (z) \leq 1\}]) \to \exists y \in \{z \in X \| N (z) \leq 1\} F (y) = w$
32	28 30 31	syl2an	$⊢ ((φ \land x \in X) \land w \in K) \to \exists y \in \{z \in X \| N (z) \leq 1\} F (y) = w$
33	32	ex	$⊢ (φ \land x \in X) \to (w \in K \to \exists y \in \{z \in X \| N (z) \leq 1\} F (y) = w)$
34		fveq2	$⊢ z = y \to N (z) = N (y)$
35	34	breq1d	$⊢ z = y \to (N (z) \leq 1 \leftrightarrow N (y) \leq 1)$
36	35	elrab	$⊢ y \in \{z \in X \| N (z) \leq 1\} \leftrightarrow (y \in X \land N (y) \leq 1)$
37		fveq2	$⊢ z = y \to T (z) = T (y)$
38	37	oveq2d	$⊢ z = y \to w P T (z) = w P T (y)$
39	38	mpteq2dv	$⊢ z = y \to (w \in X ⟼ w P T (z)) = (w \in X ⟼ w P T (y))$
40	39 10 1	mptfvmpt	$⊢ y \in X \to F (y) = (w \in X ⟼ w P T (y))$
41	40	fveq1d	$⊢ y \in X \to F (y) (x) = (w \in X ⟼ w P T (y)) (x)$
42		oveq1	$⊢ w = x \to w P T (y) = x P T (y)$
43		eqid	$⊢ (w \in X ⟼ w P T (y)) = (w \in X ⟼ w P T (y))$
44		ovex	$⊢ x P T (y) \in V$
45	42 43 44	fvmpt	$⊢ x \in X \to (w \in X ⟼ w P T (y)) (x) = x P T (y)$
46	41 45	sylan9eqr	$⊢ (x \in X \land y \in X) \to F (y) (x) = x P T (y)$
47	46	ad2ant2lr	$⊢ ((φ \land x \in X) \land (y \in X \land N (y) \leq 1)) \to F (y) (x) = x P T (y)$
48		rsp2	$⊢ \forall x \in X \forall y \in X x P T (y) = T (x) P y \to ((x \in X \land y \in X) \to x P T (y) = T (x) P y)$
49	9 48	syl	$⊢ φ \to ((x \in X \land y \in X) \to x P T (y) = T (x) P y)$
50	49	impl	$⊢ ((φ \land x \in X) \land y \in X) \to x P T (y) = T (x) P y$
51	50	adantrr	$⊢ ((φ \land x \in X) \land (y \in X \land N (y) \leq 1)) \to x P T (y) = T (x) P y$
52	47 51	eqtrd	$⊢ ((φ \land x \in X) \land (y \in X \land N (y) \leq 1)) \to F (y) (x) = T (x) P y$
53	52	fveq2d	$⊢ ((φ \land x \in X) \land (y \in X \land N (y) \leq 1)) \to \|F (y) (x)\| = \|T (x) P y\|$
54		simpl	$⊢ (y \in X \land N (y) \leq 1) \to y \in X$
55	1 2	dipcl	$⊢ (U \in NrmCVec \land T (x) \in X \land y \in X) \to T (x) P y \in ℂ$
56	12 55	mp3an1	$⊢ (T (x) \in X \land y \in X) \to T (x) P y \in ℂ$
57	16 54 56	syl2an	$⊢ ((φ \land x \in X) \land (y \in X \land N (y) \leq 1)) \to T (x) P y \in ℂ$
58	57	abscld	$⊢ ((φ \land x \in X) \land (y \in X \land N (y) \leq 1)) \to \|T (x) P y\| \in ℝ$
59	18	adantr	$⊢ ((φ \land x \in X) \land (y \in X \land N (y) \leq 1)) \to N (T (x)) \in ℝ$
60	1 5	nvcl	$⊢ (U \in NrmCVec \land y \in X) \to N (y) \in ℝ$
61	12 60	mpan	$⊢ y \in X \to N (y) \in ℝ$
62	61	ad2antrl	$⊢ ((φ \land x \in X) \land (y \in X \land N (y) \leq 1)) \to N (y) \in ℝ$
63	59 62	remulcld	$⊢ ((φ \land x \in X) \land (y \in X \land N (y) \leq 1)) \to N (T (x)) N (y) \in ℝ$
64	1 5 2 21	sii	$⊢ (T (x) \in X \land y \in X) \to \|T (x) P y\| \leq N (T (x)) N (y)$
65	16 54 64	syl2an	$⊢ ((φ \land x \in X) \land (y \in X \land N (y) \leq 1)) \to \|T (x) P y\| \leq N (T (x)) N (y)$
66		1red	$⊢ ((φ \land x \in X) \land (y \in X \land N (y) \leq 1)) \to 1 \in ℝ$
67	1 5	nvge0	$⊢ (U \in NrmCVec \land T (x) \in X) \to 0 \leq N (T (x))$
68	12 16 67	sylancr	$⊢ (φ \land x \in X) \to 0 \leq N (T (x))$
69	18 68	jca	$⊢ (φ \land x \in X) \to (N (T (x)) \in ℝ \land 0 \leq N (T (x)))$
70	69	adantr	$⊢ ((φ \land x \in X) \land (y \in X \land N (y) \leq 1)) \to (N (T (x)) \in ℝ \land 0 \leq N (T (x)))$
71		simprr	$⊢ ((φ \land x \in X) \land (y \in X \land N (y) \leq 1)) \to N (y) \leq 1$
72		lemul2a	$⊢ ((N (y) \in ℝ \land 1 \in ℝ \land (N (T (x)) \in ℝ \land 0 \leq N (T (x)))) \land N (y) \leq 1) \to N (T (x)) N (y) \leq N (T (x)) \cdot 1$
73	62 66 70 71 72	syl31anc	$⊢ ((φ \land x \in X) \land (y \in X \land N (y) \leq 1)) \to N (T (x)) N (y) \leq N (T (x)) \cdot 1$
74	59	recnd	$⊢ ((φ \land x \in X) \land (y \in X \land N (y) \leq 1)) \to N (T (x)) \in ℂ$
75	74	mulridd	$⊢ ((φ \land x \in X) \land (y \in X \land N (y) \leq 1)) \to N (T (x)) \cdot 1 = N (T (x))$
76	73 75	breqtrd	$⊢ ((φ \land x \in X) \land (y \in X \land N (y) \leq 1)) \to N (T (x)) N (y) \leq N (T (x))$
77	58 63 59 65 76	letrd	$⊢ ((φ \land x \in X) \land (y \in X \land N (y) \leq 1)) \to \|T (x) P y\| \leq N (T (x))$
78	53 77	eqbrtrd	$⊢ ((φ \land x \in X) \land (y \in X \land N (y) \leq 1)) \to \|F (y) (x)\| \leq N (T (x))$
79	36 78	sylan2b	$⊢ ((φ \land x \in X) \land y \in \{z \in X \| N (z) \leq 1\}) \to \|F (y) (x)\| \leq N (T (x))$
80		fveq1	$⊢ F (y) = w \to F (y) (x) = w (x)$
81	80	fveq2d	$⊢ F (y) = w \to \|F (y) (x)\| = \|w (x)\|$
82	81	breq1d	$⊢ F (y) = w \to (\|F (y) (x)\| \leq N (T (x)) \leftrightarrow \|w (x)\| \leq N (T (x)))$
83	79 82	syl5ibcom	$⊢ ((φ \land x \in X) \land y \in \{z \in X \| N (z) \leq 1\}) \to (F (y) = w \to \|w (x)\| \leq N (T (x)))$
84	83	rexlimdva	$⊢ (φ \land x \in X) \to (\exists y \in \{z \in X \| N (z) \leq 1\} F (y) = w \to \|w (x)\| \leq N (T (x)))$
85	33 84	syld	$⊢ (φ \land x \in X) \to (w \in K \to \|w (x)\| \leq N (T (x)))$
86	85	ralrimiv	$⊢ (φ \land x \in X) \to \forall w \in K \|w (x)\| \leq N (T (x))$
87		brralrspcev	$⊢ (N (T (x)) \in ℝ \land \forall w \in K \|w (x)\| \leq N (T (x))) \to \exists z \in ℝ \forall w \in K \|w (x)\| \leq z$
88	18 86 87	syl2anc	$⊢ (φ \land x \in X) \to \exists z \in ℝ \forall w \in K \|w (x)\| \leq z$
89	88	ralrimiva	$⊢ φ \to \forall x \in X \exists z \in ℝ \forall w \in K \|w (x)\| \leq z$
90		imassrn	$⊢ F [\{z \in X \| N (z) \leq 1\}] \subseteq ran F$
91	11 90	eqsstri	$⊢ K \subseteq ran F$
92	26	frnd	$⊢ φ \to ran F \subseteq U BLnOp W$
93	91 92	sstrid	$⊢ φ \to K \subseteq U BLnOp W$
94		hlobn	$⊢ U \in {CHil}_{OLD} \to U \in CBan$
95	6 94	ax-mp	$⊢ U \in CBan$
96	7	cnnv	$⊢ W \in NrmCVec$
97	7	cnnvnm	$⊢ abs = {norm}_{CV} (W)$
98		eqid	$⊢ U {normOp}_{OLD} W = U {normOp}_{OLD} W$
99	1 97 98	ubth	$⊢ (U \in CBan \land W \in NrmCVec \land K \subseteq U BLnOp W) \to (\forall x \in X \exists z \in ℝ \forall w \in K \|w (x)\| \leq z \leftrightarrow \exists y \in ℝ \forall w \in K (U {normOp}_{OLD} W) (w) \leq y)$
100	95 96 99	mp3an12	$⊢ K \subseteq U BLnOp W \to (\forall x \in X \exists z \in ℝ \forall w \in K \|w (x)\| \leq z \leftrightarrow \exists y \in ℝ \forall w \in K (U {normOp}_{OLD} W) (w) \leq y)$
101	93 100	syl	$⊢ φ \to (\forall x \in X \exists z \in ℝ \forall w \in K \|w (x)\| \leq z \leftrightarrow \exists y \in ℝ \forall w \in K (U {normOp}_{OLD} W) (w) \leq y)$
102	89 101	mpbid	$⊢ φ \to \exists y \in ℝ \forall w \in K (U {normOp}_{OLD} W) (w) \leq y$
103		simpr	$⊢ ((φ \land y \in ℝ) \land (x \in X \land N (x) \leq 1)) \to (x \in X \land N (x) \leq 1)$
104		fveq2	$⊢ z = x \to N (z) = N (x)$
105	104	breq1d	$⊢ z = x \to (N (z) \leq 1 \leftrightarrow N (x) \leq 1)$
106	105	elrab	$⊢ x \in \{z \in X \| N (z) \leq 1\} \leftrightarrow (x \in X \land N (x) \leq 1)$
107	103 106	sylibr	$⊢ ((φ \land y \in ℝ) \land (x \in X \land N (x) \leq 1)) \to x \in \{z \in X \| N (z) \leq 1\}$
108	10 25	dmmptd	$⊢ φ \to dom F = X$
109	108	eleq2d	$⊢ φ \to (x \in dom F \leftrightarrow x \in X)$
110	109	biimpar	$⊢ (φ \land x \in X) \to x \in dom F$
111		funfvima	$⊢ (Fun F \land x \in dom F) \to (x \in \{z \in X \| N (z) \leq 1\} \to F (x) \in F [\{z \in X \| N (z) \leq 1\}])$
112	27 111	sylan	$⊢ (φ \land x \in dom F) \to (x \in \{z \in X \| N (z) \leq 1\} \to F (x) \in F [\{z \in X \| N (z) \leq 1\}])$
113	110 112	syldan	$⊢ (φ \land x \in X) \to (x \in \{z \in X \| N (z) \leq 1\} \to F (x) \in F [\{z \in X \| N (z) \leq 1\}])$
114	113	ad2ant2r	$⊢ ((φ \land y \in ℝ) \land (x \in X \land N (x) \leq 1)) \to (x \in \{z \in X \| N (z) \leq 1\} \to F (x) \in F [\{z \in X \| N (z) \leq 1\}])$
115	107 114	mpd	$⊢ ((φ \land y \in ℝ) \land (x \in X \land N (x) \leq 1)) \to F (x) \in F [\{z \in X \| N (z) \leq 1\}]$
116	115 11	eleqtrrdi	$⊢ ((φ \land y \in ℝ) \land (x \in X \land N (x) \leq 1)) \to F (x) \in K$
117		fveq2	$⊢ w = F (x) \to (U {normOp}_{OLD} W) (w) = (U {normOp}_{OLD} W) (F (x))$
118	117	breq1d	$⊢ w = F (x) \to ((U {normOp}_{OLD} W) (w) \leq y \leftrightarrow (U {normOp}_{OLD} W) (F (x)) \leq y)$
119	118	rspcv	$⊢ F (x) \in K \to (\forall w \in K (U {normOp}_{OLD} W) (w) \leq y \to (U {normOp}_{OLD} W) (F (x)) \leq y)$
120	116 119	syl	$⊢ ((φ \land y \in ℝ) \land (x \in X \land N (x) \leq 1)) \to (\forall w \in K (U {normOp}_{OLD} W) (w) \leq y \to (U {normOp}_{OLD} W) (F (x)) \leq y)$
121	18	ad2ant2r	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to N (T (x)) \in ℝ$
122	121 121	remulcld	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to N (T (x)) N (T (x)) \in ℝ$
123	26	ffvelcdmda	$⊢ (φ \land x \in X) \to F (x) \in (U BLnOp W)$
124	7	cnnvba	$⊢ ℂ = BaseSet (W)$
125	1 124 98 22	nmblore	$⊢ (U \in NrmCVec \land W \in NrmCVec \land F (x) \in (U BLnOp W)) \to (U {normOp}_{OLD} W) (F (x)) \in ℝ$
126	12 96 125	mp3an12	$⊢ F (x) \in (U BLnOp W) \to (U {normOp}_{OLD} W) (F (x)) \in ℝ$
127	123 126	syl	$⊢ (φ \land x \in X) \to (U {normOp}_{OLD} W) (F (x)) \in ℝ$
128	127	ad2ant2r	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to (U {normOp}_{OLD} W) (F (x)) \in ℝ$
129	128 121	remulcld	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to (U {normOp}_{OLD} W) (F (x)) N (T (x)) \in ℝ$
130		simplr	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to y \in ℝ$
131	130 121	remulcld	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to y N (T (x)) \in ℝ$
132		fveq2	$⊢ z = x \to T (z) = T (x)$
133	132	oveq2d	$⊢ z = x \to w P T (z) = w P T (x)$
134	133	mpteq2dv	$⊢ z = x \to (w \in X ⟼ w P T (z)) = (w \in X ⟼ w P T (x))$
135	134 10 1	mptfvmpt	$⊢ x \in X \to F (x) = (w \in X ⟼ w P T (x))$
136	135	adantl	$⊢ (φ \land x \in X) \to F (x) = (w \in X ⟼ w P T (x))$
137	136	fveq1d	$⊢ (φ \land x \in X) \to F (x) (T (x)) = (w \in X ⟼ w P T (x)) (T (x))$
138		oveq1	$⊢ w = T (x) \to w P T (x) = T (x) P T (x)$
139		eqid	$⊢ (w \in X ⟼ w P T (x)) = (w \in X ⟼ w P T (x))$
140		ovex	$⊢ T (x) P T (x) \in V$
141	138 139 140	fvmpt	$⊢ T (x) \in X \to (w \in X ⟼ w P T (x)) (T (x)) = T (x) P T (x)$
142	16 141	syl	$⊢ (φ \land x \in X) \to (w \in X ⟼ w P T (x)) (T (x)) = T (x) P T (x)$
143	137 142	eqtrd	$⊢ (φ \land x \in X) \to F (x) (T (x)) = T (x) P T (x)$
144	143	ad2ant2r	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to F (x) (T (x)) = T (x) P T (x)$
145	16	ad2ant2r	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to T (x) \in X$
146	1 5 2	ipidsq	$⊢ (U \in NrmCVec \land T (x) \in X) \to T (x) P T (x) = {N (T (x))}^{2}$
147	12 145 146	sylancr	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to T (x) P T (x) = {N (T (x))}^{2}$
148	144 147	eqtrd	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to F (x) (T (x)) = {N (T (x))}^{2}$
149	148	fveq2d	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to \|F (x) (T (x))\| = \|{N (T (x))}^{2}\|$
150		resqcl	$⊢ N (T (x)) \in ℝ \to {N (T (x))}^{2} \in ℝ$
151		sqge0	$⊢ N (T (x)) \in ℝ \to 0 \leq {N (T (x))}^{2}$
152	150 151	absidd	$⊢ N (T (x)) \in ℝ \to \|{N (T (x))}^{2}\| = {N (T (x))}^{2}$
153	121 152	syl	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to \|{N (T (x))}^{2}\| = {N (T (x))}^{2}$
154	121	recnd	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to N (T (x)) \in ℂ$
155	154	sqvald	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to {N (T (x))}^{2} = N (T (x)) N (T (x))$
156	149 153 155	3eqtrd	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to \|F (x) (T (x))\| = N (T (x)) N (T (x))$
157	123	ad2ant2r	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to F (x) \in (U BLnOp W)$
158	1 5 97 98 22 12 96	nmblolbi	$⊢ (F (x) \in (U BLnOp W) \land T (x) \in X) \to \|F (x) (T (x))\| \leq (U {normOp}_{OLD} W) (F (x)) N (T (x))$
159	157 145 158	syl2anc	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to \|F (x) (T (x))\| \leq (U {normOp}_{OLD} W) (F (x)) N (T (x))$
160	156 159	eqbrtrrd	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to N (T (x)) N (T (x)) \leq (U {normOp}_{OLD} W) (F (x)) N (T (x))$
161	12 145 67	sylancr	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to 0 \leq N (T (x))$
162		simprr	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to (U {normOp}_{OLD} W) (F (x)) \leq y$
163	128 130 121 161 162	lemul1ad	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to (U {normOp}_{OLD} W) (F (x)) N (T (x)) \leq y N (T (x))$
164	122 129 131 160 163	letrd	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to N (T (x)) N (T (x)) \leq y N (T (x))$
165		lemul1	$⊢ (N (T (x)) \in ℝ \land y \in ℝ \land (N (T (x)) \in ℝ \land 0 < N (T (x)))) \to (N (T (x)) \leq y \leftrightarrow N (T (x)) N (T (x)) \leq y N (T (x)))$
166	165	biimprd	$⊢ (N (T (x)) \in ℝ \land y \in ℝ \land (N (T (x)) \in ℝ \land 0 < N (T (x)))) \to (N (T (x)) N (T (x)) \leq y N (T (x)) \to N (T (x)) \leq y)$
167	166	3expia	$⊢ (N (T (x)) \in ℝ \land y \in ℝ) \to ((N (T (x)) \in ℝ \land 0 < N (T (x))) \to (N (T (x)) N (T (x)) \leq y N (T (x)) \to N (T (x)) \leq y))$
168	167	expdimp	$⊢ ((N (T (x)) \in ℝ \land y \in ℝ) \land N (T (x)) \in ℝ) \to (0 < N (T (x)) \to (N (T (x)) N (T (x)) \leq y N (T (x)) \to N (T (x)) \leq y))$
169	121 130 121 168	syl21anc	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to (0 < N (T (x)) \to (N (T (x)) N (T (x)) \leq y N (T (x)) \to N (T (x)) \leq y))$
170	164 169	mpid	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to (0 < N (T (x)) \to N (T (x)) \leq y)$
171		0red	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to 0 \in ℝ$
172	1 124 22	blof	$⊢ (U \in NrmCVec \land W \in NrmCVec \land F (x) \in (U BLnOp W)) \to F (x) : X ⟶ ℂ$
173	12 96 172	mp3an12	$⊢ F (x) \in (U BLnOp W) \to F (x) : X ⟶ ℂ$
174	123 173	syl	$⊢ (φ \land x \in X) \to F (x) : X ⟶ ℂ$
175	174	ad2ant2r	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to F (x) : X ⟶ ℂ$
176	1 124 98	nmooge0	$⊢ (U \in NrmCVec \land W \in NrmCVec \land F (x) : X ⟶ ℂ) \to 0 \leq (U {normOp}_{OLD} W) (F (x))$
177	12 96 176	mp3an12	$⊢ F (x) : X ⟶ ℂ \to 0 \leq (U {normOp}_{OLD} W) (F (x))$
178	175 177	syl	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to 0 \leq (U {normOp}_{OLD} W) (F (x))$
179	171 128 130 178 162	letrd	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to 0 \leq y$
180		breq1	$⊢ 0 = N (T (x)) \to (0 \leq y \leftrightarrow N (T (x)) \leq y)$
181	179 180	syl5ibcom	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to (0 = N (T (x)) \to N (T (x)) \leq y)$
182		0re	$⊢ 0 \in ℝ$
183		leloe	$⊢ (0 \in ℝ \land N (T (x)) \in ℝ) \to (0 \leq N (T (x)) \leftrightarrow (0 < N (T (x)) \lor 0 = N (T (x))))$
184	182 121 183	sylancr	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to (0 \leq N (T (x)) \leftrightarrow (0 < N (T (x)) \lor 0 = N (T (x))))$
185	161 184	mpbid	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to (0 < N (T (x)) \lor 0 = N (T (x)))$
186	170 181 185	mpjaod	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to N (T (x)) \leq y$
187	186	expr	$⊢ ((φ \land y \in ℝ) \land x \in X) \to ((U {normOp}_{OLD} W) (F (x)) \leq y \to N (T (x)) \leq y)$
188	187	adantrr	$⊢ ((φ \land y \in ℝ) \land (x \in X \land N (x) \leq 1)) \to ((U {normOp}_{OLD} W) (F (x)) \leq y \to N (T (x)) \leq y)$
189	120 188	syld	$⊢ ((φ \land y \in ℝ) \land (x \in X \land N (x) \leq 1)) \to (\forall w \in K (U {normOp}_{OLD} W) (w) \leq y \to N (T (x)) \leq y)$
190	189	expr	$⊢ ((φ \land y \in ℝ) \land x \in X) \to (N (x) \leq 1 \to (\forall w \in K (U {normOp}_{OLD} W) (w) \leq y \to N (T (x)) \leq y))$
191	190	com23	$⊢ ((φ \land y \in ℝ) \land x \in X) \to (\forall w \in K (U {normOp}_{OLD} W) (w) \leq y \to (N (x) \leq 1 \to N (T (x)) \leq y))$
192	191	ralrimdva	$⊢ (φ \land y \in ℝ) \to (\forall w \in K (U {normOp}_{OLD} W) (w) \leq y \to \forall x \in X (N (x) \leq 1 \to N (T (x)) \leq y))$
193	192	reximdva	$⊢ φ \to (\exists y \in ℝ \forall w \in K (U {normOp}_{OLD} W) (w) \leq y \to \exists y \in ℝ \forall x \in X (N (x) \leq 1 \to N (T (x)) \leq y))$
194	102 193	mpd	$⊢ φ \to \exists y \in ℝ \forall x \in X (N (x) \leq 1 \to N (T (x)) \leq y)$
195		eqid	$⊢ U {normOp}_{OLD} U = U {normOp}_{OLD} U$
196	1 1 5 5 195 12 12	nmobndi	$⊢ T : X ⟶ X \to ((U {normOp}_{OLD} U) (T) \in ℝ \leftrightarrow \exists y \in ℝ \forall x \in X (N (x) \leq 1 \to N (T (x)) \leq y))$
197	15 196	syl	$⊢ φ \to ((U {normOp}_{OLD} U) (T) \in ℝ \leftrightarrow \exists y \in ℝ \forall x \in X (N (x) \leq 1 \to N (T (x)) \leq y))$
198	194 197	mpbird	$⊢ φ \to (U {normOp}_{OLD} U) (T) \in ℝ$
199		ltpnf	$⊢ (U {normOp}_{OLD} U) (T) \in ℝ \to (U {normOp}_{OLD} U) (T) < +∞$
200	198 199	syl	$⊢ φ \to (U {normOp}_{OLD} U) (T) < +∞$
201	195 3 4	isblo	$⊢ (U \in NrmCVec \land U \in NrmCVec) \to (T \in B \leftrightarrow (T \in L \land (U {normOp}_{OLD} U) (T) < +∞))$
202	12 12 201	mp2an	$⊢ T \in B \leftrightarrow (T \in L \land (U {normOp}_{OLD} U) (T) < +∞)$
203	8 200 202	sylanbrc	$⊢ φ \to T \in B$

Metamath Proof Explorer

Theorem htthlem

Proof