Metamath Proof Explorer

Theorem nmcopexi

Description: The norm of a continuous linear Hilbert space operator exists. Theorem 3.5(i) of Beran p. 99. (Contributed by NM, 5-Feb-2006) (Proof shortened by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nmcopex.1 ⊢ 𝑇 ∈ LinOp
nmcopex.2 ⊢ 𝑇 ∈ ContOp
Assertion nmcopexi ( normop ‘ 𝑇 ) ∈ ℝ

Proof

Step Hyp Ref Expression
1 nmcopex.1 ⊢ 𝑇 ∈ LinOp
2 nmcopex.2 ⊢ 𝑇 ∈ ContOp
3 ax-hv0cl ⊢ 0ℎ ∈ ℋ
4 1rp ⊢ 1 ∈ ℝ+
5 cnopc ⊢ ( ( 𝑇 ∈ ContOp ∧ 0ℎ ∈ ℋ ∧ 1 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ ( 𝑧 −ℎ 0ℎ ) ) < 𝑦 → ( normℎ ‘ ( ( 𝑇 ‘ 𝑧 ) −ℎ ( 𝑇 ‘ 0ℎ ) ) ) < 1 ) )
6 2 3 4 5 mp3an ⊢ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ ( 𝑧 −ℎ 0ℎ ) ) < 𝑦 → ( normℎ ‘ ( ( 𝑇 ‘ 𝑧 ) −ℎ ( 𝑇 ‘ 0ℎ ) ) ) < 1 )
7 hvsub0 ⊢ ( 𝑧 ∈ ℋ → ( 𝑧 −ℎ 0ℎ ) = 𝑧 )
8 7 fveq2d ⊢ ( 𝑧 ∈ ℋ → ( normℎ ‘ ( 𝑧 −ℎ 0ℎ ) ) = ( normℎ ‘ 𝑧 ) )
9 8 breq1d ⊢ ( 𝑧 ∈ ℋ → ( ( normℎ ‘ ( 𝑧 −ℎ 0ℎ ) ) < 𝑦 ↔ ( normℎ ‘ 𝑧 ) < 𝑦 ) )
10 1 lnop0i ⊢ ( 𝑇 ‘ 0ℎ ) = 0ℎ
11 10 oveq2i ⊢ ( ( 𝑇 ‘ 𝑧 ) −ℎ ( 𝑇 ‘ 0ℎ ) ) = ( ( 𝑇 ‘ 𝑧 ) −ℎ 0ℎ )
12 1 lnopfi ⊢ 𝑇 : ℋ ⟶ ℋ
13 12 ffvelcdmi ⊢ ( 𝑧 ∈ ℋ → ( 𝑇 ‘ 𝑧 ) ∈ ℋ )
14 hvsub0 ⊢ ( ( 𝑇 ‘ 𝑧 ) ∈ ℋ → ( ( 𝑇 ‘ 𝑧 ) −ℎ 0ℎ ) = ( 𝑇 ‘ 𝑧 ) )
15 13 14 syl ⊢ ( 𝑧 ∈ ℋ → ( ( 𝑇 ‘ 𝑧 ) −ℎ 0ℎ ) = ( 𝑇 ‘ 𝑧 ) )
16 11 15 eqtrid ⊢ ( 𝑧 ∈ ℋ → ( ( 𝑇 ‘ 𝑧 ) −ℎ ( 𝑇 ‘ 0ℎ ) ) = ( 𝑇 ‘ 𝑧 ) )
17 16 fveq2d ⊢ ( 𝑧 ∈ ℋ → ( normℎ ‘ ( ( 𝑇 ‘ 𝑧 ) −ℎ ( 𝑇 ‘ 0ℎ ) ) ) = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) )
18 17 breq1d ⊢ ( 𝑧 ∈ ℋ → ( ( normℎ ‘ ( ( 𝑇 ‘ 𝑧 ) −ℎ ( 𝑇 ‘ 0ℎ ) ) ) < 1 ↔ ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) )
19 9 18 imbi12d ⊢ ( 𝑧 ∈ ℋ → ( ( ( normℎ ‘ ( 𝑧 −ℎ 0ℎ ) ) < 𝑦 → ( normℎ ‘ ( ( 𝑇 ‘ 𝑧 ) −ℎ ( 𝑇 ‘ 0ℎ ) ) ) < 1 ) ↔ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) ) )
20 19 ralbiia ⊢ ( ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ ( 𝑧 −ℎ 0ℎ ) ) < 𝑦 → ( normℎ ‘ ( ( 𝑇 ‘ 𝑧 ) −ℎ ( 𝑇 ‘ 0ℎ ) ) ) < 1 ) ↔ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) )
21 20 rexbii ⊢ ( ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ ( 𝑧 −ℎ 0ℎ ) ) < 𝑦 → ( normℎ ‘ ( ( 𝑇 ‘ 𝑧 ) −ℎ ( 𝑇 ‘ 0ℎ ) ) ) < 1 ) ↔ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) )
22 6 21 mpbi ⊢ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 )
23 nmopval ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( normop ‘ 𝑇 ) = sup ( { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ* , < ) )
24 12 23 ax-mp ⊢ ( normop ‘ 𝑇 ) = sup ( { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ* , < )
25 12 ffvelcdmi ⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
26 normcl ⊢ ( ( 𝑇 ‘ 𝑥 ) ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
27 25 26 syl ⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
28 10 fveq2i ⊢ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) = ( normℎ ‘ 0ℎ )
29 norm0 ⊢ ( normℎ ‘ 0ℎ ) = 0
30 28 29 eqtri ⊢ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) = 0
31 rpcn ⊢ ( ( 𝑦 / 2 ) ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℂ )
32 1 lnopmuli ⊢ ( ( ( 𝑦 / 2 ) ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) = ( ( 𝑦 / 2 ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) )
33 31 32 sylan ⊢ ( ( ( 𝑦 / 2 ) ∈ ℝ+ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) = ( ( 𝑦 / 2 ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) )
34 33 fveq2d ⊢ ( ( ( 𝑦 / 2 ) ∈ ℝ+ ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) ) = ( normℎ ‘ ( ( 𝑦 / 2 ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) )
35 norm-iii ⊢ ( ( ( 𝑦 / 2 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) → ( normℎ ‘ ( ( 𝑦 / 2 ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( abs ‘ ( 𝑦 / 2 ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
36 31 25 35 syl2an ⊢ ( ( ( 𝑦 / 2 ) ∈ ℝ+ ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( ( 𝑦 / 2 ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( abs ‘ ( 𝑦 / 2 ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
37 rpre ⊢ ( ( 𝑦 / 2 ) ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℝ )
38 rpge0 ⊢ ( ( 𝑦 / 2 ) ∈ ℝ+ → 0 ≤ ( 𝑦 / 2 ) )
39 37 38 absidd ⊢ ( ( 𝑦 / 2 ) ∈ ℝ+ → ( abs ‘ ( 𝑦 / 2 ) ) = ( 𝑦 / 2 ) )
40 39 adantr ⊢ ( ( ( 𝑦 / 2 ) ∈ ℝ+ ∧ 𝑥 ∈ ℋ ) → ( abs ‘ ( 𝑦 / 2 ) ) = ( 𝑦 / 2 ) )
41 40 oveq1d ⊢ ( ( ( 𝑦 / 2 ) ∈ ℝ+ ∧ 𝑥 ∈ ℋ ) → ( ( abs ‘ ( 𝑦 / 2 ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( 𝑦 / 2 ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
42 34 36 41 3eqtrrd ⊢ ( ( ( 𝑦 / 2 ) ∈ ℝ+ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑦 / 2 ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) = ( normℎ ‘ ( 𝑇 ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) ) )
43 22 24 27 30 42 nmcexi ⊢ ( normop ‘ 𝑇 ) ∈ ℝ