Home

Hilbert Space Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem nmopcoadj 9948

Description: The norm of an operator composed with its adjoint. Part of Theorem 3.11(vi) of [Beran] p. 106.

Hypothesis

Ref	Expression
nmopcoadj.1	BndLinOp

Assertion

Ref	Expression
nmopcoadj	normopadjh normop

---

Proof of Theorem nmopcoadj

Step	Hyp	Ref	Expression
1		nmopcoadj.1	. . . . . 6 BndLinOp
2		adjbdlnb 9932	. . . . . 6 BndLinOp adjh BndLinOp
3	1, 2	mpbi 189	. . . . 5 adjh BndLinOp
4	3, 1	bdopco 9945	. . . 4 adjh BndLinOp
5		nmopret 9714	. . . 4 adjh BndLinOp normopadjh
6	4, 5	ax-mp 7	. . 3 normopadjh
7		nmopret 9714	. . . . 5 BndLinOp normop
8	1, 7	ax-mp 7	. . . 4 normop
9	8	resqcl 6554	. . 3 normop
10	6, 9	letri3 5547	. 2 normopadjh normop normopadjh normop normop normopadjh
11		bdopft 9706	. . . . 5 adjh BndLinOp adjh
12	3, 11	ax-mp 7	. . . 4 adjh
13		bdopft 9706	. . . . 5 BndLinOp
14	1, 13	ax-mp 7	. . . 4
15	12, 14	hocof 9609	. . 3 adjh
16		rexrt 5471	. . . 4 normop normop
17	9, 16	ax-mp 7	. . 3 normop
18	12, 14	hoco 9607	. . . . . . . . 9 adjh adjh
19	18	fveq2d 3713	. . . . . . . 8 adjh adjh
20	19	adantr 389	. . . . . . 7 adjh adjh
21	14	ffvelrni 3800	. . . . . . . . . . 11
22	12	ffvelrni 3800	. . . . . . . . . . 11 adjh
23	21, 22	syl 10	. . . . . . . . . 10 adjh
24		normclt 8912	. . . . . . . . . 10 adjh adjh
25	23, 24	syl 10	. . . . . . . . 9 adjh
26	25	adantr 389	. . . . . . . 8 adjh
27		normclt 8912	. . . . . . . . . . 11
28	21, 27	syl 10	. . . . . . . . . 10
29		nmopret 9714	. . . . . . . . . . . 12 adjh BndLinOp normopadjh
30	3, 29	ax-mp 7	. . . . . . . . . . 11 normopadjh
31		axmulrcl 5246	. . . . . . . . . . 11 normopadjh normopadjh
32	30, 31	mpan 693	. . . . . . . . . 10 normopadjh
33	28, 32	syl 10	. . . . . . . . 9 normopadjh
34	33	adantr 389	. . . . . . . 8 normopadjh
35	30, 8	remulcl 5307	. . . . . . . . 9 normopadjh normop
36	35	a1i 8	. . . . . . . 8 normopadjh normop
37	3	nmbdoplb 9864	. . . . . . . . . 10 adjh normopadjh
38	21, 37	syl 10	. . . . . . . . 9 adjh normopadjh
39	38	adantr 389	. . . . . . . 8 adjh normopadjh
40		nmopge0t 9751	. . . . . . . . . . . . 13 adjh normopadjh
41	12, 40	ax-mp 7	. . . . . . . . . . . 12 normopadjh
42		lemul2itOLD 5796	. . . . . . . . . . . 12 normop normopadjh normopadjh normop normopadjh normopadjh normop
43	41, 42	mpanr1 707	. . . . . . . . . . 11 normop normopadjh normop normopadjh normopadjh normop
44	30, 43	mp3anl3 909	. . . . . . . . . 10 normop normop normopadjh normopadjh normop
45	8, 44	mpanl2 705	. . . . . . . . 9 normop normopadjh normopadjh normop
46	28	adantr 389	. . . . . . . . 9
47		normclt 8912	. . . . . . . . . . . 12
48		axmulrcl 5246	. . . . . . . . . . . . 13 normop normop
49	8, 48	mpan 693	. . . . . . . . . . . 12 normop
50	47, 49	syl 10	. . . . . . . . . . 11 normop
51	50	adantr 389	. . . . . . . . . 10 normop
52	8	a1i 8	. . . . . . . . . 10 normop
53	1	nmbdoplb 9864	. . . . . . . . . . 11 normop
54	53	adantr 389	. . . . . . . . . 10 normop
55		1re 5407	. . . . . . . . . . . . 13
56		nmopge0t 9751	. . . . . . . . . . . . . . . 16 normop
57	14, 56	ax-mp 7	. . . . . . . . . . . . . . 15 normop
58		lemul2itOLD 5796	. . . . . . . . . . . . . . 15 normop normop normop normop
59	57, 58	mpanr1 707	. . . . . . . . . . . . . 14 normop normop normop
60	8, 59	mp3anl3 909	. . . . . . . . . . . . 13 normop normop
61	55, 60	mpanl2 705	. . . . . . . . . . . 12 normop normop
62	61, 47	sylan 448	. . . . . . . . . . 11 normop normop
63	8	recn 5286	. . . . . . . . . . . 12 normop
64	63	mulid1 5304	. . . . . . . . . . 11 normop normop
65	62, 64	syl6breq 2644	. . . . . . . . . 10 normop normop
66	46, 51, 52, 54, 65	letrd 5499	. . . . . . . . 9 norm