Theorem nmop0

Description: The norm of the zero operator is zero. (Contributed by NM, 8-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nmop0	⊢ ( normop ‘ 0hop ) = 0

Proof

Step	Hyp	Ref	Expression
1		ho0f	⊢ 0hop : ℋ ⟶ ℋ
2		nmopval	⊢ ( 0hop : ℋ ⟶ ℋ → ( normop ‘ 0hop ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) ) } , ℝ* , < ) )
3	1 2	ax-mp	⊢ ( normop ‘ 0hop ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) ) } , ℝ* , < )
4		ho0val	⊢ ( 𝑦 ∈ ℋ → ( 0hop ‘ 𝑦 ) = 0ℎ )
5	4	fveq2d	⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) = ( normℎ ‘ 0ℎ ) )
6		norm0	⊢ ( normℎ ‘ 0ℎ ) = 0
7	5 6	eqtrdi	⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) = 0 )
8	7	eqeq2d	⊢ ( 𝑦 ∈ ℋ → ( 𝑥 = ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) ↔ 𝑥 = 0 ) )
9	8	anbi2d	⊢ ( 𝑦 ∈ ℋ → ( ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) ) ↔ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = 0 ) ) )
10	9	rexbiia	⊢ ( ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) ) ↔ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = 0 ) )
11		ax-hv0cl	⊢ 0ℎ ∈ ℋ
12		0le1	⊢ 0 ≤ 1
13		fveq2	⊢ ( 𝑦 = 0ℎ → ( normℎ ‘ 𝑦 ) = ( normℎ ‘ 0ℎ ) )
14	13 6	eqtrdi	⊢ ( 𝑦 = 0ℎ → ( normℎ ‘ 𝑦 ) = 0 )
15	14	breq1d	⊢ ( 𝑦 = 0ℎ → ( ( normℎ ‘ 𝑦 ) ≤ 1 ↔ 0 ≤ 1 ) )
16	15	rspcev	⊢ ( ( 0ℎ ∈ ℋ ∧ 0 ≤ 1 ) → ∃ 𝑦 ∈ ℋ ( normℎ ‘ 𝑦 ) ≤ 1 )
17	11 12 16	mp2an	⊢ ∃ 𝑦 ∈ ℋ ( normℎ ‘ 𝑦 ) ≤ 1
18		r19.41v	⊢ ( ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = 0 ) ↔ ( ∃ 𝑦 ∈ ℋ ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = 0 ) )
19	17 18	mpbiran	⊢ ( ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = 0 ) ↔ 𝑥 = 0 )
20	10 19	bitri	⊢ ( ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) ) ↔ 𝑥 = 0 )
21	20	abbii	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) ) } = { 𝑥 ∣ 𝑥 = 0 }
22		df-sn	⊢ { 0 } = { 𝑥 ∣ 𝑥 = 0 }
23	21 22	eqtr4i	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) ) } = { 0 }
24	23	supeq1i	⊢ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) ) } , ℝ* , < ) = sup ( { 0 } , ℝ* , < )
25		xrltso	⊢ < Or ℝ*
26		0xr	⊢ 0 ∈ ℝ*
27		supsn	⊢ ( ( < Or ℝ* ∧ 0 ∈ ℝ* ) → sup ( { 0 } , ℝ* , < ) = 0 )
28	25 26 27	mp2an	⊢ sup ( { 0 } , ℝ* , < ) = 0
29	3 24 28	3eqtri	⊢ ( normop ‘ 0hop ) = 0