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 ⊢ T ∈ LinOp
nmcopex.2 ⊢ T ∈ ContOp
Assertion nmcopexi ⊢ norm op ⁡ T ∈ ℝ

Proof

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