Metamath Proof Explorer

Theorem nmopcoadji

Description: The norm of an operator composed with its adjoint. Part of Theorem 3.11(vi) of Beran p. 106. (Contributed by NM, 8-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmopcoadj.1 ⊢ T ∈ BndLinOp
Assertion nmopcoadji ⊢ norm op ⁡ adj h ⁡ T ∘ T = norm op ⁡ T 2

Proof

Step Hyp Ref Expression
1 nmopcoadj.1 ⊢ T ∈ BndLinOp
2 adjbdlnb ⊢ T ∈ BndLinOp ↔ adj h ⁡ T ∈ BndLinOp
3 1 2 mpbi ⊢ adj h ⁡ T ∈ BndLinOp
4 bdopf ⊢ adj h ⁡ T ∈ BndLinOp → adj h ⁡ T : ℋ ⟶ ℋ
5 3 4 ax-mp ⊢ adj h ⁡ T : ℋ ⟶ ℋ
6 bdopf ⊢ T ∈ BndLinOp → T : ℋ ⟶ ℋ
7 1 6 ax-mp ⊢ T : ℋ ⟶ ℋ
8 5 7 hocofi ⊢ adj h ⁡ T ∘ T : ℋ ⟶ ℋ
9 nmopre ⊢ T ∈ BndLinOp → norm op ⁡ T ∈ ℝ
10 1 9 ax-mp ⊢ norm op ⁡ T ∈ ℝ
11 10 resqcli ⊢ norm op ⁡ T 2 ∈ ℝ
12 rexr ⊢ norm op ⁡ T 2 ∈ ℝ → norm op ⁡ T 2 ∈ ℝ *
13 11 12 ax-mp ⊢ norm op ⁡ T 2 ∈ ℝ *
14 nmopub ⊢ adj h ⁡ T ∘ T : ℋ ⟶ ℋ ∧ norm op ⁡ T 2 ∈ ℝ * → norm op ⁡ adj h ⁡ T ∘ T ≤ norm op ⁡ T 2 ↔ ∀ x ∈ ℋ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ adj h ⁡ T ∘ T ⁡ x ≤ norm op ⁡ T 2
15 8 13 14 mp2an ⊢ norm op ⁡ adj h ⁡ T ∘ T ≤ norm op ⁡ T 2 ↔ ∀ x ∈ ℋ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ adj h ⁡ T ∘ T ⁡ x ≤ norm op ⁡ T 2
16 5 7 hocoi ⊢ x ∈ ℋ → adj h ⁡ T ∘ T ⁡ x = adj h ⁡ T ⁡ T ⁡ x
17 16 fveq2d ⊢ x ∈ ℋ → norm ℎ ⁡ adj h ⁡ T ∘ T ⁡ x = norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x
18 17 adantr ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ adj h ⁡ T ∘ T ⁡ x = norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x
19 7 ffvelcdmi ⊢ x ∈ ℋ → T ⁡ x ∈ ℋ
20 5 ffvelcdmi ⊢ T ⁡ x ∈ ℋ → adj h ⁡ T ⁡ T ⁡ x ∈ ℋ
21 normcl ⊢ adj h ⁡ T ⁡ T ⁡ x ∈ ℋ → norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ∈ ℝ
22 19 20 21 3syl ⊢ x ∈ ℋ → norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ∈ ℝ
23 22 adantr ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ∈ ℝ
24 nmopre ⊢ adj h ⁡ T ∈ BndLinOp → norm op ⁡ adj h ⁡ T ∈ ℝ
25 3 24 ax-mp ⊢ norm op ⁡ adj h ⁡ T ∈ ℝ
26 normcl ⊢ T ⁡ x ∈ ℋ → norm ℎ ⁡ T ⁡ x ∈ ℝ
27 19 26 syl ⊢ x ∈ ℋ → norm ℎ ⁡ T ⁡ x ∈ ℝ
28 remulcl ⊢ norm op ⁡ adj h ⁡ T ∈ ℝ ∧ norm ℎ ⁡ T ⁡ x ∈ ℝ → norm op ⁡ adj h ⁡ T ⁢ norm ℎ ⁡ T ⁡ x ∈ ℝ
29 25 27 28 sylancr ⊢ x ∈ ℋ → norm op ⁡ adj h ⁡ T ⁢ norm ℎ ⁡ T ⁡ x ∈ ℝ
30 29 adantr ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm op ⁡ adj h ⁡ T ⁢ norm ℎ ⁡ T ⁡ x ∈ ℝ
31 25 10 remulcli ⊢ norm op ⁡ adj h ⁡ T ⁢ norm op ⁡ T ∈ ℝ
32 31 a1i ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm op ⁡ adj h ⁡ T ⁢ norm op ⁡ T ∈ ℝ
33 3 nmbdoplbi ⊢ T ⁡ x ∈ ℋ → norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ≤ norm op ⁡ adj h ⁡ T ⁢ norm ℎ ⁡ T ⁡ x
34 19 33 syl ⊢ x ∈ ℋ → norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ≤ norm op ⁡ adj h ⁡ T ⁢ norm ℎ ⁡ T ⁡ x
35 34 adantr ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ≤ norm op ⁡ adj h ⁡ T ⁢ norm ℎ ⁡ T ⁡ x
36 27 adantr ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ∈ ℝ
37 10 a1i ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm op ⁡ T ∈ ℝ
38 normcl ⊢ x ∈ ℋ → norm ℎ ⁡ x ∈ ℝ
39 remulcl ⊢ norm op ⁡ T ∈ ℝ ∧ norm ℎ ⁡ x ∈ ℝ → norm op ⁡ T ⁢ norm ℎ ⁡ x ∈ ℝ
40 10 38 39 sylancr ⊢ x ∈ ℋ → norm op ⁡ T ⁢ norm ℎ ⁡ x ∈ ℝ
41 40 adantr ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm op ⁡ T ⁢ norm ℎ ⁡ x ∈ ℝ
42 1 nmbdoplbi ⊢ x ∈ ℋ → norm ℎ ⁡ T ⁡ x ≤ norm op ⁡ T ⁢ norm ℎ ⁡ x
43 42 adantr ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ norm op ⁡ T ⁢ norm ℎ ⁡ x
44 1re ⊢ 1 ∈ ℝ
45 nmopge0 ⊢ T : ℋ ⟶ ℋ → 0 ≤ norm op ⁡ T
46 1 6 45 mp2b ⊢ 0 ≤ norm op ⁡ T
47 10 46 pm3.2i ⊢ norm op ⁡ T ∈ ℝ ∧ 0 ≤ norm op ⁡ T
48 lemul2a ⊢ norm ℎ ⁡ x ∈ ℝ ∧ 1 ∈ ℝ ∧ norm op ⁡ T ∈ ℝ ∧ 0 ≤ norm op ⁡ T ∧ norm ℎ ⁡ x ≤ 1 → norm op ⁡ T ⁢ norm ℎ ⁡ x ≤ norm op ⁡ T ⋅ 1
49 47 48 mp3anl3 ⊢ norm ℎ ⁡ x ∈ ℝ ∧ 1 ∈ ℝ ∧ norm ℎ ⁡ x ≤ 1 → norm op ⁡ T ⁢ norm ℎ ⁡ x ≤ norm op ⁡ T ⋅ 1
50 44 49 mpanl2 ⊢ norm ℎ ⁡ x ∈ ℝ ∧ norm ℎ ⁡ x ≤ 1 → norm op ⁡ T ⁢ norm ℎ ⁡ x ≤ norm op ⁡ T ⋅ 1
51 38 50 sylan ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm op ⁡ T ⁢ norm ℎ ⁡ x ≤ norm op ⁡ T ⋅ 1
52 10 recni ⊢ norm op ⁡ T ∈ ℂ
53 52 mulridi ⊢ norm op ⁡ T ⋅ 1 = norm op ⁡ T
54 51 53 breqtrdi ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm op ⁡ T ⁢ norm ℎ ⁡ x ≤ norm op ⁡ T
55 36 41 37 43 54 letrd ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ norm op ⁡ T
56 nmopge0 ⊢ adj h ⁡ T : ℋ ⟶ ℋ → 0 ≤ norm op ⁡ adj h ⁡ T
57 3 4 56 mp2b ⊢ 0 ≤ norm op ⁡ adj h ⁡ T
58 25 57 pm3.2i ⊢ norm op ⁡ adj h ⁡ T ∈ ℝ ∧ 0 ≤ norm op ⁡ adj h ⁡ T
59 lemul2a ⊢ norm ℎ ⁡ T ⁡ x ∈ ℝ ∧ norm op ⁡ T ∈ ℝ ∧ norm op ⁡ adj h ⁡ T ∈ ℝ ∧ 0 ≤ norm op ⁡ adj h ⁡ T ∧ norm ℎ ⁡ T ⁡ x ≤ norm op ⁡ T → norm op ⁡ adj h ⁡ T ⁢ norm ℎ ⁡ T ⁡ x ≤ norm op ⁡ adj h ⁡ T ⁢ norm op ⁡ T
60 58 59 mp3anl3 ⊢ norm ℎ ⁡ T ⁡ x ∈ ℝ ∧ norm op ⁡ T ∈ ℝ ∧ norm ℎ ⁡ T ⁡ x ≤ norm op ⁡ T → norm op ⁡ adj h ⁡ T ⁢ norm ℎ ⁡ T ⁡ x ≤ norm op ⁡ adj h ⁡ T ⁢ norm op ⁡ T
61 36 37 55 60 syl21anc ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm op ⁡ adj h ⁡ T ⁢ norm ℎ ⁡ T ⁡ x ≤ norm op ⁡ adj h ⁡ T ⁢ norm op ⁡ T
62 23 30 32 35 61 letrd ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ≤ norm op ⁡ adj h ⁡ T ⁢ norm op ⁡ T
63 18 62 eqbrtrd ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ adj h ⁡ T ∘ T ⁡ x ≤ norm op ⁡ adj h ⁡ T ⁢ norm op ⁡ T
64 1 nmopadji ⊢ norm op ⁡ adj h ⁡ T = norm op ⁡ T
65 64 oveq1i ⊢ norm op ⁡ adj h ⁡ T ⁢ norm op ⁡ T = norm op ⁡ T ⁢ norm op ⁡ T
66 52 sqvali ⊢ norm op ⁡ T 2 = norm op ⁡ T ⁢ norm op ⁡ T
67 65 66 eqtr4i ⊢ norm op ⁡ adj h ⁡ T ⁢ norm op ⁡ T = norm op ⁡ T 2
68 63 67 breqtrdi ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ adj h ⁡ T ∘ T ⁡ x ≤ norm op ⁡ T 2
69 68 ex ⊢ x ∈ ℋ → norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ adj h ⁡ T ∘ T ⁡ x ≤ norm op ⁡ T 2
70 15 69 mprgbir ⊢ norm op ⁡ adj h ⁡ T ∘ T ≤ norm op ⁡ T 2
71 nmopge0 ⊢ adj h ⁡ T ∘ T : ℋ ⟶ ℋ → 0 ≤ norm op ⁡ adj h ⁡ T ∘ T
72 8 71 ax-mp ⊢ 0 ≤ norm op ⁡ adj h ⁡ T ∘ T
73 3 1 bdopcoi ⊢ adj h ⁡ T ∘ T ∈ BndLinOp
74 nmopre ⊢ adj h ⁡ T ∘ T ∈ BndLinOp → norm op ⁡ adj h ⁡ T ∘ T ∈ ℝ
75 73 74 ax-mp ⊢ norm op ⁡ adj h ⁡ T ∘ T ∈ ℝ
76 75 sqrtcli ⊢ 0 ≤ norm op ⁡ adj h ⁡ T ∘ T → norm op ⁡ adj h ⁡ T ∘ T ∈ ℝ
77 rexr ⊢ norm op ⁡ adj h ⁡ T ∘ T ∈ ℝ → norm op ⁡ adj h ⁡ T ∘ T ∈ ℝ *
78 72 76 77 mp2b ⊢ norm op ⁡ adj h ⁡ T ∘ T ∈ ℝ *
79 nmopub ⊢ T : ℋ ⟶ ℋ ∧ norm op ⁡ adj h ⁡ T ∘ T ∈ ℝ * → norm op ⁡ T ≤ norm op ⁡ adj h ⁡ T ∘ T ↔ ∀ x ∈ ℋ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ norm op ⁡ adj h ⁡ T ∘ T
80 7 78 79 mp2an ⊢ norm op ⁡ T ≤ norm op ⁡ adj h ⁡ T ∘ T ↔ ∀ x ∈ ℋ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ norm op ⁡ adj h ⁡ T ∘ T
81 19 20 syl ⊢ x ∈ ℋ → adj h ⁡ T ⁡ T ⁡ x ∈ ℋ
82 hicl ⊢ adj h ⁡ T ⁡ T ⁡ x ∈ ℋ ∧ x ∈ ℋ → adj h ⁡ T ⁡ T ⁡ x ⋅ ih x ∈ ℂ
83 81 82 mpancom ⊢ x ∈ ℋ → adj h ⁡ T ⁡ T ⁡ x ⋅ ih x ∈ ℂ
84 83 abscld ⊢ x ∈ ℋ → adj h ⁡ T ⁡ T ⁡ x ⋅ ih x ∈ ℝ
85 84 adantr ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → adj h ⁡ T ⁡ T ⁡ x ⋅ ih x ∈ ℝ
86 22 38 remulcld ⊢ x ∈ ℋ → norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ⁢ norm ℎ ⁡ x ∈ ℝ
87 86 adantr ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ⁢ norm ℎ ⁡ x ∈ ℝ
88 75 a1i ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm op ⁡ adj h ⁡ T ∘ T ∈ ℝ
89 bcs ⊢ adj h ⁡ T ⁡ T ⁡ x ∈ ℋ ∧ x ∈ ℋ → adj h ⁡ T ⁡ T ⁡ x ⋅ ih x ≤ norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ⁢ norm ℎ ⁡ x
90 81 89 mpancom ⊢ x ∈ ℋ → adj h ⁡ T ⁡ T ⁡ x ⋅ ih x ≤ norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ⁢ norm ℎ ⁡ x
91 90 adantr ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → adj h ⁡ T ⁡ T ⁡ x ⋅ ih x ≤ norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ⁢ norm ℎ ⁡ x
92 5 7 hococli ⊢ x ∈ ℋ → adj h ⁡ T ∘ T ⁡ x ∈ ℋ
93 normcl ⊢ adj h ⁡ T ∘ T ⁡ x ∈ ℋ → norm ℎ ⁡ adj h ⁡ T ∘ T ⁡ x ∈ ℝ
94 92 93 syl ⊢ x ∈ ℋ → norm ℎ ⁡ adj h ⁡ T ∘ T ⁡ x ∈ ℝ
95 94 adantr ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ adj h ⁡ T ∘ T ⁡ x ∈ ℝ
96 38 adantr ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ x ∈ ℝ
97 normge0 ⊢ adj h ⁡ T ⁡ T ⁡ x ∈ ℋ → 0 ≤ norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x
98 19 20 97 3syl ⊢ x ∈ ℋ → 0 ≤ norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x
99 22 98 jca ⊢ x ∈ ℋ → norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ∈ ℝ ∧ 0 ≤ norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x
100 99 adantr ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ∈ ℝ ∧ 0 ≤ norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x
101 simpr ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ x ≤ 1
102 lemul2a ⊢ norm ℎ ⁡ x ∈ ℝ ∧ 1 ∈ ℝ ∧ norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ∈ ℝ ∧ 0 ≤ norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ⁢ norm ℎ ⁡ x ≤ norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ⋅ 1
103 44 102 mp3anl2 ⊢ norm ℎ ⁡ x ∈ ℝ ∧ norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ∈ ℝ ∧ 0 ≤ norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ⁢ norm ℎ ⁡ x ≤ norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ⋅ 1
104 96 100 101 103 syl21anc ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ⁢ norm ℎ ⁡ x ≤ norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ⋅ 1
105 22 recnd ⊢ x ∈ ℋ → norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ∈ ℂ
106 105 mulridd ⊢ x ∈ ℋ → norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ⋅ 1 = norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x
107 106 17 eqtr4d ⊢ x ∈ ℋ → norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ⋅ 1 = norm ℎ ⁡ adj h ⁡ T ∘ T ⁡ x
108 107 adantr ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ⋅ 1 = norm ℎ ⁡ adj h ⁡ T ∘ T ⁡ x
109 104 108 breqtrd ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ⁢ norm ℎ ⁡ x ≤ norm ℎ ⁡ adj h ⁡ T ∘ T ⁡ x
110 remulcl ⊢ norm op ⁡ adj h ⁡ T ∘ T ∈ ℝ ∧ norm ℎ ⁡ x ∈ ℝ → norm op ⁡ adj h ⁡ T ∘ T ⁢ norm ℎ ⁡ x ∈ ℝ
111 75 38 110 sylancr ⊢ x ∈ ℋ → norm op ⁡ adj h ⁡ T ∘ T ⁢ norm ℎ ⁡ x ∈ ℝ
112 111 adantr ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm op ⁡ adj h ⁡ T ∘ T ⁢ norm ℎ ⁡ x ∈ ℝ
113 73 nmbdoplbi ⊢ x ∈ ℋ → norm ℎ ⁡ adj h ⁡ T ∘ T ⁡ x ≤ norm op ⁡ adj h ⁡ T ∘ T ⁢ norm ℎ ⁡ x
114 113 adantr ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ adj h ⁡ T ∘ T ⁡ x ≤ norm op ⁡ adj h ⁡ T ∘ T ⁢ norm ℎ ⁡ x
115 75 72 pm3.2i ⊢ norm op ⁡ adj h ⁡ T ∘ T ∈ ℝ ∧ 0 ≤ norm op ⁡ adj h ⁡ T ∘ T
116 lemul2a ⊢ norm ℎ ⁡ x ∈ ℝ ∧ 1 ∈ ℝ ∧ norm op ⁡ adj h ⁡ T ∘ T ∈ ℝ ∧ 0 ≤ norm op ⁡ adj h ⁡ T ∘ T ∧ norm ℎ ⁡ x ≤ 1 → norm op ⁡ adj h ⁡ T ∘ T ⁢ norm ℎ ⁡ x ≤ norm op ⁡ adj h ⁡ T ∘ T ⋅ 1
117 115 116 mp3anl3 ⊢ norm ℎ ⁡ x ∈ ℝ ∧ 1 ∈ ℝ ∧ norm ℎ ⁡ x ≤ 1 → norm op ⁡ adj h ⁡ T ∘ T ⁢ norm ℎ ⁡ x ≤ norm op ⁡ adj h ⁡ T ∘ T ⋅ 1
118 44 117 mpanl2 ⊢ norm ℎ ⁡ x ∈ ℝ ∧ norm ℎ ⁡ x ≤ 1 → norm op ⁡ adj h ⁡ T ∘ T ⁢ norm ℎ ⁡ x ≤ norm op ⁡ adj h ⁡ T ∘ T ⋅ 1
119 38 118 sylan ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm op ⁡ adj h ⁡ T ∘ T ⁢ norm ℎ ⁡ x ≤ norm op ⁡ adj h ⁡ T ∘ T ⋅ 1
120 75 recni ⊢ norm op ⁡ adj h ⁡ T ∘ T ∈ ℂ
121 120 mulridi ⊢ norm op ⁡ adj h ⁡ T ∘ T ⋅ 1 = norm op ⁡ adj h ⁡ T ∘ T
122 119 121 breqtrdi ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm op ⁡ adj h ⁡ T ∘ T ⁢ norm ℎ ⁡ x ≤ norm op ⁡ adj h ⁡ T ∘ T
123 95 112 88 114 122 letrd ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ adj h ⁡ T ∘ T ⁡ x ≤ norm op ⁡ adj h ⁡ T ∘ T
124 87 95 88 109 123 letrd ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ adj h ⁡ T ⁡ T ⁡ x ⁢ norm ℎ ⁡ x ≤ norm op ⁡ adj h ⁡ T ∘ T
125 85 87 88 91 124 letrd ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → adj h ⁡ T ⁡ T ⁡ x ⋅ ih x ≤ norm op ⁡ adj h ⁡ T ∘ T
126 resqcl ⊢ norm ℎ ⁡ T ⁡ x ∈ ℝ → norm ℎ ⁡ T ⁡ x 2 ∈ ℝ
127 sqge0 ⊢ norm ℎ ⁡ T ⁡ x ∈ ℝ → 0 ≤ norm ℎ ⁡ T ⁡ x 2
128 126 127 absidd ⊢ norm ℎ ⁡ T ⁡ x ∈ ℝ → norm ℎ ⁡ T ⁡ x 2 = norm ℎ ⁡ T ⁡ x 2
129 19 26 128 3syl ⊢ x ∈ ℋ → norm ℎ ⁡ T ⁡ x 2 = norm ℎ ⁡ T ⁡ x 2
130 normsq ⊢ T ⁡ x ∈ ℋ → norm ℎ ⁡ T ⁡ x 2 = T ⁡ x ⋅ ih T ⁡ x
131 19 130 syl ⊢ x ∈ ℋ → norm ℎ ⁡ T ⁡ x 2 = T ⁡ x ⋅ ih T ⁡ x
132 bdopadj ⊢ adj h ⁡ T ∈ BndLinOp → adj h ⁡ T ∈ dom ⁡ adj h
133 3 132 ax-mp ⊢ adj h ⁡ T ∈ dom ⁡ adj h
134 adj2 ⊢ adj h ⁡ T ∈ dom ⁡ adj h ∧ T ⁡ x ∈ ℋ ∧ x ∈ ℋ → adj h ⁡ T ⁡ T ⁡ x ⋅ ih x = T ⁡ x ⋅ ih adj h ⁡ adj h ⁡ T ⁡ x
135 133 134 mp3an1 ⊢ T ⁡ x ∈ ℋ ∧ x ∈ ℋ → adj h ⁡ T ⁡ T ⁡ x ⋅ ih x = T ⁡ x ⋅ ih adj h ⁡ adj h ⁡ T ⁡ x
136 19 135 mpancom ⊢ x ∈ ℋ → adj h ⁡ T ⁡ T ⁡ x ⋅ ih x = T ⁡ x ⋅ ih adj h ⁡ adj h ⁡ T ⁡ x
137 bdopadj ⊢ T ∈ BndLinOp → T ∈ dom ⁡ adj h
138 adjadj ⊢ T ∈ dom ⁡ adj h → adj h ⁡ adj h ⁡ T = T
139 1 137 138 mp2b ⊢ adj h ⁡ adj h ⁡ T = T
140 139 fveq1i ⊢ adj h ⁡ adj h ⁡ T ⁡ x = T ⁡ x
141 140 oveq2i ⊢ T ⁡ x ⋅ ih adj h ⁡ adj h ⁡ T ⁡ x = T ⁡ x ⋅ ih T ⁡ x
142 136 141 eqtr2di ⊢ x ∈ ℋ → T ⁡ x ⋅ ih T ⁡ x = adj h ⁡ T ⁡ T ⁡ x ⋅ ih x
143 131 142 eqtrd ⊢ x ∈ ℋ → norm ℎ ⁡ T ⁡ x 2 = adj h ⁡ T ⁡ T ⁡ x ⋅ ih x
144 143 fveq2d ⊢ x ∈ ℋ → norm ℎ ⁡ T ⁡ x 2 = adj h ⁡ T ⁡ T ⁡ x ⋅ ih x
145 129 144 eqtr3d ⊢ x ∈ ℋ → norm ℎ ⁡ T ⁡ x 2 = adj h ⁡ T ⁡ T ⁡ x ⋅ ih x
146 145 adantr ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x 2 = adj h ⁡ T ⁡ T ⁡ x ⋅ ih x
147 75 sqsqrti ⊢ 0 ≤ norm op ⁡ adj h ⁡ T ∘ T → norm op ⁡ adj h ⁡ T ∘ T 2 = norm op ⁡ adj h ⁡ T ∘ T
148 8 71 147 mp2b ⊢ norm op ⁡ adj h ⁡ T ∘ T 2 = norm op ⁡ adj h ⁡ T ∘ T
149 148 a1i ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm op ⁡ adj h ⁡ T ∘ T 2 = norm op ⁡ adj h ⁡ T ∘ T
150 125 146 149 3brtr4d ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x 2 ≤ norm op ⁡ adj h ⁡ T ∘ T 2
151 normge0 ⊢ T ⁡ x ∈ ℋ → 0 ≤ norm ℎ ⁡ T ⁡ x
152 19 151 syl ⊢ x ∈ ℋ → 0 ≤ norm ℎ ⁡ T ⁡ x
153 8 71 76 mp2b ⊢ norm op ⁡ adj h ⁡ T ∘ T ∈ ℝ
154 75 sqrtge0i ⊢ 0 ≤ norm op ⁡ adj h ⁡ T ∘ T → 0 ≤ norm op ⁡ adj h ⁡ T ∘ T
155 8 71 154 mp2b ⊢ 0 ≤ norm op ⁡ adj h ⁡ T ∘ T
156 le2sq ⊢ norm ℎ ⁡ T ⁡ x ∈ ℝ ∧ 0 ≤ norm ℎ ⁡ T ⁡ x ∧ norm op ⁡ adj h ⁡ T ∘ T ∈ ℝ ∧ 0 ≤ norm op ⁡ adj h ⁡ T ∘ T → norm ℎ ⁡ T ⁡ x ≤ norm op ⁡ adj h ⁡ T ∘ T ↔ norm ℎ ⁡ T ⁡ x 2 ≤ norm op ⁡ adj h ⁡ T ∘ T 2
157 153 155 156 mpanr12 ⊢ norm ℎ ⁡ T ⁡ x ∈ ℝ ∧ 0 ≤ norm ℎ ⁡ T ⁡ x → norm ℎ ⁡ T ⁡ x ≤ norm op ⁡ adj h ⁡ T ∘ T ↔ norm ℎ ⁡ T ⁡ x 2 ≤ norm op ⁡ adj h ⁡ T ∘ T 2
158 27 152 157 syl2anc ⊢ x ∈ ℋ → norm ℎ ⁡ T ⁡ x ≤ norm op ⁡ adj h ⁡ T ∘ T ↔ norm ℎ ⁡ T ⁡ x 2 ≤ norm op ⁡ adj h ⁡ T ∘ T 2
159 158 adantr ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ norm op ⁡ adj h ⁡ T ∘ T ↔ norm ℎ ⁡ T ⁡ x 2 ≤ norm op ⁡ adj h ⁡ T ∘ T 2
160 150 159 mpbird ⊢ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ norm op ⁡ adj h ⁡ T ∘ T
161 160 ex ⊢ x ∈ ℋ → norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ norm op ⁡ adj h ⁡ T ∘ T
162 80 161 mprgbir ⊢ norm op ⁡ T ≤ norm op ⁡ adj h ⁡ T ∘ T
163 10 153 le2sqi ⊢ 0 ≤ norm op ⁡ T ∧ 0 ≤ norm op ⁡ adj h ⁡ T ∘ T → norm op ⁡ T ≤ norm op ⁡ adj h ⁡ T ∘ T ↔ norm op ⁡ T 2 ≤ norm op ⁡ adj h ⁡ T ∘ T 2
164 46 155 163 mp2an ⊢ norm op ⁡ T ≤ norm op ⁡ adj h ⁡ T ∘ T ↔ norm op ⁡ T 2 ≤ norm op ⁡ adj h ⁡ T ∘ T 2
165 162 164 mpbi ⊢ norm op ⁡ T 2 ≤ norm op ⁡ adj h ⁡ T ∘ T 2
166 165 148 breqtri ⊢ norm op ⁡ T 2 ≤ norm op ⁡ adj h ⁡ T ∘ T
167 75 11 letri3i ⊢ norm op ⁡ adj h ⁡ T ∘ T = norm op ⁡ T 2 ↔ norm op ⁡ adj h ⁡ T ∘ T ≤ norm op ⁡ T 2 ∧ norm op ⁡ T 2 ≤ norm op ⁡ adj h ⁡ T ∘ T
168 70 166 167 mpbir2an ⊢ norm op ⁡ adj h ⁡ T ∘ T = norm op ⁡ T 2