Metamath Proof Explorer

Theorem cnlnadjlem7

Description: Lemma for cnlnadji . Helper lemma to show that F is continuous. (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypotheses cnlnadjlem.1 ⊢ 𝑇 ∈ LinOp
cnlnadjlem.2 ⊢ 𝑇 ∈ ContOp
cnlnadjlem.3 ⊢ 𝐺 = ( 𝑔 ∈ ℋ ↦ ( ( 𝑇 ‘ 𝑔 ) ·ih 𝑦 ) )
cnlnadjlem.4 ⊢ 𝐵 = ( ℩ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) )
cnlnadjlem.5 ⊢ 𝐹 = ( 𝑦 ∈ ℋ ↦ 𝐵 )
Assertion cnlnadjlem7 ( 𝐴 ∈ ℋ → ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 cnlnadjlem.1 ⊢ 𝑇 ∈ LinOp
2 cnlnadjlem.2 ⊢ 𝑇 ∈ ContOp
3 cnlnadjlem.3 ⊢ 𝐺 = ( 𝑔 ∈ ℋ ↦ ( ( 𝑇 ‘ 𝑔 ) ·ih 𝑦 ) )
4 cnlnadjlem.4 ⊢ 𝐵 = ( ℩ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) )
5 cnlnadjlem.5 ⊢ 𝐹 = ( 𝑦 ∈ ℋ ↦ 𝐵 )
6 breq1 ⊢ ( ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) = 0 → ( ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ↔ 0 ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ) )
7 1 2 3 4 5 cnlnadjlem4 ⊢ ( 𝐴 ∈ ℋ → ( 𝐹 ‘ 𝐴 ) ∈ ℋ )
8 1 lnopfi ⊢ 𝑇 : ℋ ⟶ ℋ
9 8 ffvelcdmi ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ℋ → ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ℋ )
10 7 9 syl ⊢ ( 𝐴 ∈ ℋ → ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ℋ )
11 hicl ⊢ ( ( ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ·ih 𝐴 ) ∈ ℂ )
12 10 11 mpancom ⊢ ( 𝐴 ∈ ℋ → ( ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ·ih 𝐴 ) ∈ ℂ )
13 12 abscld ⊢ ( 𝐴 ∈ ℋ → ( abs ‘ ( ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ·ih 𝐴 ) ) ∈ ℝ )
14 normcl ⊢ ( ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ) ∈ ℝ )
15 10 14 syl ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ) ∈ ℝ )
16 normcl ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ 𝐴 ) ∈ ℝ )
17 15 16 remulcld ⊢ ( 𝐴 ∈ ℋ → ( ( normℎ ‘ ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ) · ( normℎ ‘ 𝐴 ) ) ∈ ℝ )
18 1 2 nmcopexi ⊢ ( normop ‘ 𝑇 ) ∈ ℝ
19 normcl ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ℋ → ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ )
20 7 19 syl ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ )
21 remulcl ⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ ) → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) ∈ ℝ )
22 18 20 21 sylancr ⊢ ( 𝐴 ∈ ℋ → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) ∈ ℝ )
23 22 16 remulcld ⊢ ( 𝐴 ∈ ℋ → ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) · ( normℎ ‘ 𝐴 ) ) ∈ ℝ )
24 bcs ⊢ ( ( ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( abs ‘ ( ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ·ih 𝐴 ) ) ≤ ( ( normℎ ‘ ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ) · ( normℎ ‘ 𝐴 ) ) )
25 10 24 mpancom ⊢ ( 𝐴 ∈ ℋ → ( abs ‘ ( ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ·ih 𝐴 ) ) ≤ ( ( normℎ ‘ ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ) · ( normℎ ‘ 𝐴 ) ) )
26 normge0 ⊢ ( 𝐴 ∈ ℋ → 0 ≤ ( normℎ ‘ 𝐴 ) )
27 1 2 nmcoplbi ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) )
28 7 27 syl ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) )
29 15 22 16 26 28 lemul1ad ⊢ ( 𝐴 ∈ ℋ → ( ( normℎ ‘ ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ) · ( normℎ ‘ 𝐴 ) ) ≤ ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) · ( normℎ ‘ 𝐴 ) ) )
30 13 17 23 25 29 letrd ⊢ ( 𝐴 ∈ ℋ → ( abs ‘ ( ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ·ih 𝐴 ) ) ≤ ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) · ( normℎ ‘ 𝐴 ) ) )
31 1 2 3 4 5 cnlnadjlem5 ⊢ ( ( 𝐴 ∈ ℋ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℋ ) → ( ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ·ih 𝐴 ) = ( ( 𝐹 ‘ 𝐴 ) ·ih ( 𝐹 ‘ 𝐴 ) ) )
32 7 31 mpdan ⊢ ( 𝐴 ∈ ℋ → ( ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ·ih 𝐴 ) = ( ( 𝐹 ‘ 𝐴 ) ·ih ( 𝐹 ‘ 𝐴 ) ) )
33 32 fveq2d ⊢ ( 𝐴 ∈ ℋ → ( abs ‘ ( ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ·ih 𝐴 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) ·ih ( 𝐹 ‘ 𝐴 ) ) ) )
34 hiidrcl ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ℋ → ( ( 𝐹 ‘ 𝐴 ) ·ih ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ )
35 7 34 syl ⊢ ( 𝐴 ∈ ℋ → ( ( 𝐹 ‘ 𝐴 ) ·ih ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ )
36 hiidge0 ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ℋ → 0 ≤ ( ( 𝐹 ‘ 𝐴 ) ·ih ( 𝐹 ‘ 𝐴 ) ) )
37 7 36 syl ⊢ ( 𝐴 ∈ ℋ → 0 ≤ ( ( 𝐹 ‘ 𝐴 ) ·ih ( 𝐹 ‘ 𝐴 ) ) )
38 35 37 absidd ⊢ ( 𝐴 ∈ ℋ → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) ·ih ( 𝐹 ‘ 𝐴 ) ) ) = ( ( 𝐹 ‘ 𝐴 ) ·ih ( 𝐹 ‘ 𝐴 ) ) )
39 normsq ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ℋ → ( ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ↑ 2 ) = ( ( 𝐹 ‘ 𝐴 ) ·ih ( 𝐹 ‘ 𝐴 ) ) )
40 7 39 syl ⊢ ( 𝐴 ∈ ℋ → ( ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ↑ 2 ) = ( ( 𝐹 ‘ 𝐴 ) ·ih ( 𝐹 ‘ 𝐴 ) ) )
41 20 recnd ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ℂ )
42 41 sqvald ⊢ ( 𝐴 ∈ ℋ → ( ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ↑ 2 ) = ( ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) )
43 40 42 eqtr3d ⊢ ( 𝐴 ∈ ℋ → ( ( 𝐹 ‘ 𝐴 ) ·ih ( 𝐹 ‘ 𝐴 ) ) = ( ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) )
44 33 38 43 3eqtrd ⊢ ( 𝐴 ∈ ℋ → ( abs ‘ ( ( 𝑇 ‘ ( 𝐹 ‘ 𝐴 ) ) ·ih 𝐴 ) ) = ( ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) )
45 16 recnd ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ 𝐴 ) ∈ ℂ )
46 18 recni ⊢ ( normop ‘ 𝑇 ) ∈ ℂ
47 mul32 ⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℂ ∧ ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ℂ ∧ ( normℎ ‘ 𝐴 ) ∈ ℂ ) → ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) · ( normℎ ‘ 𝐴 ) ) = ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) )
48 46 47 mp3an1 ⊢ ( ( ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ℂ ∧ ( normℎ ‘ 𝐴 ) ∈ ℂ ) → ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) · ( normℎ ‘ 𝐴 ) ) = ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) )
49 41 45 48 syl2anc ⊢ ( 𝐴 ∈ ℋ → ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) · ( normℎ ‘ 𝐴 ) ) = ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) )
50 30 44 49 3brtr3d ⊢ ( 𝐴 ∈ ℋ → ( ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) ≤ ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) )
51 50 adantr ⊢ ( ( 𝐴 ∈ ℋ ∧ ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ≠ 0 ) → ( ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) ≤ ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) )
52 20 adantr ⊢ ( ( 𝐴 ∈ ℋ ∧ ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ≠ 0 ) → ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ )
53 remulcl ⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ ( normℎ ‘ 𝐴 ) ∈ ℝ ) → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ∈ ℝ )
54 18 16 53 sylancr ⊢ ( 𝐴 ∈ ℋ → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ∈ ℝ )
55 54 adantr ⊢ ( ( 𝐴 ∈ ℋ ∧ ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ≠ 0 ) → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ∈ ℝ )
56 normge0 ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ℋ → 0 ≤ ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) )
57 0re ⊢ 0 ∈ ℝ
58 leltne ⊢ ( ( 0 ∈ ℝ ∧ ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) → ( 0 < ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ↔ ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ≠ 0 ) )
59 57 58 mp3an1 ⊢ ( ( ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) → ( 0 < ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ↔ ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ≠ 0 ) )
60 19 56 59 syl2anc ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ℋ → ( 0 < ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ↔ ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ≠ 0 ) )
61 60 biimpar ⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ℋ ∧ ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ≠ 0 ) → 0 < ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) )
62 7 61 sylan ⊢ ( ( 𝐴 ∈ ℋ ∧ ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ≠ 0 ) → 0 < ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) )
63 lemul1 ⊢ ( ( ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ ∧ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ∈ ℝ ∧ ( ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ ∧ 0 < ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) ) → ( ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ↔ ( ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) ≤ ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) ) )
64 52 55 52 62 63 syl112anc ⊢ ( ( 𝐴 ∈ ℋ ∧ ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ≠ 0 ) → ( ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ↔ ( ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) ≤ ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) · ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ) ) )
65 51 64 mpbird ⊢ ( ( 𝐴 ∈ ℋ ∧ ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ≠ 0 ) → ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )
66 nmopge0 ⊢ ( 𝑇 : ℋ ⟶ ℋ → 0 ≤ ( normop ‘ 𝑇 ) )
67 8 66 ax-mp ⊢ 0 ≤ ( normop ‘ 𝑇 )
68 mulge0 ⊢ ( ( ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ 0 ≤ ( normop ‘ 𝑇 ) ) ∧ ( ( normℎ ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( normℎ ‘ 𝐴 ) ) ) → 0 ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )
69 18 67 68 mpanl12 ⊢ ( ( ( normℎ ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( normℎ ‘ 𝐴 ) ) → 0 ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )
70 16 26 69 syl2anc ⊢ ( 𝐴 ∈ ℋ → 0 ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )
71 6 65 70 pm2.61ne ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ ( 𝐹 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )