Metamath Proof Explorer

Theorem nmcfnex

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

Ref Expression
Assertion nmcfnex ⊢ T ∈ LinFn ∧ T ∈ ContFn → norm fn ⁡ T ∈ ℝ

Proof

Step Hyp Ref Expression
1 elin ⊢ T ∈ LinFn ∩ ContFn ↔ T ∈ LinFn ∧ T ∈ ContFn
2 fveq2 ⊢ T = if T ∈ LinFn ∩ ContFn T ℋ × 0 → norm fn ⁡ T = norm fn ⁡ if T ∈ LinFn ∩ ContFn T ℋ × 0
3 2 eleq1d ⊢ T = if T ∈ LinFn ∩ ContFn T ℋ × 0 → norm fn ⁡ T ∈ ℝ ↔ norm fn ⁡ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ ℝ
4 0lnfn ⊢ ℋ × 0 ∈ LinFn
5 0cnfn ⊢ ℋ × 0 ∈ ContFn
6 elin ⊢ ℋ × 0 ∈ LinFn ∩ ContFn ↔ ℋ × 0 ∈ LinFn ∧ ℋ × 0 ∈ ContFn
7 4 5 6 mpbir2an ⊢ ℋ × 0 ∈ LinFn ∩ ContFn
8 7 elimel ⊢ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ LinFn ∩ ContFn
9 elin ⊢ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ LinFn ∩ ContFn ↔ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ LinFn ∧ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ ContFn
10 8 9 mpbi ⊢ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ LinFn ∧ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ ContFn
11 10 simpli ⊢ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ LinFn
12 10 simpri ⊢ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ ContFn
13 11 12 nmcfnexi ⊢ norm fn ⁡ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ ℝ
14 3 13 dedth ⊢ T ∈ LinFn ∩ ContFn → norm fn ⁡ T ∈ ℝ
15 1 14 sylbir ⊢ T ∈ LinFn ∧ T ∈ ContFn → norm fn ⁡ T ∈ ℝ