Theorem nmopsetn0

Description: The set in the supremum of the operator norm definition df-nmop is nonempty. (Contributed by NM, 9-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nmopsetn0	⊢ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) }

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	⊢ 0ℎ ∈ ℋ
2		norm0	⊢ ( normℎ ‘ 0ℎ ) = 0
3		0le1	⊢ 0 ≤ 1
4	2 3	eqbrtri	⊢ ( normℎ ‘ 0ℎ ) ≤ 1
5		eqid	⊢ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) = ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) )
6	4 5	pm3.2i	⊢ ( ( normℎ ‘ 0ℎ ) ≤ 1 ∧ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) = ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) )
7		fveq2	⊢ ( 𝑦 = 0ℎ → ( normℎ ‘ 𝑦 ) = ( normℎ ‘ 0ℎ ) )
8	7	breq1d	⊢ ( 𝑦 = 0ℎ → ( ( normℎ ‘ 𝑦 ) ≤ 1 ↔ ( normℎ ‘ 0ℎ ) ≤ 1 ) )
9		2fveq3	⊢ ( 𝑦 = 0ℎ → ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) = ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) )
10	9	eqeq2d	⊢ ( 𝑦 = 0ℎ → ( ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ↔ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) = ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ) )
11	8 10	anbi12d	⊢ ( 𝑦 = 0ℎ → ( ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) ↔ ( ( normℎ ‘ 0ℎ ) ≤ 1 ∧ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) = ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ) ) )
12	11	rspcev	⊢ ( ( 0ℎ ∈ ℋ ∧ ( ( normℎ ‘ 0ℎ ) ≤ 1 ∧ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) = ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ) ) → ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) )
13	1 6 12	mp2an	⊢ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) )
14		fvex	⊢ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ∈ V
15		eqeq1	⊢ ( 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) → ( 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ↔ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) )
16	15	anbi2d	⊢ ( 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) → ( ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) ↔ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) ) )
17	16	rexbidv	⊢ ( 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) → ( ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) ↔ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) ) )
18	14 17	elab	⊢ ( ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ↔ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) )
19	13 18	mpbir	⊢ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) }