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		fveq2	$⊢ z = x \to N (z) = N (x)$
104	103	breq1d	$⊢ z = x \to (N (z) \leq 1 \leftrightarrow N (x) \leq 1)$
105	104	elrab	$⊢ x \in \{z \in X \| N (z) \leq 1\} \leftrightarrow (x \in X \land N (x) \leq 1)$
106	105	bilanri	$⊢ ((φ \land y \in ℝ) \land (x \in X \land N (x) \leq 1)) \to x \in \{z \in X \| N (z) \leq 1\}$
107	10 25	dmmptd	$⊢ φ \to dom F = X$
108	107	eleq2d	$⊢ φ \to (x \in dom F \leftrightarrow x \in X)$
109	108	biimpar	$⊢ (φ \land x \in X) \to x \in dom F$
110		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\}])$
111	27 110	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\}])$
112	109 111	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\}])$
113	112	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\}])$
114	106 113	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\}]$
115	114 11	eleqtrrdi	$⊢ ((φ \land y \in ℝ) \land (x \in X \land N (x) \leq 1)) \to F (x) \in K$
116		fveq2	$⊢ w = F (x) \to (U {normOp}_{OLD} W) (w) = (U {normOp}_{OLD} W) (F (x))$
117	116	breq1d	$⊢ w = F (x) \to ((U {normOp}_{OLD} W) (w) \leq y \leftrightarrow (U {normOp}_{OLD} W) (F (x)) \leq y)$
118	117	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)$
119	115 118	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)$
120	18	ad2ant2r	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to N (T (x)) \in ℝ$
121	120 120	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 ℝ$
122	26	ffvelcdmda	$⊢ (φ \land x \in X) \to F (x) \in (U BLnOp W)$
123	7	cnnvba	$⊢ ℂ = BaseSet (W)$
124	1 123 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 ℝ$
125	12 96 124	mp3an12	$⊢ F (x) \in (U BLnOp W) \to (U {normOp}_{OLD} W) (F (x)) \in ℝ$
126	122 125	syl	$⊢ (φ \land x \in X) \to (U {normOp}_{OLD} W) (F (x)) \in ℝ$
127	126	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 ℝ$
128	127 120	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 ℝ$
129		simplr	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to y \in ℝ$
130	129 120	remulcld	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to y N (T (x)) \in ℝ$
131		fveq2	$⊢ z = x \to T (z) = T (x)$
132	131	oveq2d	$⊢ z = x \to w P T (z) = w P T (x)$
133	132	mpteq2dv	$⊢ z = x \to (w \in X ⟼ w P T (z)) = (w \in X ⟼ w P T (x))$
134	133 10 1	mptfvmpt	$⊢ x \in X \to F (x) = (w \in X ⟼ w P T (x))$
135	134	adantl	$⊢ (φ \land x \in X) \to F (x) = (w \in X ⟼ w P T (x))$
136	135	fveq1d	$⊢ (φ \land x \in X) \to F (x) (T (x)) = (w \in X ⟼ w P T (x)) (T (x))$
137		oveq1	$⊢ w = T (x) \to w P T (x) = T (x) P T (x)$
138		eqid	$⊢ (w \in X ⟼ w P T (x)) = (w \in X ⟼ w P T (x))$
139		ovex	$⊢ T (x) P T (x) \in V$
140	137 138 139	fvmpt	$⊢ T (x) \in X \to (w \in X ⟼ w P T (x)) (T (x)) = T (x) P T (x)$
141	16 140	syl	$⊢ (φ \land x \in X) \to (w \in X ⟼ w P T (x)) (T (x)) = T (x) P T (x)$
142	136 141	eqtrd	$⊢ (φ \land x \in X) \to F (x) (T (x)) = T (x) P T (x)$
143	142	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)$
144	16	ad2ant2r	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to T (x) \in X$
145	1 5 2	ipidsq	$⊢ (U \in NrmCVec \land T (x) \in X) \to T (x) P T (x) = {N (T (x))}^{2}$
146	12 144 145	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}$
147	143 146	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}$
148	147	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}\|$
149		resqcl	$⊢ N (T (x)) \in ℝ \to {N (T (x))}^{2} \in ℝ$
150		sqge0	$⊢ N (T (x)) \in ℝ \to 0 \leq {N (T (x))}^{2}$
151	149 150	absidd	$⊢ N (T (x)) \in ℝ \to \|{N (T (x))}^{2}\| = {N (T (x))}^{2}$
152	120 151	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}$
153	120	recnd	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to N (T (x)) \in ℂ$
154	153	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))$
155	148 152 154	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))$
156	122	ad2ant2r	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to F (x) \in (U BLnOp W)$
157	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))$
158	156 144 157	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))$
159	155 158	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))$
160	12 144 67	sylancr	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to 0 \leq N (T (x))$
161		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$
162	127 129 120 160 161	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))$
163	121 128 130 159 162	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))$
164		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)))$
165	164	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)$
166	165	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))$
167	166	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))$
168	120 129 120 167	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))$
169	163 168	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)$
170		0red	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to 0 \in ℝ$
171	1 123 22	blof	$⊢ (U \in NrmCVec \land W \in NrmCVec \land F (x) \in (U BLnOp W)) \to F (x) : X ⟶ ℂ$
172	12 96 171	mp3an12	$⊢ F (x) \in (U BLnOp W) \to F (x) : X ⟶ ℂ$
173	122 172	syl	$⊢ (φ \land x \in X) \to F (x) : X ⟶ ℂ$
174	173	ad2ant2r	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to F (x) : X ⟶ ℂ$
175	1 123 98	nmooge0	$⊢ (U \in NrmCVec \land W \in NrmCVec \land F (x) : X ⟶ ℂ) \to 0 \leq (U {normOp}_{OLD} W) (F (x))$
176	12 96 175	mp3an12	$⊢ F (x) : X ⟶ ℂ \to 0 \leq (U {normOp}_{OLD} W) (F (x))$
177	174 176	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))$
178	170 127 129 177 161	letrd	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to 0 \leq y$
179		breq1	$⊢ 0 = N (T (x)) \to (0 \leq y \leftrightarrow N (T (x)) \leq y)$
180	178 179	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)$
181		0re	$⊢ 0 \in ℝ$
182		leloe	$⊢ (0 \in ℝ \land N (T (x)) \in ℝ) \to (0 \leq N (T (x)) \leftrightarrow (0 < N (T (x)) \lor 0 = N (T (x))))$
183	181 120 182	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))))$
184	160 183	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)))$
185	169 180 184	mpjaod	$⊢ ((φ \land y \in ℝ) \land (x \in X \land (U {normOp}_{OLD} W) (F (x)) \leq y)) \to N (T (x)) \leq y$
186	185	expr	$⊢ ((φ \land y \in ℝ) \land x \in X) \to ((U {normOp}_{OLD} W) (F (x)) \leq y \to N (T (x)) \leq y)$
187	186	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)$
188	119 187	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)$
189	188	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))$
190	189	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))$
191	190	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))$
192	191	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))$
193	102 192	mpd	$⊢ φ \to \exists y \in ℝ \forall x \in X (N (x) \leq 1 \to N (T (x)) \leq y)$
194		eqid	$⊢ U {normOp}_{OLD} U = U {normOp}_{OLD} U$
195	1 1 5 5 194 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))$
196	15 195	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))$
197	193 196	mpbird	$⊢ φ \to (U {normOp}_{OLD} U) (T) \in ℝ$
198		ltpnf	$⊢ (U {normOp}_{OLD} U) (T) \in ℝ \to (U {normOp}_{OLD} U) (T) < +∞$
199	197 198	syl	$⊢ φ \to (U {normOp}_{OLD} U) (T) < +∞$
200	194 3 4	isblo	$⊢ (U \in NrmCVec \land U \in NrmCVec) \to (T \in B \leftrightarrow (T \in L \land (U {normOp}_{OLD} U) (T) < +∞))$
201	12 12 200	mp2an	$⊢ T \in B \leftrightarrow (T \in L \land (U {normOp}_{OLD} U) (T) < +∞)$
202	8 199 201	sylanbrc	$⊢ φ \to T \in B$

Metamath Proof Explorer

Theorem htthlem

Proof