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