This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nmophmi

Description: The norm of the scalar product of a bounded linear operator. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmophm.1 ⊢ 𝑇 ∈ BndLinOp
Assertion nmophmi ( 𝐴 ∈ ℂ → ( normop ‘ ( 𝐴 ·op 𝑇 ) ) = ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) )

Proof

Step Hyp Ref Expression
1 nmophm.1 ⊢ 𝑇 ∈ BndLinOp
2 bdopf ⊢ ( 𝑇 ∈ BndLinOp → 𝑇 : ℋ ⟶ ℋ )
3 1 2 ax-mp ⊢ 𝑇 : ℋ ⟶ ℋ
4 homval ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝐴 ·op 𝑇 ) ‘ 𝑥 ) = ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑥 ) ) )
5 3 4 mp3an2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( ( 𝐴 ·op 𝑇 ) ‘ 𝑥 ) = ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑥 ) ) )
6 5 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑥 ) ) = ( normℎ ‘ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) )
7 3 ffvelcdmi ⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
8 norm-iii ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) → ( normℎ ‘ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( abs ‘ 𝐴 ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
9 7 8 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( abs ‘ 𝐴 ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
10 6 9 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑥 ) ) = ( ( abs ‘ 𝐴 ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
11 10 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑥 ) ) = ( ( abs ‘ 𝐴 ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
12 normcl ⊢ ( ( 𝑇 ‘ 𝑥 ) ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
13 7 12 syl ⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
14 13 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
15 abscl ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
16 absge0 ⊢ ( 𝐴 ∈ ℂ → 0 ≤ ( abs ‘ 𝐴 ) )
17 15 16 jca ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐴 ) ) )
18 17 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐴 ) ) )
19 nmoplb ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( normop ‘ 𝑇 ) )
20 3 19 mp3an1 ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( normop ‘ 𝑇 ) )
21 20 adantll ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( normop ‘ 𝑇 ) )
22 nmopre ⊢ ( 𝑇 ∈ BndLinOp → ( normop ‘ 𝑇 ) ∈ ℝ )
23 1 22 ax-mp ⊢ ( normop ‘ 𝑇 ) ∈ ℝ
24 lemul2a ⊢ ( ( ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ ( normop ‘ 𝑇 ) ∈ ℝ ∧ ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐴 ) ) ) ∧ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( normop ‘ 𝑇 ) ) → ( ( abs ‘ 𝐴 ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) )
25 23 24 mp3anl2 ⊢ ( ( ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐴 ) ) ) ∧ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( normop ‘ 𝑇 ) ) → ( ( abs ‘ 𝐴 ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) )
26 14 18 21 25 syl21anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( ( abs ‘ 𝐴 ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) )
27 11 26 eqbrtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) )
28 27 ex ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) ) )
29 28 ralrimiva ⊢ ( 𝐴 ∈ ℂ → ∀ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) ) )
30 homulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝐴 ·op 𝑇 ) : ℋ ⟶ ℋ )
31 3 30 mpan2 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ·op 𝑇 ) : ℋ ⟶ ℋ )
32 remulcl ⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) → ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) ∈ ℝ )
33 15 23 32 sylancl ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) ∈ ℝ )
34 33 rexrd ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) ∈ ℝ* )
35 nmopub ⊢ ( ( ( 𝐴 ·op 𝑇 ) : ℋ ⟶ ℋ ∧ ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) ∈ ℝ* ) → ( ( normop ‘ ( 𝐴 ·op 𝑇 ) ) ≤ ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) ↔ ∀ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) ) ) )
36 31 34 35 syl2anc ⊢ ( 𝐴 ∈ ℂ → ( ( normop ‘ ( 𝐴 ·op 𝑇 ) ) ≤ ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) ↔ ∀ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) ) ) )
37 29 36 mpbird ⊢ ( 𝐴 ∈ ℂ → ( normop ‘ ( 𝐴 ·op 𝑇 ) ) ≤ ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) )
38 fveq2 ⊢ ( 𝐴 = 0 → ( abs ‘ 𝐴 ) = ( abs ‘ 0 ) )
39 abs0 ⊢ ( abs ‘ 0 ) = 0
40 38 39 eqtrdi ⊢ ( 𝐴 = 0 → ( abs ‘ 𝐴 ) = 0 )
41 40 oveq1d ⊢ ( 𝐴 = 0 → ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) = ( 0 · ( normop ‘ 𝑇 ) ) )
42 23 recni ⊢ ( normop ‘ 𝑇 ) ∈ ℂ
43 42 mul02i ⊢ ( 0 · ( normop ‘ 𝑇 ) ) = 0
44 41 43 eqtrdi ⊢ ( 𝐴 = 0 → ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) = 0 )
45 44 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 = 0 ) → ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) = 0 )
46 nmopge0 ⊢ ( ( 𝐴 ·op 𝑇 ) : ℋ ⟶ ℋ → 0 ≤ ( normop ‘ ( 𝐴 ·op 𝑇 ) ) )
47 31 46 syl ⊢ ( 𝐴 ∈ ℂ → 0 ≤ ( normop ‘ ( 𝐴 ·op 𝑇 ) ) )
48 47 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 = 0 ) → 0 ≤ ( normop ‘ ( 𝐴 ·op 𝑇 ) ) )
49 45 48 eqbrtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 = 0 ) → ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) ≤ ( normop ‘ ( 𝐴 ·op 𝑇 ) ) )
50 nmoplb ⊢ ( ( ( 𝐴 ·op 𝑇 ) : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑥 ) ) ≤ ( normop ‘ ( 𝐴 ·op 𝑇 ) ) )
51 31 50 syl3an1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑥 ) ) ≤ ( normop ‘ ( 𝐴 ·op 𝑇 ) ) )
52 51 3expa ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑥 ) ) ≤ ( normop ‘ ( 𝐴 ·op 𝑇 ) ) )
53 11 52 eqbrtrrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( ( abs ‘ 𝐴 ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( normop ‘ ( 𝐴 ·op 𝑇 ) ) )
54 53 adantllr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℋ ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( ( abs ‘ 𝐴 ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( normop ‘ ( 𝐴 ·op 𝑇 ) ) )
55 13 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
56 nmopxr ⊢ ( ( 𝐴 ·op 𝑇 ) : ℋ ⟶ ℋ → ( normop ‘ ( 𝐴 ·op 𝑇 ) ) ∈ ℝ* )
57 31 56 syl ⊢ ( 𝐴 ∈ ℂ → ( normop ‘ ( 𝐴 ·op 𝑇 ) ) ∈ ℝ* )
58 nmopgtmnf ⊢ ( ( 𝐴 ·op 𝑇 ) : ℋ ⟶ ℋ → -∞ < ( normop ‘ ( 𝐴 ·op 𝑇 ) ) )
59 31 58 syl ⊢ ( 𝐴 ∈ ℂ → -∞ < ( normop ‘ ( 𝐴 ·op 𝑇 ) ) )
60 xrre ⊢ ( ( ( ( normop ‘ ( 𝐴 ·op 𝑇 ) ) ∈ ℝ* ∧ ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) ∈ ℝ ) ∧ ( -∞ < ( normop ‘ ( 𝐴 ·op 𝑇 ) ) ∧ ( normop ‘ ( 𝐴 ·op 𝑇 ) ) ≤ ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) ) ) → ( normop ‘ ( 𝐴 ·op 𝑇 ) ) ∈ ℝ )
61 57 33 59 37 60 syl22anc ⊢ ( 𝐴 ∈ ℂ → ( normop ‘ ( 𝐴 ·op 𝑇 ) ) ∈ ℝ )
62 61 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℋ ) → ( normop ‘ ( 𝐴 ·op 𝑇 ) ) ∈ ℝ )
63 15 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℋ ) → ( abs ‘ 𝐴 ) ∈ ℝ )
64 absgt0 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ≠ 0 ↔ 0 < ( abs ‘ 𝐴 ) ) )
65 64 biimpa ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 0 < ( abs ‘ 𝐴 ) )
66 65 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℋ ) → 0 < ( abs ‘ 𝐴 ) )
67 lemuldiv2 ⊢ ( ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ ( normop ‘ ( 𝐴 ·op 𝑇 ) ) ∈ ℝ ∧ ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( abs ‘ 𝐴 ) ) ) → ( ( ( abs ‘ 𝐴 ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( normop ‘ ( 𝐴 ·op 𝑇 ) ) ↔ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normop ‘ ( 𝐴 ·op 𝑇 ) ) / ( abs ‘ 𝐴 ) ) ) )
68 55 62 63 66 67 syl112anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℋ ) → ( ( ( abs ‘ 𝐴 ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( normop ‘ ( 𝐴 ·op 𝑇 ) ) ↔ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normop ‘ ( 𝐴 ·op 𝑇 ) ) / ( abs ‘ 𝐴 ) ) ) )
69 68 adantr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℋ ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( ( ( abs ‘ 𝐴 ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( normop ‘ ( 𝐴 ·op 𝑇 ) ) ↔ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normop ‘ ( 𝐴 ·op 𝑇 ) ) / ( abs ‘ 𝐴 ) ) ) )
70 54 69 mpbid ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℋ ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normop ‘ ( 𝐴 ·op 𝑇 ) ) / ( abs ‘ 𝐴 ) ) )
71 70 ex ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℋ ) → ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normop ‘ ( 𝐴 ·op 𝑇 ) ) / ( abs ‘ 𝐴 ) ) ) )
72 71 ralrimiva ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ∀ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normop ‘ ( 𝐴 ·op 𝑇 ) ) / ( abs ‘ 𝐴 ) ) ) )
73 61 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( normop ‘ ( 𝐴 ·op 𝑇 ) ) ∈ ℝ )
74 15 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
75 abs00 ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )
76 75 necon3bid ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ≠ 0 ) )
77 76 biimpar ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ≠ 0 )
78 73 74 77 redivcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( normop ‘ ( 𝐴 ·op 𝑇 ) ) / ( abs ‘ 𝐴 ) ) ∈ ℝ )
79 78 rexrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( normop ‘ ( 𝐴 ·op 𝑇 ) ) / ( abs ‘ 𝐴 ) ) ∈ ℝ* )
80 nmopub ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ ( ( normop ‘ ( 𝐴 ·op 𝑇 ) ) / ( abs ‘ 𝐴 ) ) ∈ ℝ* ) → ( ( normop ‘ 𝑇 ) ≤ ( ( normop ‘ ( 𝐴 ·op 𝑇 ) ) / ( abs ‘ 𝐴 ) ) ↔ ∀ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normop ‘ ( 𝐴 ·op 𝑇 ) ) / ( abs ‘ 𝐴 ) ) ) ) )
81 3 79 80 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( normop ‘ 𝑇 ) ≤ ( ( normop ‘ ( 𝐴 ·op 𝑇 ) ) / ( abs ‘ 𝐴 ) ) ↔ ∀ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normop ‘ ( 𝐴 ·op 𝑇 ) ) / ( abs ‘ 𝐴 ) ) ) ) )
82 72 81 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( normop ‘ 𝑇 ) ≤ ( ( normop ‘ ( 𝐴 ·op 𝑇 ) ) / ( abs ‘ 𝐴 ) ) )
83 23 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( normop ‘ 𝑇 ) ∈ ℝ )
84 lemuldiv2 ⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ ( normop ‘ ( 𝐴 ·op 𝑇 ) ) ∈ ℝ ∧ ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( abs ‘ 𝐴 ) ) ) → ( ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) ≤ ( normop ‘ ( 𝐴 ·op 𝑇 ) ) ↔ ( normop ‘ 𝑇 ) ≤ ( ( normop ‘ ( 𝐴 ·op 𝑇 ) ) / ( abs ‘ 𝐴 ) ) ) )
85 83 73 74 65 84 syl112anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) ≤ ( normop ‘ ( 𝐴 ·op 𝑇 ) ) ↔ ( normop ‘ 𝑇 ) ≤ ( ( normop ‘ ( 𝐴 ·op 𝑇 ) ) / ( abs ‘ 𝐴 ) ) ) )
86 82 85 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) ≤ ( normop ‘ ( 𝐴 ·op 𝑇 ) ) )
87 49 86 pm2.61dane ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) ≤ ( normop ‘ ( 𝐴 ·op 𝑇 ) ) )
88 61 33 letri3d ⊢ ( 𝐴 ∈ ℂ → ( ( normop ‘ ( 𝐴 ·op 𝑇 ) ) = ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) ↔ ( ( normop ‘ ( 𝐴 ·op 𝑇 ) ) ≤ ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) ∧ ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) ≤ ( normop ‘ ( 𝐴 ·op 𝑇 ) ) ) ) )
89 37 87 88 mpbir2and ⊢ ( 𝐴 ∈ ℂ → ( normop ‘ ( 𝐴 ·op 𝑇 ) ) = ( ( abs ‘ 𝐴 ) · ( normop ‘ 𝑇 ) ) )