# Metamath Proof Explorer

Description: Lemma for cnlnadji . Helper lemma to show that F is continuous. (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypotheses cnlnadjlem.1 ${⊢}{T}\in \mathrm{LinOp}$
cnlnadjlem.2 ${⊢}{T}\in \mathrm{ContOp}$
cnlnadjlem.3 ${⊢}{G}=\left({g}\in ℋ⟼{T}\left({g}\right){\cdot }_{\mathrm{ih}}{y}\right)$
cnlnadjlem.4 ${⊢}{B}=\left(\iota {w}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{y}={v}{\cdot }_{\mathrm{ih}}{w}\right)$
cnlnadjlem.5 ${⊢}{F}=\left({y}\in ℋ⟼{B}\right)$
Assertion cnlnadjlem7 ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({F}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 cnlnadjlem.1 ${⊢}{T}\in \mathrm{LinOp}$
2 cnlnadjlem.2 ${⊢}{T}\in \mathrm{ContOp}$
3 cnlnadjlem.3 ${⊢}{G}=\left({g}\in ℋ⟼{T}\left({g}\right){\cdot }_{\mathrm{ih}}{y}\right)$
4 cnlnadjlem.4 ${⊢}{B}=\left(\iota {w}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{y}={v}{\cdot }_{\mathrm{ih}}{w}\right)$
5 cnlnadjlem.5 ${⊢}{F}=\left({y}\in ℋ⟼{B}\right)$
6 breq1 ${⊢}{norm}_{ℎ}\left({F}\left({A}\right)\right)=0\to \left({norm}_{ℎ}\left({F}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)↔0\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)\right)$
7 1 2 3 4 5 cnlnadjlem4 ${⊢}{A}\in ℋ\to {F}\left({A}\right)\in ℋ$
8 1 lnopfi ${⊢}{T}:ℋ⟶ℋ$
9 8 ffvelrni ${⊢}{F}\left({A}\right)\in ℋ\to {T}\left({F}\left({A}\right)\right)\in ℋ$
10 7 9 syl ${⊢}{A}\in ℋ\to {T}\left({F}\left({A}\right)\right)\in ℋ$
11 hicl ${⊢}\left({T}\left({F}\left({A}\right)\right)\in ℋ\wedge {A}\in ℋ\right)\to {T}\left({F}\left({A}\right)\right){\cdot }_{\mathrm{ih}}{A}\in ℂ$
12 10 11 mpancom ${⊢}{A}\in ℋ\to {T}\left({F}\left({A}\right)\right){\cdot }_{\mathrm{ih}}{A}\in ℂ$
13 12 abscld ${⊢}{A}\in ℋ\to \left|{T}\left({F}\left({A}\right)\right){\cdot }_{\mathrm{ih}}{A}\right|\in ℝ$
14 normcl ${⊢}{T}\left({F}\left({A}\right)\right)\in ℋ\to {norm}_{ℎ}\left({T}\left({F}\left({A}\right)\right)\right)\in ℝ$
15 10 14 syl ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({T}\left({F}\left({A}\right)\right)\right)\in ℝ$
16 normcl ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({A}\right)\in ℝ$
17 15 16 remulcld ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({T}\left({F}\left({A}\right)\right)\right){norm}_{ℎ}\left({A}\right)\in ℝ$
18 1 2 nmcopexi ${⊢}{norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
19 normcl ${⊢}{F}\left({A}\right)\in ℋ\to {norm}_{ℎ}\left({F}\left({A}\right)\right)\in ℝ$
20 7 19 syl ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({F}\left({A}\right)\right)\in ℝ$
21 remulcl ${⊢}\left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ\wedge {norm}_{ℎ}\left({F}\left({A}\right)\right)\in ℝ\right)\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({F}\left({A}\right)\right)\in ℝ$
22 18 20 21 sylancr ${⊢}{A}\in ℋ\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({F}\left({A}\right)\right)\in ℝ$
23 22 16 remulcld ${⊢}{A}\in ℋ\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({F}\left({A}\right)\right){norm}_{ℎ}\left({A}\right)\in ℝ$
24 bcs ${⊢}\left({T}\left({F}\left({A}\right)\right)\in ℋ\wedge {A}\in ℋ\right)\to \left|{T}\left({F}\left({A}\right)\right){\cdot }_{\mathrm{ih}}{A}\right|\le {norm}_{ℎ}\left({T}\left({F}\left({A}\right)\right)\right){norm}_{ℎ}\left({A}\right)$
25 10 24 mpancom ${⊢}{A}\in ℋ\to \left|{T}\left({F}\left({A}\right)\right){\cdot }_{\mathrm{ih}}{A}\right|\le {norm}_{ℎ}\left({T}\left({F}\left({A}\right)\right)\right){norm}_{ℎ}\left({A}\right)$
26 normge0 ${⊢}{A}\in ℋ\to 0\le {norm}_{ℎ}\left({A}\right)$
27 1 2 nmcoplbi ${⊢}{F}\left({A}\right)\in ℋ\to {norm}_{ℎ}\left({T}\left({F}\left({A}\right)\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({F}\left({A}\right)\right)$
28 7 27 syl ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({T}\left({F}\left({A}\right)\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({F}\left({A}\right)\right)$
29 15 22 16 26 28 lemul1ad ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({T}\left({F}\left({A}\right)\right)\right){norm}_{ℎ}\left({A}\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({F}\left({A}\right)\right){norm}_{ℎ}\left({A}\right)$
30 13 17 23 25 29 letrd ${⊢}{A}\in ℋ\to \left|{T}\left({F}\left({A}\right)\right){\cdot }_{\mathrm{ih}}{A}\right|\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({F}\left({A}\right)\right){norm}_{ℎ}\left({A}\right)$
31 1 2 3 4 5 cnlnadjlem5 ${⊢}\left({A}\in ℋ\wedge {F}\left({A}\right)\in ℋ\right)\to {T}\left({F}\left({A}\right)\right){\cdot }_{\mathrm{ih}}{A}={F}\left({A}\right){\cdot }_{\mathrm{ih}}{F}\left({A}\right)$
32 7 31 mpdan ${⊢}{A}\in ℋ\to {T}\left({F}\left({A}\right)\right){\cdot }_{\mathrm{ih}}{A}={F}\left({A}\right){\cdot }_{\mathrm{ih}}{F}\left({A}\right)$
33 32 fveq2d ${⊢}{A}\in ℋ\to \left|{T}\left({F}\left({A}\right)\right){\cdot }_{\mathrm{ih}}{A}\right|=\left|{F}\left({A}\right){\cdot }_{\mathrm{ih}}{F}\left({A}\right)\right|$
34 hiidrcl ${⊢}{F}\left({A}\right)\in ℋ\to {F}\left({A}\right){\cdot }_{\mathrm{ih}}{F}\left({A}\right)\in ℝ$
35 7 34 syl ${⊢}{A}\in ℋ\to {F}\left({A}\right){\cdot }_{\mathrm{ih}}{F}\left({A}\right)\in ℝ$
36 hiidge0 ${⊢}{F}\left({A}\right)\in ℋ\to 0\le {F}\left({A}\right){\cdot }_{\mathrm{ih}}{F}\left({A}\right)$
37 7 36 syl ${⊢}{A}\in ℋ\to 0\le {F}\left({A}\right){\cdot }_{\mathrm{ih}}{F}\left({A}\right)$
38 35 37 absidd ${⊢}{A}\in ℋ\to \left|{F}\left({A}\right){\cdot }_{\mathrm{ih}}{F}\left({A}\right)\right|={F}\left({A}\right){\cdot }_{\mathrm{ih}}{F}\left({A}\right)$
39 normsq ${⊢}{F}\left({A}\right)\in ℋ\to {{norm}_{ℎ}\left({F}\left({A}\right)\right)}^{2}={F}\left({A}\right){\cdot }_{\mathrm{ih}}{F}\left({A}\right)$
40 7 39 syl ${⊢}{A}\in ℋ\to {{norm}_{ℎ}\left({F}\left({A}\right)\right)}^{2}={F}\left({A}\right){\cdot }_{\mathrm{ih}}{F}\left({A}\right)$
41 20 recnd ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({F}\left({A}\right)\right)\in ℂ$
42 41 sqvald ${⊢}{A}\in ℋ\to {{norm}_{ℎ}\left({F}\left({A}\right)\right)}^{2}={norm}_{ℎ}\left({F}\left({A}\right)\right){norm}_{ℎ}\left({F}\left({A}\right)\right)$
43 40 42 eqtr3d ${⊢}{A}\in ℋ\to {F}\left({A}\right){\cdot }_{\mathrm{ih}}{F}\left({A}\right)={norm}_{ℎ}\left({F}\left({A}\right)\right){norm}_{ℎ}\left({F}\left({A}\right)\right)$
44 33 38 43 3eqtrd ${⊢}{A}\in ℋ\to \left|{T}\left({F}\left({A}\right)\right){\cdot }_{\mathrm{ih}}{A}\right|={norm}_{ℎ}\left({F}\left({A}\right)\right){norm}_{ℎ}\left({F}\left({A}\right)\right)$
45 16 recnd ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({A}\right)\in ℂ$
46 18 recni ${⊢}{norm}_{\mathrm{op}}\left({T}\right)\in ℂ$
47 mul32 ${⊢}\left({norm}_{\mathrm{op}}\left({T}\right)\in ℂ\wedge {norm}_{ℎ}\left({F}\left({A}\right)\right)\in ℂ\wedge {norm}_{ℎ}\left({A}\right)\in ℂ\right)\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({F}\left({A}\right)\right){norm}_{ℎ}\left({A}\right)={norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({F}\left({A}\right)\right)$
48 46 47 mp3an1 ${⊢}\left({norm}_{ℎ}\left({F}\left({A}\right)\right)\in ℂ\wedge {norm}_{ℎ}\left({A}\right)\in ℂ\right)\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({F}\left({A}\right)\right){norm}_{ℎ}\left({A}\right)={norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({F}\left({A}\right)\right)$
49 41 45 48 syl2anc ${⊢}{A}\in ℋ\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({F}\left({A}\right)\right){norm}_{ℎ}\left({A}\right)={norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({F}\left({A}\right)\right)$
50 30 44 49 3brtr3d ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({F}\left({A}\right)\right){norm}_{ℎ}\left({F}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({F}\left({A}\right)\right)$
51 50 adantr ${⊢}\left({A}\in ℋ\wedge {norm}_{ℎ}\left({F}\left({A}\right)\right)\ne 0\right)\to {norm}_{ℎ}\left({F}\left({A}\right)\right){norm}_{ℎ}\left({F}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({F}\left({A}\right)\right)$
52 20 adantr ${⊢}\left({A}\in ℋ\wedge {norm}_{ℎ}\left({F}\left({A}\right)\right)\ne 0\right)\to {norm}_{ℎ}\left({F}\left({A}\right)\right)\in ℝ$
53 remulcl ${⊢}\left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ\wedge {norm}_{ℎ}\left({A}\right)\in ℝ\right)\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)\in ℝ$
54 18 16 53 sylancr ${⊢}{A}\in ℋ\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)\in ℝ$
55 54 adantr ${⊢}\left({A}\in ℋ\wedge {norm}_{ℎ}\left({F}\left({A}\right)\right)\ne 0\right)\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)\in ℝ$
56 normge0 ${⊢}{F}\left({A}\right)\in ℋ\to 0\le {norm}_{ℎ}\left({F}\left({A}\right)\right)$
57 0re ${⊢}0\in ℝ$
58 leltne ${⊢}\left(0\in ℝ\wedge {norm}_{ℎ}\left({F}\left({A}\right)\right)\in ℝ\wedge 0\le {norm}_{ℎ}\left({F}\left({A}\right)\right)\right)\to \left(0<{norm}_{ℎ}\left({F}\left({A}\right)\right)↔{norm}_{ℎ}\left({F}\left({A}\right)\right)\ne 0\right)$
59 57 58 mp3an1 ${⊢}\left({norm}_{ℎ}\left({F}\left({A}\right)\right)\in ℝ\wedge 0\le {norm}_{ℎ}\left({F}\left({A}\right)\right)\right)\to \left(0<{norm}_{ℎ}\left({F}\left({A}\right)\right)↔{norm}_{ℎ}\left({F}\left({A}\right)\right)\ne 0\right)$
60 19 56 59 syl2anc ${⊢}{F}\left({A}\right)\in ℋ\to \left(0<{norm}_{ℎ}\left({F}\left({A}\right)\right)↔{norm}_{ℎ}\left({F}\left({A}\right)\right)\ne 0\right)$
61 60 biimpar ${⊢}\left({F}\left({A}\right)\in ℋ\wedge {norm}_{ℎ}\left({F}\left({A}\right)\right)\ne 0\right)\to 0<{norm}_{ℎ}\left({F}\left({A}\right)\right)$
62 7 61 sylan ${⊢}\left({A}\in ℋ\wedge {norm}_{ℎ}\left({F}\left({A}\right)\right)\ne 0\right)\to 0<{norm}_{ℎ}\left({F}\left({A}\right)\right)$
63 lemul1 ${⊢}\left({norm}_{ℎ}\left({F}\left({A}\right)\right)\in ℝ\wedge {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)\in ℝ\wedge \left({norm}_{ℎ}\left({F}\left({A}\right)\right)\in ℝ\wedge 0<{norm}_{ℎ}\left({F}\left({A}\right)\right)\right)\right)\to \left({norm}_{ℎ}\left({F}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)↔{norm}_{ℎ}\left({F}\left({A}\right)\right){norm}_{ℎ}\left({F}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({F}\left({A}\right)\right)\right)$
64 52 55 52 62 63 syl112anc ${⊢}\left({A}\in ℋ\wedge {norm}_{ℎ}\left({F}\left({A}\right)\right)\ne 0\right)\to \left({norm}_{ℎ}\left({F}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)↔{norm}_{ℎ}\left({F}\left({A}\right)\right){norm}_{ℎ}\left({F}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({F}\left({A}\right)\right)\right)$
65 51 64 mpbird ${⊢}\left({A}\in ℋ\wedge {norm}_{ℎ}\left({F}\left({A}\right)\right)\ne 0\right)\to {norm}_{ℎ}\left({F}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)$
66 nmopge0 ${⊢}{T}:ℋ⟶ℋ\to 0\le {norm}_{\mathrm{op}}\left({T}\right)$
67 8 66 ax-mp ${⊢}0\le {norm}_{\mathrm{op}}\left({T}\right)$
68 mulge0 ${⊢}\left(\left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ\wedge 0\le {norm}_{\mathrm{op}}\left({T}\right)\right)\wedge \left({norm}_{ℎ}\left({A}\right)\in ℝ\wedge 0\le {norm}_{ℎ}\left({A}\right)\right)\right)\to 0\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)$
69 18 67 68 mpanl12 ${⊢}\left({norm}_{ℎ}\left({A}\right)\in ℝ\wedge 0\le {norm}_{ℎ}\left({A}\right)\right)\to 0\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)$
70 16 26 69 syl2anc ${⊢}{A}\in ℋ\to 0\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)$
71 6 65 70 pm2.61ne ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({F}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)$