Metamath Proof Explorer


Theorem nmoix

Description: The operator norm is a bound on the size of an operator, even when it is infinite (using extended real multiplication). (Contributed by Mario Carneiro, 18-Oct-2015)

Ref Expression
Hypotheses nmofval.1 N = S normOp T
nmoi.2 V = Base S
nmoi.3 L = norm S
nmoi.4 M = norm T
Assertion nmoix S NrmGrp T NrmGrp F S GrpHom T X V M F X N F 𝑒 L X

Proof

Step Hyp Ref Expression
1 nmofval.1 N = S normOp T
2 nmoi.2 V = Base S
3 nmoi.3 L = norm S
4 nmoi.4 M = norm T
5 1 isnghm2 S NrmGrp T NrmGrp F S GrpHom T F S NGHom T N F
6 5 biimpar S NrmGrp T NrmGrp F S GrpHom T N F F S NGHom T
7 1 2 3 4 nmoi F S NGHom T X V M F X N F L X
8 6 7 sylan S NrmGrp T NrmGrp F S GrpHom T N F X V M F X N F L X
9 8 an32s S NrmGrp T NrmGrp F S GrpHom T X V N F M F X N F L X
10 id N F N F
11 2 3 nmcl S NrmGrp X V L X
12 11 3ad2antl1 S NrmGrp T NrmGrp F S GrpHom T X V L X
13 rexmul N F L X N F 𝑒 L X = N F L X
14 10 12 13 syl2anr S NrmGrp T NrmGrp F S GrpHom T X V N F N F 𝑒 L X = N F L X
15 9 14 breqtrrd S NrmGrp T NrmGrp F S GrpHom T X V N F M F X N F 𝑒 L X
16 fveq2 X = 0 S F X = F 0 S
17 16 fveq2d X = 0 S M F X = M F 0 S
18 fveq2 X = 0 S L X = L 0 S
19 18 oveq2d X = 0 S +∞ 𝑒 L X = +∞ 𝑒 L 0 S
20 17 19 breq12d X = 0 S M F X +∞ 𝑒 L X M F 0 S +∞ 𝑒 L 0 S
21 simpl2 S NrmGrp T NrmGrp F S GrpHom T X V T NrmGrp
22 eqid Base T = Base T
23 2 22 ghmf F S GrpHom T F : V Base T
24 23 ffvelrnda F S GrpHom T X V F X Base T
25 24 3ad2antl3 S NrmGrp T NrmGrp F S GrpHom T X V F X Base T
26 22 4 nmcl T NrmGrp F X Base T M F X
27 21 25 26 syl2anc S NrmGrp T NrmGrp F S GrpHom T X V M F X
28 27 adantr S NrmGrp T NrmGrp F S GrpHom T X V X 0 S M F X
29 28 rexrd S NrmGrp T NrmGrp F S GrpHom T X V X 0 S M F X *
30 pnfge M F X * M F X +∞
31 29 30 syl S NrmGrp T NrmGrp F S GrpHom T X V X 0 S M F X +∞
32 simp1 S NrmGrp T NrmGrp F S GrpHom T S NrmGrp
33 eqid 0 S = 0 S
34 2 3 33 nmrpcl S NrmGrp X V X 0 S L X +
35 34 3expa S NrmGrp X V X 0 S L X +
36 32 35 sylanl1 S NrmGrp T NrmGrp F S GrpHom T X V X 0 S L X +
37 rpxr L X + L X *
38 rpgt0 L X + 0 < L X
39 xmulpnf2 L X * 0 < L X +∞ 𝑒 L X = +∞
40 37 38 39 syl2anc L X + +∞ 𝑒 L X = +∞
41 36 40 syl S NrmGrp T NrmGrp F S GrpHom T X V X 0 S +∞ 𝑒 L X = +∞
42 31 41 breqtrrd S NrmGrp T NrmGrp F S GrpHom T X V X 0 S M F X +∞ 𝑒 L X
43 0le0 0 0
44 simpl3 S NrmGrp T NrmGrp F S GrpHom T X V F S GrpHom T
45 eqid 0 T = 0 T
46 33 45 ghmid F S GrpHom T F 0 S = 0 T
47 44 46 syl S NrmGrp T NrmGrp F S GrpHom T X V F 0 S = 0 T
48 47 fveq2d S NrmGrp T NrmGrp F S GrpHom T X V M F 0 S = M 0 T
49 4 45 nm0 T NrmGrp M 0 T = 0
50 21 49 syl S NrmGrp T NrmGrp F S GrpHom T X V M 0 T = 0
51 48 50 eqtrd S NrmGrp T NrmGrp F S GrpHom T X V M F 0 S = 0
52 simpl1 S NrmGrp T NrmGrp F S GrpHom T X V S NrmGrp
53 3 33 nm0 S NrmGrp L 0 S = 0
54 52 53 syl S NrmGrp T NrmGrp F S GrpHom T X V L 0 S = 0
55 54 oveq2d S NrmGrp T NrmGrp F S GrpHom T X V +∞ 𝑒 L 0 S = +∞ 𝑒 0
56 pnfxr +∞ *
57 xmul01 +∞ * +∞ 𝑒 0 = 0
58 56 57 ax-mp +∞ 𝑒 0 = 0
59 55 58 syl6eq S NrmGrp T NrmGrp F S GrpHom T X V +∞ 𝑒 L 0 S = 0
60 51 59 breq12d S NrmGrp T NrmGrp F S GrpHom T X V M F 0 S +∞ 𝑒 L 0 S 0 0
61 43 60 mpbiri S NrmGrp T NrmGrp F S GrpHom T X V M F 0 S +∞ 𝑒 L 0 S
62 20 42 61 pm2.61ne S NrmGrp T NrmGrp F S GrpHom T X V M F X +∞ 𝑒 L X
63 62 adantr S NrmGrp T NrmGrp F S GrpHom T X V N F = +∞ M F X +∞ 𝑒 L X
64 simpr S NrmGrp T NrmGrp F S GrpHom T X V N F = +∞ N F = +∞
65 64 oveq1d S NrmGrp T NrmGrp F S GrpHom T X V N F = +∞ N F 𝑒 L X = +∞ 𝑒 L X
66 63 65 breqtrrd S NrmGrp T NrmGrp F S GrpHom T X V N F = +∞ M F X N F 𝑒 L X
67 1 nmocl S NrmGrp T NrmGrp F S GrpHom T N F *
68 1 nmoge0 S NrmGrp T NrmGrp F S GrpHom T 0 N F
69 ge0nemnf N F * 0 N F N F −∞
70 67 68 69 syl2anc S NrmGrp T NrmGrp F S GrpHom T N F −∞
71 67 70 jca S NrmGrp T NrmGrp F S GrpHom T N F * N F −∞
72 xrnemnf N F * N F −∞ N F N F = +∞
73 71 72 sylib S NrmGrp T NrmGrp F S GrpHom T N F N F = +∞
74 73 adantr S NrmGrp T NrmGrp F S GrpHom T X V N F N F = +∞
75 15 66 74 mpjaodan S NrmGrp T NrmGrp F S GrpHom T X V M F X N F 𝑒 L X