Metamath Proof Explorer


Theorem nmfnleub

Description: An upper bound for the norm of a functional. (Contributed by NM, 24-May-2006) (Revised by Mario Carneiro, 7-Sep-2014) (New usage is discouraged.)

Ref Expression
Assertion nmfnleub T : A * norm fn T A x norm x 1 T x A

Proof

Step Hyp Ref Expression
1 nmfnval T : norm fn T = sup y | x norm x 1 y = T x * <
2 1 adantr T : A * norm fn T = sup y | x norm x 1 y = T x * <
3 2 breq1d T : A * norm fn T A sup y | x norm x 1 y = T x * < A
4 nmfnsetre T : y | x norm x 1 y = T x
5 ressxr *
6 4 5 sstrdi T : y | x norm x 1 y = T x *
7 supxrleub y | x norm x 1 y = T x * A * sup y | x norm x 1 y = T x * < A z y | x norm x 1 y = T x z A
8 6 7 sylan T : A * sup y | x norm x 1 y = T x * < A z y | x norm x 1 y = T x z A
9 ancom norm x 1 y = T x y = T x norm x 1
10 eqeq1 y = z y = T x z = T x
11 10 anbi1d y = z y = T x norm x 1 z = T x norm x 1
12 9 11 syl5bb y = z norm x 1 y = T x z = T x norm x 1
13 12 rexbidv y = z x norm x 1 y = T x x z = T x norm x 1
14 13 ralab z y | x norm x 1 y = T x z A z x z = T x norm x 1 z A
15 ralcom4 x z z = T x norm x 1 z A z x z = T x norm x 1 z A
16 impexp z = T x norm x 1 z A z = T x norm x 1 z A
17 16 albii z z = T x norm x 1 z A z z = T x norm x 1 z A
18 fvex T x V
19 breq1 z = T x z A T x A
20 19 imbi2d z = T x norm x 1 z A norm x 1 T x A
21 18 20 ceqsalv z z = T x norm x 1 z A norm x 1 T x A
22 17 21 bitri z z = T x norm x 1 z A norm x 1 T x A
23 22 ralbii x z z = T x norm x 1 z A x norm x 1 T x A
24 r19.23v x z = T x norm x 1 z A x z = T x norm x 1 z A
25 24 albii z x z = T x norm x 1 z A z x z = T x norm x 1 z A
26 15 23 25 3bitr3i x norm x 1 T x A z x z = T x norm x 1 z A
27 14 26 bitr4i z y | x norm x 1 y = T x z A x norm x 1 T x A
28 8 27 bitrdi T : A * sup y | x norm x 1 y = T x * < A x norm x 1 T x A
29 3 28 bitrd T : A * norm fn T A x norm x 1 T x A