Detailed syntax breakdown of Definition df-nmfn
Step | Hyp | Ref
| Expression |
1 | | cnmf 29307 |
. 2
class
normfn |
2 | | vt |
. . 3
setvar 𝑡 |
3 | | cc 10868 |
. . . 4
class
ℂ |
4 | | chba 29275 |
. . . 4
class
ℋ |
5 | | cmap 8596 |
. . . 4
class
↑m |
6 | 3, 4, 5 | co 7269 |
. . 3
class (ℂ
↑m ℋ) |
7 | | vz |
. . . . . . . . . 10
setvar 𝑧 |
8 | 7 | cv 1541 |
. . . . . . . . 9
class 𝑧 |
9 | | cno 29279 |
. . . . . . . . 9
class
normℎ |
10 | 8, 9 | cfv 6431 |
. . . . . . . 8
class
(normℎ‘𝑧) |
11 | | c1 10871 |
. . . . . . . 8
class
1 |
12 | | cle 11009 |
. . . . . . . 8
class
≤ |
13 | 10, 11, 12 | wbr 5079 |
. . . . . . 7
wff
(normℎ‘𝑧) ≤ 1 |
14 | | vx |
. . . . . . . . 9
setvar 𝑥 |
15 | 14 | cv 1541 |
. . . . . . . 8
class 𝑥 |
16 | 2 | cv 1541 |
. . . . . . . . . 10
class 𝑡 |
17 | 8, 16 | cfv 6431 |
. . . . . . . . 9
class (𝑡‘𝑧) |
18 | | cabs 14941 |
. . . . . . . . 9
class
abs |
19 | 17, 18 | cfv 6431 |
. . . . . . . 8
class
(abs‘(𝑡‘𝑧)) |
20 | 15, 19 | wceq 1542 |
. . . . . . 7
wff 𝑥 = (abs‘(𝑡‘𝑧)) |
21 | 13, 20 | wa 396 |
. . . . . 6
wff
((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡‘𝑧))) |
22 | 21, 7, 4 | wrex 3067 |
. . . . 5
wff
∃𝑧 ∈
ℋ ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡‘𝑧))) |
23 | 22, 14 | cab 2717 |
. . . 4
class {𝑥 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡‘𝑧)))} |
24 | | cxr 11007 |
. . . 4
class
ℝ* |
25 | | clt 11008 |
. . . 4
class
< |
26 | 23, 24, 25 | csup 9175 |
. . 3
class
sup({𝑥 ∣
∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡‘𝑧)))}, ℝ*, <
) |
27 | 2, 6, 26 | cmpt 5162 |
. 2
class (𝑡 ∈ (ℂ
↑m ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡‘𝑧)))}, ℝ*, <
)) |
28 | 1, 27 | wceq 1542 |
1
wff
normfn = (𝑡 ∈ (ℂ ↑m ℋ)
↦ sup({𝑥 ∣
∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡‘𝑧)))}, ℝ*, <
)) |