# 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 ffvelrni $⊢ 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 syl5eq $⊢ 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 ffvelrni $⊢ 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 ∈ ℝ$