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	|- T e. BndLinOp

Assertion

Ref	Expression
nmopcoadj	|- (normop` ((adjh` T) o. T)) = ((normop` T)^2)

Proof of Theorem nmopcoadj

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