Metamath Proof Explorer

Theorem nmopcoi

Description: Upper bound for the norm of the composition of two bounded linear operators. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nmoptri.1 ⊢ 𝑆 ∈ BndLinOp
nmoptri.2 ⊢ 𝑇 ∈ BndLinOp
Assertion nmopcoi ( normop ‘ ( 𝑆 ∘ 𝑇 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 nmoptri.1 ⊢ 𝑆 ∈ BndLinOp
2 nmoptri.2 ⊢ 𝑇 ∈ BndLinOp
3 bdopln ⊢ ( 𝑆 ∈ BndLinOp → 𝑆 ∈ LinOp )
4 1 3 ax-mp ⊢ 𝑆 ∈ LinOp
5 bdopln ⊢ ( 𝑇 ∈ BndLinOp → 𝑇 ∈ LinOp )
6 2 5 ax-mp ⊢ 𝑇 ∈ LinOp
7 4 6 lnopcoi ⊢ ( 𝑆 ∘ 𝑇 ) ∈ LinOp
8 7 lnopfi ⊢ ( 𝑆 ∘ 𝑇 ) : ℋ ⟶ ℋ
9 nmopre ⊢ ( 𝑆 ∈ BndLinOp → ( normop ‘ 𝑆 ) ∈ ℝ )
10 1 9 ax-mp ⊢ ( normop ‘ 𝑆 ) ∈ ℝ
11 nmopre ⊢ ( 𝑇 ∈ BndLinOp → ( normop ‘ 𝑇 ) ∈ ℝ )
12 2 11 ax-mp ⊢ ( normop ‘ 𝑇 ) ∈ ℝ
13 10 12 remulcli ⊢ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) ∈ ℝ
14 13 rexri ⊢ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) ∈ ℝ*
15 nmopub ⊢ ( ( ( 𝑆 ∘ 𝑇 ) : ℋ ⟶ ℋ ∧ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) ∈ ℝ* ) → ( ( normop ‘ ( 𝑆 ∘ 𝑇 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) ↔ ∀ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) ) ) )
16 8 14 15 mp2an ⊢ ( ( normop ‘ ( 𝑆 ∘ 𝑇 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) ↔ ∀ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) ) )
17 0le0 ⊢ 0 ≤ 0
18 17 a1i ⊢ ( ( ( normop ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) → 0 ≤ 0 )
19 4 6 lnopco0i ⊢ ( ( normop ‘ 𝑇 ) = 0 → ( normop ‘ ( 𝑆 ∘ 𝑇 ) ) = 0 )
20 7 nmlnop0iHIL ⊢ ( ( normop ‘ ( 𝑆 ∘ 𝑇 ) ) = 0 ↔ ( 𝑆 ∘ 𝑇 ) = 0hop )
21 19 20 sylib ⊢ ( ( normop ‘ 𝑇 ) = 0 → ( 𝑆 ∘ 𝑇 ) = 0hop )
22 fveq1 ⊢ ( ( 𝑆 ∘ 𝑇 ) = 0hop → ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) = ( 0hop ‘ 𝑥 ) )
23 22 fveq2d ⊢ ( ( 𝑆 ∘ 𝑇 ) = 0hop → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) = ( normℎ ‘ ( 0hop ‘ 𝑥 ) ) )
24 ho0val ⊢ ( 𝑥 ∈ ℋ → ( 0hop ‘ 𝑥 ) = 0ℎ )
25 24 fveq2d ⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( 0hop ‘ 𝑥 ) ) = ( normℎ ‘ 0ℎ ) )
26 norm0 ⊢ ( normℎ ‘ 0ℎ ) = 0
27 25 26 eqtrdi ⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( 0hop ‘ 𝑥 ) ) = 0 )
28 23 27 sylan9eq ⊢ ( ( ( 𝑆 ∘ 𝑇 ) = 0hop ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) = 0 )
29 21 28 sylan ⊢ ( ( ( normop ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) = 0 )
30 oveq2 ⊢ ( ( normop ‘ 𝑇 ) = 0 → ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) = ( ( normop ‘ 𝑆 ) · 0 ) )
31 10 recni ⊢ ( normop ‘ 𝑆 ) ∈ ℂ
32 31 mul01i ⊢ ( ( normop ‘ 𝑆 ) · 0 ) = 0
33 30 32 eqtrdi ⊢ ( ( normop ‘ 𝑇 ) = 0 → ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) = 0 )
34 33 adantr ⊢ ( ( ( normop ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) → ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) = 0 )
35 18 29 34 3brtr4d ⊢ ( ( ( normop ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) )
36 35 adantrr ⊢ ( ( ( normop ‘ 𝑇 ) = 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) )
37 df-ne ⊢ ( ( normop ‘ 𝑇 ) ≠ 0 ↔ ¬ ( normop ‘ 𝑇 ) = 0 )
38 8 ffvelrni ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ∈ ℋ )
39 normcl ⊢ ( ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ∈ ℋ → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ∈ ℝ )
40 38 39 syl ⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ∈ ℝ )
41 40 recnd ⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ∈ ℂ )
42 12 recni ⊢ ( normop ‘ 𝑇 ) ∈ ℂ
43 divrec2 ⊢ ( ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ∈ ℂ ∧ ( normop ‘ 𝑇 ) ∈ ℂ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) )
44 42 43 mp3an2 ⊢ ( ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ∈ ℂ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) )
45 41 44 sylan ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) )
46 45 ancoms ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) )
47 12 rerecclzi ⊢ ( ( normop ‘ 𝑇 ) ≠ 0 → ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℝ )
48 bdopf ⊢ ( 𝑇 ∈ BndLinOp → 𝑇 : ℋ ⟶ ℋ )
49 2 48 ax-mp ⊢ 𝑇 : ℋ ⟶ ℋ
50 nmopgt0 ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( ( normop ‘ 𝑇 ) ≠ 0 ↔ 0 < ( normop ‘ 𝑇 ) ) )
51 49 50 ax-mp ⊢ ( ( normop ‘ 𝑇 ) ≠ 0 ↔ 0 < ( normop ‘ 𝑇 ) )
52 12 recgt0i ⊢ ( 0 < ( normop ‘ 𝑇 ) → 0 < ( 1 / ( normop ‘ 𝑇 ) ) )
53 51 52 sylbi ⊢ ( ( normop ‘ 𝑇 ) ≠ 0 → 0 < ( 1 / ( normop ‘ 𝑇 ) ) )
54 0re ⊢ 0 ∈ ℝ
55 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℝ ) → ( 0 < ( 1 / ( normop ‘ 𝑇 ) ) → 0 ≤ ( 1 / ( normop ‘ 𝑇 ) ) ) )
56 54 55 mpan ⊢ ( ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℝ → ( 0 < ( 1 / ( normop ‘ 𝑇 ) ) → 0 ≤ ( 1 / ( normop ‘ 𝑇 ) ) ) )
57 47 53 56 sylc ⊢ ( ( normop ‘ 𝑇 ) ≠ 0 → 0 ≤ ( 1 / ( normop ‘ 𝑇 ) ) )
58 47 57 absidd ⊢ ( ( normop ‘ 𝑇 ) ≠ 0 → ( abs ‘ ( 1 / ( normop ‘ 𝑇 ) ) ) = ( 1 / ( normop ‘ 𝑇 ) ) )
59 58 adantr ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( abs ‘ ( 1 / ( normop ‘ 𝑇 ) ) ) = ( 1 / ( normop ‘ 𝑇 ) ) )
60 59 oveq1d ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( abs ‘ ( 1 / ( normop ‘ 𝑇 ) ) ) · ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) )
61 46 60 eqtr4d ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( ( abs ‘ ( 1 / ( normop ‘ 𝑇 ) ) ) · ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) )
62 42 recclzi ⊢ ( ( normop ‘ 𝑇 ) ≠ 0 → ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℂ )
63 norm-iii ⊢ ( ( ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℂ ∧ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ∈ ℋ ) → ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) = ( ( abs ‘ ( 1 / ( normop ‘ 𝑇 ) ) ) · ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) )
64 62 38 63 syl2an ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) = ( ( abs ‘ ( 1 / ( normop ‘ 𝑇 ) ) ) · ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) )
65 61 64 eqtr4d ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) )
66 49 ffvelrni ⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
67 4 lnopmuli ⊢ ( ( ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) → ( 𝑆 ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑆 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
68 62 66 67 syl2an ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( 𝑆 ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑆 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
69 bdopf ⊢ ( 𝑆 ∈ BndLinOp → 𝑆 : ℋ ⟶ ℋ )
70 1 69 ax-mp ⊢ 𝑆 : ℋ ⟶ ℋ
71 70 49 hocoi ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝑇 ‘ 𝑥 ) ) )
72 71 oveq2d ⊢ ( 𝑥 ∈ ℋ → ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑆 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
73 72 adantl ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑆 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
74 68 73 eqtr4d ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( 𝑆 ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) )
75 74 fveq2d ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( 𝑆 ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) = ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) )
76 65 75 eqtr4d ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( normℎ ‘ ( 𝑆 ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) )
77 76 adantrr ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( normℎ ‘ ( 𝑆 ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) )
78 hvmulcl ⊢ ( ( ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) → ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ )
79 62 66 78 syl2an ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ )
80 79 adantrr ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ )
81 norm-iii ⊢ ( ( ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) → ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( abs ‘ ( 1 / ( normop ‘ 𝑇 ) ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
82 62 66 81 syl2an ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( abs ‘ ( 1 / ( normop ‘ 𝑇 ) ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
83 normcl ⊢ ( ( 𝑇 ‘ 𝑥 ) ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
84 66 83 syl ⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
85 84 recnd ⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℂ )
86 divrec2 ⊢ ( ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℂ ∧ ( normop ‘ 𝑇 ) ∈ ℂ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
87 42 86 mp3an2 ⊢ ( ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℂ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
88 85 87 sylan ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
89 88 ancoms ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
90 59 oveq1d ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( abs ‘ ( 1 / ( normop ‘ 𝑇 ) ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
91 89 90 eqtr4d ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( ( abs ‘ ( 1 / ( normop ‘ 𝑇 ) ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
92 82 91 eqtr4d ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) )
93 92 adantrr ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) )
94 nmoplb ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( normop ‘ 𝑇 ) )
95 49 94 mp3an1 ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( normop ‘ 𝑇 ) )
96 42 mulid2i ⊢ ( 1 · ( normop ‘ 𝑇 ) ) = ( normop ‘ 𝑇 )
97 95 96 breqtrrdi ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 1 · ( normop ‘ 𝑇 ) ) )
98 97 adantl ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 1 · ( normop ‘ 𝑇 ) ) )
99 84 adantr ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
100 1red ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → 1 ∈ ℝ )
101 12 a1i ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( normop ‘ 𝑇 ) ∈ ℝ )
102 51 biimpi ⊢ ( ( normop ‘ 𝑇 ) ≠ 0 → 0 < ( normop ‘ 𝑇 ) )
103 102 adantl ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → 0 < ( normop ‘ 𝑇 ) )
104 ledivmul2 ⊢ ( ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ 0 < ( normop ‘ 𝑇 ) ) ) → ( ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) ≤ 1 ↔ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 1 · ( normop ‘ 𝑇 ) ) ) )
105 99 100 101 103 104 syl112anc ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) ≤ 1 ↔ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 1 · ( normop ‘ 𝑇 ) ) ) )
106 105 ancoms ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) ≤ 1 ↔ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 1 · ( normop ‘ 𝑇 ) ) ) )
107 106 adantrr ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) ≤ 1 ↔ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 1 · ( normop ‘ 𝑇 ) ) ) )
108 98 107 mpbird ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) ≤ 1 )
109 93 108 eqbrtrd ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ≤ 1 )
110 nmoplb ⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ ∧ ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ≤ 1 ) → ( normℎ ‘ ( 𝑆 ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) ≤ ( normop ‘ 𝑆 ) )
111 70 110 mp3an1 ⊢ ( ( ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ ∧ ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ≤ 1 ) → ( normℎ ‘ ( 𝑆 ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) ≤ ( normop ‘ 𝑆 ) )
112 80 109 111 syl2anc ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normℎ ‘ ( 𝑆 ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) ≤ ( normop ‘ 𝑆 ) )
113 77 112 eqbrtrd ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) ≤ ( normop ‘ 𝑆 ) )
114 40 ad2antrl ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ∈ ℝ )
115 10 a1i ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normop ‘ 𝑆 ) ∈ ℝ )
116 102 adantr ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → 0 < ( normop ‘ 𝑇 ) )
117 116 12 jctil ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ 0 < ( normop ‘ 𝑇 ) ) )
118 ledivmul2 ⊢ ( ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ∈ ℝ ∧ ( normop ‘ 𝑆 ) ∈ ℝ ∧ ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ 0 < ( normop ‘ 𝑇 ) ) ) → ( ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) ≤ ( normop ‘ 𝑆 ) ↔ ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) ) )
119 114 115 117 118 syl3anc ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) ≤ ( normop ‘ 𝑆 ) ↔ ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) ) )
120 113 119 mpbid ⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) )
121 37 120 sylanbr ⊢ ( ( ¬ ( normop ‘ 𝑇 ) = 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) )
122 36 121 pm2.61ian ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) )
123 122 ex ⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) ) )
124 16 123 mprgbir ⊢ ( normop ‘ ( 𝑆 ∘ 𝑇 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) )