# 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}\mathrm{normOp}{T}$
nmoi.2 ${⊢}{V}={\mathrm{Base}}_{{S}}$
nmoi.3 ${⊢}{L}=\mathrm{norm}\left({S}\right)$
nmoi.4 ${⊢}{M}=\mathrm{norm}\left({T}\right)$
Assertion nmoix ${⊢}\left(\left({S}\in \mathrm{NrmGrp}\wedge {T}\in \mathrm{NrmGrp}\wedge {F}\in \left({S}\mathrm{GrpHom}{T}\right)\right)\wedge {X}\in {V}\right)\to {M}\left({F}\left({X}\right)\right)\le {N}\left({F}\right){\cdot }_{𝑒}{L}\left({X}\right)$

### Proof

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