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

Metamath Proof Explorer

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ℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) }