Metamath Proof Explorer

Theorem nmosetn0

Description: The set in the supremum of the operator norm definition df-nmoo is nonempty. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmosetn0.1 ⊢ X = BaseSet ⁡ U
nmosetn0.5 ⊢ Z = 0 vec ⁡ U
nmosetn0.4 ⊢ M = norm CV ⁡ U
Assertion nmosetn0 ⊢ U ∈ NrmCVec → N ⁡ T ⁡ Z ∈ x | ∃ y ∈ X M ⁡ y ≤ 1 ∧ x = N ⁡ T ⁡ y

Proof

Step Hyp Ref Expression
1 nmosetn0.1 ⊢ X = BaseSet ⁡ U
2 nmosetn0.5 ⊢ Z = 0 vec ⁡ U
3 nmosetn0.4 ⊢ M = norm CV ⁡ U
4 1 2 nvzcl ⊢ U ∈ NrmCVec → Z ∈ X
5 2 3 nvz0 ⊢ U ∈ NrmCVec → M ⁡ Z = 0
6 0le1 ⊢ 0 ≤ 1
7 5 6 eqbrtrdi ⊢ U ∈ NrmCVec → M ⁡ Z ≤ 1
8 eqid ⊢ N ⁡ T ⁡ Z = N ⁡ T ⁡ Z
9 7 8 jctir ⊢ U ∈ NrmCVec → M ⁡ Z ≤ 1 ∧ N ⁡ T ⁡ Z = N ⁡ T ⁡ Z
10 fveq2 ⊢ y = Z → M ⁡ y = M ⁡ Z
11 10 breq1d ⊢ y = Z → M ⁡ y ≤ 1 ↔ M ⁡ Z ≤ 1
12 2fveq3 ⊢ y = Z → N ⁡ T ⁡ y = N ⁡ T ⁡ Z
13 12 eqeq2d ⊢ y = Z → N ⁡ T ⁡ Z = N ⁡ T ⁡ y ↔ N ⁡ T ⁡ Z = N ⁡ T ⁡ Z
14 11 13 anbi12d ⊢ y = Z → M ⁡ y ≤ 1 ∧ N ⁡ T ⁡ Z = N ⁡ T ⁡ y ↔ M ⁡ Z ≤ 1 ∧ N ⁡ T ⁡ Z = N ⁡ T ⁡ Z
15 14 rspcev ⊢ Z ∈ X ∧ M ⁡ Z ≤ 1 ∧ N ⁡ T ⁡ Z = N ⁡ T ⁡ Z → ∃ y ∈ X M ⁡ y ≤ 1 ∧ N ⁡ T ⁡ Z = N ⁡ T ⁡ y
16 4 9 15 syl2anc ⊢ U ∈ NrmCVec → ∃ y ∈ X M ⁡ y ≤ 1 ∧ N ⁡ T ⁡ Z = N ⁡ T ⁡ y
17 fvex ⊢ N ⁡ T ⁡ Z ∈ V
18 eqeq1 ⊢ x = N ⁡ T ⁡ Z → x = N ⁡ T ⁡ y ↔ N ⁡ T ⁡ Z = N ⁡ T ⁡ y
19 18 anbi2d ⊢ x = N ⁡ T ⁡ Z → M ⁡ y ≤ 1 ∧ x = N ⁡ T ⁡ y ↔ M ⁡ y ≤ 1 ∧ N ⁡ T ⁡ Z = N ⁡ T ⁡ y
20 19 rexbidv ⊢ x = N ⁡ T ⁡ Z → ∃ y ∈ X M ⁡ y ≤ 1 ∧ x = N ⁡ T ⁡ y ↔ ∃ y ∈ X M ⁡ y ≤ 1 ∧ N ⁡ T ⁡ Z = N ⁡ T ⁡ y
21 17 20 elab ⊢ N ⁡ T ⁡ Z ∈ x | ∃ y ∈ X M ⁡ y ≤ 1 ∧ x = N ⁡ T ⁡ y ↔ ∃ y ∈ X M ⁡ y ≤ 1 ∧ N ⁡ T ⁡ Z = N ⁡ T ⁡ y
22 16 21 sylibr ⊢ U ∈ NrmCVec → N ⁡ T ⁡ Z ∈ x | ∃ y ∈ X M ⁡ y ≤ 1 ∧ x = N ⁡ T ⁡ y