Metamath Proof Explorer

Theorem nmcopex

Description: The norm of a continuous linear Hilbert space operator exists. Theorem 3.5(i) of Beran p. 99. (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmcopex ⊢ T ∈ LinOp ∧ T ∈ ContOp → norm op ⁡ T ∈ ℝ

Proof

Step Hyp Ref Expression
1 elin ⊢ T ∈ LinOp ∩ ContOp ↔ T ∈ LinOp ∧ T ∈ ContOp
2 fveq2 ⊢ T = if T ∈ LinOp ∩ ContOp T I ↾ ℋ → norm op ⁡ T = norm op ⁡ if T ∈ LinOp ∩ ContOp T I ↾ ℋ
3 2 eleq1d ⊢ T = if T ∈ LinOp ∩ ContOp T I ↾ ℋ → norm op ⁡ T ∈ ℝ ↔ norm op ⁡ if T ∈ LinOp ∩ ContOp T I ↾ ℋ ∈ ℝ
4 idlnop ⊢ I ↾ ℋ ∈ LinOp
5 idcnop ⊢ I ↾ ℋ ∈ ContOp
6 elin ⊢ I ↾ ℋ ∈ LinOp ∩ ContOp ↔ I ↾ ℋ ∈ LinOp ∧ I ↾ ℋ ∈ ContOp
7 4 5 6 mpbir2an ⊢ I ↾ ℋ ∈ LinOp ∩ ContOp
8 7 elimel ⊢ if T ∈ LinOp ∩ ContOp T I ↾ ℋ ∈ LinOp ∩ ContOp
9 elin ⊢ if T ∈ LinOp ∩ ContOp T I ↾ ℋ ∈ LinOp ∩ ContOp ↔ if T ∈ LinOp ∩ ContOp T I ↾ ℋ ∈ LinOp ∧ if T ∈ LinOp ∩ ContOp T I ↾ ℋ ∈ ContOp
10 8 9 mpbi ⊢ if T ∈ LinOp ∩ ContOp T I ↾ ℋ ∈ LinOp ∧ if T ∈ LinOp ∩ ContOp T I ↾ ℋ ∈ ContOp
11 10 simpli ⊢ if T ∈ LinOp ∩ ContOp T I ↾ ℋ ∈ LinOp
12 10 simpri ⊢ if T ∈ LinOp ∩ ContOp T I ↾ ℋ ∈ ContOp
13 11 12 nmcopexi ⊢ norm op ⁡ if T ∈ LinOp ∩ ContOp T I ↾ ℋ ∈ ℝ
14 3 13 dedth ⊢ T ∈ LinOp ∩ ContOp → norm op ⁡ T ∈ ℝ
15 1 14 sylbir ⊢ T ∈ LinOp ∧ T ∈ ContOp → norm op ⁡ T ∈ ℝ