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