Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem nmoub3i 8368

Description: An upper bound for an operator norm.

Hypotheses

Ref	Expression
nmoubi.1	Base
nmoubi.y	Base
nmoubi.l
nmoubi.m
nmoubi.3	normOp
nmoubi.u	NrmCVec
nmoubi.w	NrmCVec

Assertion

Ref	Expression
nmoub3i

Distinct variable groups:   ,   ,   ,   ,   ,   ,

---

Proof of Theorem nmoub3i

Step	Hyp	Ref	Expression
1		axmulrcl 5246	. . . . . . . . . . . 12
2		nmoubi.u	. . . . . . . . . . . . 13 NrmCVec
3		nmoubi.1	. . . . . . . . . . . . . 14 Base
4		nmoubi.l	. . . . . . . . . . . . . 14
5	3, 4	nvcl 8227	. . . . . . . . . . . . 13 NrmCVec
6	2, 5	mpan 693	. . . . . . . . . . . 12
7	1, 6	sylan2 451	. . . . . . . . . . 11
8	7	adantr 389	. . . . . . . . . 10
9		axmulrcl 5246	. . . . . . . . . . . 12
10		recnt 5285	. . . . . . . . . . . . 13
11		absclt 6768	. . . . . . . . . . . . 13
12	10, 11	syl 10	. . . . . . . . . . . 12
13	9, 12, 6	syl2an 454	. . . . . . . . . . 11
14	13	adantr 389	. . . . . . . . . 10
15	12	ad2antrr 404	. . . . . . . . . 10
16		lemul1it 5793	. . . . . . . . . . . 12
17		pm3.26 319	. . . . . . . . . . . . 13
18	12	adantr 389	. . . . . . . . . . . . 13
19	3, 4	nvge0 8241	. . . . . . . . . . . . . . . 16 NrmCVec
20	2, 19	mpan 693	. . . . . . . . . . . . . . 15
21	6, 20	jca 288	. . . . . . . . . . . . . 14
22	21	adantl 388	. . . . . . . . . . . . 13
23	17, 18, 22	3jca 817	. . . . . . . . . . . 12
24		leabst 6799	. . . . . . . . . . . . 13
25	24	adantr 389	. . . . . . . . . . . 12
26	16, 23, 25	sylanc 471	. . . . . . . . . . 11
27	26	adantr 389	. . . . . . . . . 10
28		lemul2it 5795	. . . . . . . . . . . 12
29	6	adantl 388	. . . . . . . . . . . . 13
30		1re 5407	. . . . . . . . . . . . . 14
31	30	a1i 8	. . . . . . . . . . . . 13
32		absge0t 6789	. . . . . . . . . . . . . . . 16
33	10, 32	syl 10	. . . . . . . . . . . . . . 15
34	33	adantr 389	. . . . . . . . . . . . . 14
35	18, 34	jca 288	. . . . . . . . . . . . 13
36	29, 31, 35	3jca 817	. . . . . . . . . . . 12
37	28, 36	sylan 448	. . . . . . . . . . 11
38	12	recnd 5287	. . . . . . . . . . . . 13
39		ax1id 5254	. . . . . . . . . . . . 13
40	38, 39	syl 10	. . . . . . . . . . . 12
41	40	ad2antrr 404	. . . . . . . . . . 11
42	37, 41	breqtrd 2629	. . . . . . . . . 10
43	8, 14, 15, 27, 42	letrd 5499	. . . . . . . . 9
44	43	adantlll 396	. . . . . . . 8
45		letrt 5498	. . . . . . . . . 10
46		ffvelrn 3799	. . . . . . . . . . . 12
47		nmoubi.w	. . . . . . . . . . . . 13 NrmCVec
48		nmoubi.y	. . . . . . . . . . . . . 14 Base
49		nmoubi.m	. . . . . . . . . . . . . 14
50	48, 49	nvcl 8227	. . . . . . . . . . . . 13 NrmCVec
51	47, 50	mpan 693	. . . . . . . . . . . 12
52	46, 51	syl 10	. . . . . . . . . . 11
53	52	adantlr 393	. . . . . . . . . 10
54	7	adantll 392	. . . . . . . . . 10
55	12	ad2antlr 405	. . . . . . . . . 10
56	45, 53, 54, 55	syl3anc 856	. . . . . . . . 9
57	56	adantr 389	. . . . . . . 8
58	44, 57	mpan2d 700	. . . . . . 7
59	58	ex 373	. . . . . 6
60	59	com23 32	. . . . 5
61	60	r19.20dva 1701	. . . 4