Theorem cnlnadjlem7

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 \mathscr{H}⟼T\left(g\right){\cdot }_{\mathrm{ih}}y\right)$$
	cnlnadjlem.4	$$⊢B=\left(\iota w\in \mathscr{H}|\forall v\in \mathscr{H}T\left(v\right){\cdot }_{\mathrm{ih}}y=v{\cdot }_{\mathrm{ih}}w\right)$$
	cnlnadjlem.5	$$⊢F=\left(y\in \mathscr{H}⟼B\right)$$
Assertion	cnlnadjlem7	$$⊢A\in \mathscr{H}\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 \mathscr{H}⟼T\left(g\right){\cdot }_{\mathrm{ih}}y\right)$$
4		cnlnadjlem.4	$$⊢B=\left(\iota w\in \mathscr{H}|\forall v\in \mathscr{H}T\left(v\right){\cdot }_{\mathrm{ih}}y=v{\cdot }_{\mathrm{ih}}w\right)$$
5		cnlnadjlem.5	$$⊢F=\left(y\in \mathscr{H}⟼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)\leftrightarrow 0\le {norm}_{\mathrm{op}}\left(T\right){norm}_{ℎ}\left(A\right)\right)$$
7	1 2 3 4 5	cnlnadjlem4	$$⊢A\in \mathscr{H}\to F\left(A\right)\in \mathscr{H}$$
8	1	lnopfi	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
9	8	ffvelcdmi	$$⊢F\left(A\right)\in \mathscr{H}\to T\left(F\left(A\right)\right)\in \mathscr{H}$$
10	7 9	syl	$$⊢A\in \mathscr{H}\to T\left(F\left(A\right)\right)\in \mathscr{H}$$
11		hicl	$$⊢\left(T\left(F\left(A\right)\right)\in \mathscr{H}\wedge A\in \mathscr{H}\right)\to T\left(F\left(A\right)\right){\cdot }_{\mathrm{ih}}A\in ℂ$$
12	10 11	mpancom	$$⊢A\in \mathscr{H}\to T\left(F\left(A\right)\right){\cdot }_{\mathrm{ih}}A\in ℂ$$
13	12	abscld	$$⊢A\in \mathscr{H}\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 \mathscr{H}\to {norm}_{ℎ}\left(T\left(F\left(A\right)\right)\right)\in ℝ$$
15	10 14	syl	$$⊢A\in \mathscr{H}\to {norm}_{ℎ}\left(T\left(F\left(A\right)\right)\right)\in ℝ$$
16		normcl	$$⊢A\in \mathscr{H}\to {norm}_{ℎ}\left(A\right)\in ℝ$$
17	15 16	remulcld	$$⊢A\in \mathscr{H}\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 \mathscr{H}\to {norm}_{ℎ}\left(F\left(A\right)\right)\in ℝ$$
20	7 19	syl	$$⊢A\in \mathscr{H}\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 \mathscr{H}\to {norm}_{\mathrm{op}}\left(T\right){norm}_{ℎ}\left(F\left(A\right)\right)\in ℝ$$
23	22 16	remulcld	$$⊢A\in \mathscr{H}\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 \mathscr{H}\wedge A\in \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\to 0\le {norm}_{ℎ}\left(A\right)$$
27	1 2	nmcoplbi	$$⊢F\left(A\right)\in \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\wedge F\left(A\right)\in \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\to F\left(A\right){\cdot }_{\mathrm{ih}}F\left(A\right)\in ℝ$$
35	7 34	syl	$$⊢A\in \mathscr{H}\to F\left(A\right){\cdot }_{\mathrm{ih}}F\left(A\right)\in ℝ$$
36		hiidge0	$$⊢F\left(A\right)\in \mathscr{H}\to 0\le F\left(A\right){\cdot }_{\mathrm{ih}}F\left(A\right)$$
37	7 36	syl	$$⊢A\in \mathscr{H}\to 0\le F\left(A\right){\cdot }_{\mathrm{ih}}F\left(A\right)$$
38	35 37	absidd	$$⊢A\in \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\to {norm}_{ℎ}\left(F\left(A\right)\right)\in ℂ$$
42	41	sqvald	$$⊢A\in \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\to {norm}_{\mathrm{op}}\left(T\right){norm}_{ℎ}\left(A\right)\in ℝ$$
55	54	adantr	$$⊢\left(A\in \mathscr{H}\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 \mathscr{H}\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)\leftrightarrow {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)\leftrightarrow {norm}_{ℎ}\left(F\left(A\right)\right)\ne 0\right)$$
60	19 56 59	syl2anc	$$⊢F\left(A\right)\in \mathscr{H}\to \left(0<{norm}_{ℎ}\left(F\left(A\right)\right)\leftrightarrow {norm}_{ℎ}\left(F\left(A\right)\right)\ne 0\right)$$
61	60	biimpar	$$⊢\left(F\left(A\right)\in \mathscr{H}\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 \mathscr{H}\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)\leftrightarrow {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 \mathscr{H}\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)\leftrightarrow {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 \mathscr{H}\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:\mathscr{H}⟶\mathscr{H}\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 \mathscr{H}\to 0\le {norm}_{\mathrm{op}}\left(T\right){norm}_{ℎ}\left(A\right)$$
71	6 65 70	pm2.61ne	$$⊢A\in \mathscr{H}\to {norm}_{ℎ}\left(F\left(A\right)\right)\le {norm}_{\mathrm{op}}\left(T\right){norm}_{ℎ}\left(A\right)$$