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

Theorem nmoolb 22264
 Description: A lower bound for an operator norm. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
Hypotheses
Ref Expression
nmolb.1
nmolb.2
nmolb.l CV
nmolb.m CV
nmolb.3
Assertion
Ref Expression
nmoolb

Proof of Theorem nmoolb
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nmolb.2 . . . . . 6
2 nmolb.m . . . . . 6 CV
31, 2nmosetre 22257 . . . . 5
4 ressxr 9121 . . . . 5
53, 4syl6ss 3352 . . . 4
7 fveq2 5720 . . . . . . . 8
87breq1d 4214 . . . . . . 7
9 fveq2 5720 . . . . . . . . 9
109fveq2d 5724 . . . . . . . 8
1110eqeq2d 2446 . . . . . . 7
128, 11anbi12d 692 . . . . . 6
13 eqid 2435 . . . . . . 7
1413biantru 492 . . . . . 6
1512, 14syl6bbr 255 . . . . 5
1615rspcev 3044 . . . 4
17 fvex 5734 . . . . 5
18 eqeq1 2441 . . . . . . 7
1918anbi2d 685 . . . . . 6
2019rexbidv 2718 . . . . 5
2117, 20elab 3074 . . . 4
2216, 21sylibr 204 . . 3
23 supxrub 10895 . . 3
246, 22, 23syl2an 464 . 2
25 nmolb.1 . . . 4
26 nmolb.l . . . 4 CV
27 nmolb.3 . . . 4
2825, 1, 26, 2, 27nmooval 22256 . . 3