Metamath Proof Explorer

Theorem nmfn0

Description: The norm of the identically zero functional is zero. (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion nmfn0 ⊢ norm fn ⁡ ℋ × 0 = 0

Proof

Step Hyp Ref Expression
1 0lnfn ⊢ ℋ × 0 ∈ LinFn
2 lnfnf ⊢ ℋ × 0 ∈ LinFn → ℋ × 0 : ℋ ⟶ ℂ
3 nmfnval ⊢ ℋ × 0 : ℋ ⟶ ℂ → norm fn ⁡ ℋ × 0 = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = ℋ × 0 ⁡ y ℝ * <
4 1 2 3 mp2b ⊢ norm fn ⁡ ℋ × 0 = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = ℋ × 0 ⁡ y ℝ * <
5 c0ex ⊢ 0 ∈ V
6 5 fvconst2 ⊢ y ∈ ℋ → ℋ × 0 ⁡ y = 0
7 6 fveq2d ⊢ y ∈ ℋ → ℋ × 0 ⁡ y = 0
8 abs0 ⊢ 0 = 0
9 7 8 eqtrdi ⊢ y ∈ ℋ → ℋ × 0 ⁡ y = 0
10 9 eqeq2d ⊢ y ∈ ℋ → x = ℋ × 0 ⁡ y ↔ x = 0
11 10 anbi2d ⊢ y ∈ ℋ → norm ℎ ⁡ y ≤ 1 ∧ x = ℋ × 0 ⁡ y ↔ norm ℎ ⁡ y ≤ 1 ∧ x = 0
12 11 rexbiia ⊢ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = ℋ × 0 ⁡ y ↔ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = 0
13 ax-hv0cl ⊢ 0 ℎ ∈ ℋ
14 0le1 ⊢ 0 ≤ 1
15 fveq2 ⊢ y = 0 ℎ → norm ℎ ⁡ y = norm ℎ ⁡ 0 ℎ
16 norm0 ⊢ norm ℎ ⁡ 0 ℎ = 0
17 15 16 eqtrdi ⊢ y = 0 ℎ → norm ℎ ⁡ y = 0
18 17 breq1d ⊢ y = 0 ℎ → norm ℎ ⁡ y ≤ 1 ↔ 0 ≤ 1
19 18 rspcev ⊢ 0 ℎ ∈ ℋ ∧ 0 ≤ 1 → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1
20 13 14 19 mp2an ⊢ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1
21 r19.41v ⊢ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = 0 ↔ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = 0
22 20 21 mpbiran ⊢ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = 0 ↔ x = 0
23 12 22 bitri ⊢ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = ℋ × 0 ⁡ y ↔ x = 0
24 23 abbii ⊢ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = ℋ × 0 ⁡ y = x | x = 0
25 df-sn ⊢ 0 = x | x = 0
26 24 25 eqtr4i ⊢ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = ℋ × 0 ⁡ y = 0
27 26 supeq1i ⊢ sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = ℋ × 0 ⁡ y ℝ * < = sup 0 ℝ * <
28 xrltso ⊢ < Or ℝ *
29 0xr ⊢ 0 ∈ ℝ *
30 supsn ⊢ < Or ℝ * ∧ 0 ∈ ℝ * → sup 0 ℝ * < = 0
31 28 29 30 mp2an ⊢ sup 0 ℝ * < = 0
32 4 27 31 3eqtri ⊢ norm fn ⁡ ℋ × 0 = 0