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

Theorem nmoolb 22120
 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 22113 . . . . 5
4 ressxr 9062 . . . . 5
53, 4syl6ss 3303 . . . 4
7 fveq2 5668 . . . . . . . 8
87breq1d 4163 . . . . . . 7
9 fveq2 5668 . . . . . . . . 9
109fveq2d 5672 . . . . . . . 8
1110eqeq2d 2398 . . . . . . 7
128, 11anbi12d 692 . . . . . 6
13 eqid 2387 . . . . . . 7
1413biantru 492 . . . . . 6
1512, 14syl6bbr 255 . . . . 5
1615rspcev 2995 . . . 4
17 fvex 5682 . . . . 5
18 eqeq1 2393 . . . . . . 7
1918anbi2d 685 . . . . . 6
2019rexbidv 2670 . . . . 5
2117, 20elab 3025 . . . 4
2216, 21sylibr 204 . . 3
23 supxrub 10835 . . 3
246, 22, 23syl2an 464 . 2
25 nmolb.1 . . . 4
26 nmolb.l . . . 4 CV
27 nmolb.3 . . . 4
2825, 1, 26, 2, 27nmooval 22112 . . 3