Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nmoleub Structured version   Unicode version

Theorem nmoleub 21364
 Description: The operator norm, defined as an infimum of upper bounds, can also be defined as a supremum of norms of away from zero. (Contributed by Mario Carneiro, 18-Oct-2015.)
Hypotheses
Ref Expression
nmofval.1
nmoi.2
nmoi.3
nmoi.4
nmoleub.z
nmoleub.1 NrmGrp
nmoleub.2 NrmGrp
nmoleub.3
nmoleub.4
nmoleub.5
Assertion
Ref Expression
nmoleub
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem nmoleub
StepHypRef Expression
1 nmoleub.2 . . . . . . . . 9 NrmGrp
21ad2antrr 725 . . . . . . . 8 NrmGrp
3 nmoleub.3 . . . . . . . . . . 11
4 nmoi.2 . . . . . . . . . . . 12
5 eqid 2457 . . . . . . . . . . . 12
64, 5ghmf 16398 . . . . . . . . . . 11
73, 6syl 16 . . . . . . . . . 10
87ad2antrr 725 . . . . . . . . 9
9 simprl 756 . . . . . . . . 9
10 ffvelrn 6030 . . . . . . . . 9
118, 9, 10syl2anc 661 . . . . . . . 8
12 nmoi.4 . . . . . . . . 9
135, 12nmcl 21261 . . . . . . . 8 NrmGrp
142, 11, 13syl2anc 661 . . . . . . 7
15 nmoleub.1 . . . . . . . . 9 NrmGrp
1615adantr 465 . . . . . . . 8 NrmGrp
17 nmoi.3 . . . . . . . . . 10
18 nmoleub.z . . . . . . . . . 10
194, 17, 18nmrpcl 21265 . . . . . . . . 9 NrmGrp
20193expb 1197 . . . . . . . 8 NrmGrp
2116, 20sylan 471 . . . . . . 7
2214, 21rerpdivcld 11308 . . . . . 6
2322rexrd 9660 . . . . 5
24 nmofval.1 . . . . . . . 8
2524nmocl 21353 . . . . . . 7 NrmGrp NrmGrp
2615, 1, 3, 25syl3anc 1228 . . . . . 6
2726ad2antrr 725 . . . . 5
28 nmoleub.4 . . . . . 6
2928ad2antrr 725 . . . . 5
3015, 1, 33jca 1176 . . . . . . 7 NrmGrp NrmGrp
3130adantr 465 . . . . . 6 NrmGrp NrmGrp
3224, 4, 17, 12, 18nmoi2 21363 . . . . . 6 NrmGrp NrmGrp
3331, 32sylan 471 . . . . 5
34 simplr 755 . . . . 5
3523, 27, 29, 33, 34xrletrd 11390 . . . 4
3635expr 615 . . 3
3736ralrimiva 2871 . 2
38 0le0 10646 . . . . . . . . . . 11
39 simpllr 760 . . . . . . . . . . . . 13
4039recnd 9639 . . . . . . . . . . . 12
4140mul01d 9796 . . . . . . . . . . 11
4238, 41syl5breqr 4492 . . . . . . . . . 10
43 fveq2 5872 . . . . . . . . . . . . 13
443ad2antrr 725 . . . . . . . . . . . . . 14
45 eqid 2457 . . . . . . . . . . . . . . 15
4618, 45ghmid 16400 . . . . . . . . . . . . . 14
4744, 46syl 16 . . . . . . . . . . . . 13
4843, 47sylan9eqr 2520 . . . . . . . . . . . 12
4948fveq2d 5876 . . . . . . . . . . 11
501ad3antrrr 729 . . . . . . . . . . . 12 NrmGrp
5112, 45nm0 21272 . . . . . . . . . . . 12 NrmGrp
5250, 51syl 16 . . . . . . . . . . 11
5349, 52eqtrd 2498 . . . . . . . . . 10
54 fveq2 5872 . . . . . . . . . . . 12
5515ad2antrr 725 . . . . . . . . . . . . 13 NrmGrp
5617, 18nm0 21272 . . . . . . . . . . . . 13 NrmGrp
5755, 56syl 16 . . . . . . . . . . . 12
5854, 57sylan9eqr 2520 . . . . . . . . . . 11
5958oveq2d 6312 . . . . . . . . . 10
6042, 53, 593brtr4d 4486 . . . . . . . . 9
6160a1d 25 . . . . . . . 8
62 simpr 461 . . . . . . . . 9
631ad2antrr 725 . . . . . . . . . . . . 13 NrmGrp
647adantr 465 . . . . . . . . . . . . . 14
6564, 10sylan 471 . . . . . . . . . . . . 13
6663, 65, 13syl2anc 661 . . . . . . . . . . . 12
6766adantr 465 . . . . . . . . . . 11
68 simpllr 760 . . . . . . . . . . 11
6915adantr 465 . . . . . . . . . . . 12 NrmGrp
70193expa 1196 . . . . . . . . . . . 12 NrmGrp
7169, 70sylanl1 650 . . . . . . . . . . 11
7267, 68, 71ledivmul2d 11331 . . . . . . . . . 10
7372biimpd 207 . . . . . . . . 9
7462, 73embantd 54 . . . . . . . 8
7561, 74pm2.61dane 2775 . . . . . . 7
7675ralimdva 2865 . . . . . 6
771adantr 465 . . . . . . 7 NrmGrp
783adantr 465 . . . . . . 7
79 simpr 461 . . . . . . 7
80 nmoleub.5 . . . . . . . 8
8180adantr 465 . . . . . . 7
8224, 4, 17, 12nmolb 21350 . . . . . . 7 NrmGrp NrmGrp
8369, 77, 78, 79, 81, 82syl311anc 1242 . . . . . 6
8476, 83syld 44 . . . . 5
8584imp 429 . . . 4
8685an32s 804 . . 3
8726ad2antrr 725 . . . . 5
88 pnfge 11364 . . . . 5
8987, 88syl 16 . . . 4
90 simpr 461 . . . 4
9189, 90breqtrrd 4482 . . 3
92 ge0nemnf 11399 . . . . . . 7
9328, 80, 92syl2anc 661 . . . . . 6
9428, 93jca 532 . . . . 5
95 xrnemnf 11353 . . . . 5
9694, 95sylib 196 . . . 4