Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem ubthlem10 8469

Description: Lemma for ubthi 8475. Upper limit for the norm of an operator value at auxiliary vector .

Hypotheses

Ref	Expression
ubthlem10.1	Base
ubthlem10.2	Base
ubthlem10.3
ubthlem10.4	normOp
ubthlem10.5	BLnOp
ubthlem10.6
ubthlem10.7	NrmCVec
ubthlem10.8	NrmCVec
ubthlem10.9	IndMet
ubthlem10.n
ubthlem10.g
ubthlem10.m
ubthlem10.r
ubthlem10.z
ubthlem10.11
ubthlem10.q

Assertion

Ref	Expression
ubthlem10	ball

Distinct variable groups:   ,,,,,   ,,,,,   ,   ,,,,,,,   ,,,   ,,,   ,,,,,,,,,   ,   ,   ,,,,,,,

---

Proof of Theorem ubthlem10

Step	Hyp	Ref	Expression
1		ubthlem10.1	. . . . . . . 8 Base
2		ubthlem10.11	. . . . . . . 8
3	1, 2	ubthlem1 8460	. . . . . . 7
4	3	pm3.27bda 421	. . . . . 6
5	4	ex 373	. . . . 5
6		ra4 1686	. . . . 5
7	5, 6	syl6com 53	. . . 4
8	7	com3l 34	. . 3
9	8	imp31 362	. 2
10		ssel 2053	. . . 4 ball ball
11	10	impcom 351	. . 3 ball ball
12		ubthlem10.7	. . . . . . . . . . . . 13 NrmCVec
13		ubthlem10.r	. . . . . . . . . . . . . 14
14	1, 13	nvsass 8189	. . . . . . . . . . . . 13 NrmCVec
15	12, 14	mpan 693	. . . . . . . . . . . 12
16		rehalfclt 5981	. . . . . . . . . . . . . 14
17	16	recnd 5287	. . . . . . . . . . . . 13
18	17	adantr 389	. . . . . . . . . . . 12
19		rerecclt 5759	. . . . . . . . . . . . . . 15
20		ubthlem10.n	. . . . . . . . . . . . . . . . . 18
21	1, 20	nvcl 8227	. . . . . . . . . . . . . . . . 17 NrmCVec
22	12, 21	mpan 693	. . . . . . . . . . . . . . . 16
23	22	adantr 389	. . . . . . . . . . . . . . 15
24		ubthlem10.z	. . . . . . . . . . . . . . . . . . 19
25	1, 24, 20	nvz 8236	. . . . . . . . . . . . . . . . . 18 NrmCVec
26	12, 25	mpan 693	. . . . . . . . . . . . . . . . 17
27	26	necon3bid 1593	. . . . . . . . . . . . . . . 16
28	27	biimpar 417	. . . . . . . . . . . . . . 15
29	19, 23, 28	sylanc 471	. . . . . . . . . . . . . 14
30	29	recnd 5287	. . . . . . . . . . . . 13
31	30	adantl 388	. . . . . . . . . . . 12
32		simprl 414	. . . . . . . . . . . 12
33	15, 18, 31, 32	syl3anc 856	. . . . . . . . . . 11
34	33	adantlr 393	. . . . . . . . . 10
35	34	fveq2d 3713	. . . . . . . . 9
36	1, 13, 20	nvsge0 8230	. . . . . . . . . . 11 NrmCVec
37	12, 36	mp3an1 900	. . . . . . . . . 10
38	16	adantr 389	. . . . . . . . . . 11
39		halfpos2t 5984	. . . . . . . . . . . . 13
40	39	biimpa 416	. . . . . . . . . . . 12
41		0re 5412	. . . . . . . . . . . . . . 15
42		ltlet 5493	. . . . . . . . . . . . . . 15
43	41, 42	mpan 693	. . . . . . . . . . . . . 14
44	16, 43	syl 10	. . . . . . . . . . . . 13
45	44	adantr 389	. . . . . . . . . . . 12
46	40, 45	mpd 26	. . . . . . . . . . 11
47	38, 46	jca 288	. . . . . . . . . 10
48	1, 13	nvscl 8187	. . . . . . . . . . . 12 NrmCVec
49	12, 48	mp3an1 900	. . . . . . . . . . 11
50		pm3.26 319	. . . . . . . . . . 11
51	49, 30, 50	sylanc 471	. . . . . . . . . 10
52	37, 47, 51	syl2an 454	. . . . . . . . 9
53	35, 52	eqtrd 1499	. . . . . . . 8