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 ℎ ⁡ T ⁡ 0 ℎ ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y

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 ℎ ⁡ T ⁡ 0 ℎ = norm ℎ ⁡ T ⁡ 0 ℎ
6 4 5 pm3.2i ⊢ norm ℎ ⁡ 0 ℎ ≤ 1 ∧ norm ℎ ⁡ T ⁡ 0 ℎ = norm ℎ ⁡ T ⁡ 0 ℎ
7 fveq2 ⊢ y = 0 ℎ → norm ℎ ⁡ y = norm ℎ ⁡ 0 ℎ
8 7 breq1d ⊢ y = 0 ℎ → norm ℎ ⁡ y ≤ 1 ↔ norm ℎ ⁡ 0 ℎ ≤ 1
9 2fveq3 ⊢ y = 0 ℎ → norm ℎ ⁡ T ⁡ y = norm ℎ ⁡ T ⁡ 0 ℎ
10 9 eqeq2d ⊢ y = 0 ℎ → norm ℎ ⁡ T ⁡ 0 ℎ = norm ℎ ⁡ T ⁡ y ↔ norm ℎ ⁡ T ⁡ 0 ℎ = norm ℎ ⁡ T ⁡ 0 ℎ
11 8 10 anbi12d ⊢ y = 0 ℎ → norm ℎ ⁡ y ≤ 1 ∧ norm ℎ ⁡ T ⁡ 0 ℎ = norm ℎ ⁡ T ⁡ y ↔ norm ℎ ⁡ 0 ℎ ≤ 1 ∧ norm ℎ ⁡ T ⁡ 0 ℎ = norm ℎ ⁡ T ⁡ 0 ℎ
12 11 rspcev ⊢ 0 ℎ ∈ ℋ ∧ norm ℎ ⁡ 0 ℎ ≤ 1 ∧ norm ℎ ⁡ T ⁡ 0 ℎ = norm ℎ ⁡ T ⁡ 0 ℎ → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ norm ℎ ⁡ T ⁡ 0 ℎ = norm ℎ ⁡ T ⁡ y
13 1 6 12 mp2an ⊢ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ norm ℎ ⁡ T ⁡ 0 ℎ = norm ℎ ⁡ T ⁡ y
14 fvex ⊢ norm ℎ ⁡ T ⁡ 0 ℎ ∈ V
15 eqeq1 ⊢ x = norm ℎ ⁡ T ⁡ 0 ℎ → x = norm ℎ ⁡ T ⁡ y ↔ norm ℎ ⁡ T ⁡ 0 ℎ = norm ℎ ⁡ T ⁡ y
16 15 anbi2d ⊢ x = norm ℎ ⁡ T ⁡ 0 ℎ → norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ↔ norm ℎ ⁡ y ≤ 1 ∧ norm ℎ ⁡ T ⁡ 0 ℎ = norm ℎ ⁡ T ⁡ y
17 16 rexbidv ⊢ x = norm ℎ ⁡ T ⁡ 0 ℎ → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ↔ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ norm ℎ ⁡ T ⁡ 0 ℎ = norm ℎ ⁡ T ⁡ y
18 14 17 elab ⊢ norm ℎ ⁡ T ⁡ 0 ℎ ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ↔ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ norm ℎ ⁡ T ⁡ 0 ℎ = norm ℎ ⁡ T ⁡ y
19 13 18 mpbir ⊢ norm ℎ ⁡ T ⁡ 0 ℎ ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y