This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( normfn ‘ ( ℋ × { 0 } ) ) = 0

Proof

Step Hyp Ref Expression
1 0lnfn ⊢ ( ℋ × { 0 } ) ∈ LinFn
2 lnfnf ⊢ ( ( ℋ × { 0 } ) ∈ LinFn → ( ℋ × { 0 } ) : ℋ ⟶ ℂ )
3 nmfnval ⊢ ( ( ℋ × { 0 } ) : ℋ ⟶ ℂ → ( normfn ‘ ( ℋ × { 0 } ) ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( ( ℋ × { 0 } ) ‘ 𝑦 ) ) ) } , ℝ* , < ) )
4 1 2 3 mp2b ⊢ ( normfn ‘ ( ℋ × { 0 } ) ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( ( ℋ × { 0 } ) ‘ 𝑦 ) ) ) } , ℝ* , < )
5 c0ex ⊢ 0 ∈ V
6 5 fvconst2 ⊢ ( 𝑦 ∈ ℋ → ( ( ℋ × { 0 } ) ‘ 𝑦 ) = 0 )
7 6 fveq2d ⊢ ( 𝑦 ∈ ℋ → ( abs ‘ ( ( ℋ × { 0 } ) ‘ 𝑦 ) ) = ( abs ‘ 0 ) )
8 abs0 ⊢ ( abs ‘ 0 ) = 0
9 7 8 eqtrdi ⊢ ( 𝑦 ∈ ℋ → ( abs ‘ ( ( ℋ × { 0 } ) ‘ 𝑦 ) ) = 0 )
10 9 eqeq2d ⊢ ( 𝑦 ∈ ℋ → ( 𝑥 = ( abs ‘ ( ( ℋ × { 0 } ) ‘ 𝑦 ) ) ↔ 𝑥 = 0 ) )
11 10 anbi2d ⊢ ( 𝑦 ∈ ℋ → ( ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( ( ℋ × { 0 } ) ‘ 𝑦 ) ) ) ↔ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = 0 ) ) )
12 11 rexbiia ⊢ ( ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( ( ℋ × { 0 } ) ‘ 𝑦 ) ) ) ↔ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = 0 ) )
13 ax-hv0cl ⊢ 0ℎ ∈ ℋ
14 0le1 ⊢ 0 ≤ 1
15 fveq2 ⊢ ( 𝑦 = 0ℎ → ( normℎ ‘ 𝑦 ) = ( normℎ ‘ 0ℎ ) )
16 norm0 ⊢ ( normℎ ‘ 0ℎ ) = 0
17 15 16 eqtrdi ⊢ ( 𝑦 = 0ℎ → ( normℎ ‘ 𝑦 ) = 0 )
18 17 breq1d ⊢ ( 𝑦 = 0ℎ → ( ( normℎ ‘ 𝑦 ) ≤ 1 ↔ 0 ≤ 1 ) )
19 18 rspcev ⊢ ( ( 0ℎ ∈ ℋ ∧ 0 ≤ 1 ) → ∃ 𝑦 ∈ ℋ ( normℎ ‘ 𝑦 ) ≤ 1 )
20 13 14 19 mp2an ⊢ ∃ 𝑦 ∈ ℋ ( normℎ ‘ 𝑦 ) ≤ 1
21 r19.41v ⊢ ( ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = 0 ) ↔ ( ∃ 𝑦 ∈ ℋ ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = 0 ) )
22 20 21 mpbiran ⊢ ( ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = 0 ) ↔ 𝑥 = 0 )
23 12 22 bitri ⊢ ( ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( ( ℋ × { 0 } ) ‘ 𝑦 ) ) ) ↔ 𝑥 = 0 )
24 23 abbii ⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( ( ℋ × { 0 } ) ‘ 𝑦 ) ) ) } = { 𝑥 ∣ 𝑥 = 0 }
25 df-sn ⊢ { 0 } = { 𝑥 ∣ 𝑥 = 0 }
26 24 25 eqtr4i ⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( ( ℋ × { 0 } ) ‘ 𝑦 ) ) ) } = { 0 }
27 26 supeq1i ⊢ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( ( ℋ × { 0 } ) ‘ 𝑦 ) ) ) } , ℝ* , < ) = 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 ⊢ ( normfn ‘ ( ℋ × { 0 } ) ) = 0