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 ⊢ 𝑇 ∈ BndLinOp
Assertion nmopcoadji ( normop ‘ ( ( adjℎ ‘ 𝑇 ) ∘ 𝑇 ) ) = ( ( normop ‘ 𝑇 ) ↑ 2 )

Proof

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