Detailed syntax breakdown of Definition df-nmo
| Step | Hyp | Ref
| Expression |
| 1 | | cnmo 24726 |
. 2
class
normOp |
| 2 | | vs |
. . 3
setvar 𝑠 |
| 3 | | vt |
. . 3
setvar 𝑡 |
| 4 | | cngp 24590 |
. . 3
class
NrmGrp |
| 5 | | vf |
. . . 4
setvar 𝑓 |
| 6 | 2 | cv 1539 |
. . . . 5
class 𝑠 |
| 7 | 3 | cv 1539 |
. . . . 5
class 𝑡 |
| 8 | | cghm 19230 |
. . . . 5
class
GrpHom |
| 9 | 6, 7, 8 | co 7431 |
. . . 4
class (𝑠 GrpHom 𝑡) |
| 10 | | vx |
. . . . . . . . . . 11
setvar 𝑥 |
| 11 | 10 | cv 1539 |
. . . . . . . . . 10
class 𝑥 |
| 12 | 5 | cv 1539 |
. . . . . . . . . 10
class 𝑓 |
| 13 | 11, 12 | cfv 6561 |
. . . . . . . . 9
class (𝑓‘𝑥) |
| 14 | | cnm 24589 |
. . . . . . . . . 10
class
norm |
| 15 | 7, 14 | cfv 6561 |
. . . . . . . . 9
class
(norm‘𝑡) |
| 16 | 13, 15 | cfv 6561 |
. . . . . . . 8
class
((norm‘𝑡)‘(𝑓‘𝑥)) |
| 17 | | vr |
. . . . . . . . . 10
setvar 𝑟 |
| 18 | 17 | cv 1539 |
. . . . . . . . 9
class 𝑟 |
| 19 | 6, 14 | cfv 6561 |
. . . . . . . . . 10
class
(norm‘𝑠) |
| 20 | 11, 19 | cfv 6561 |
. . . . . . . . 9
class
((norm‘𝑠)‘𝑥) |
| 21 | | cmul 11160 |
. . . . . . . . 9
class
· |
| 22 | 18, 20, 21 | co 7431 |
. . . . . . . 8
class (𝑟 · ((norm‘𝑠)‘𝑥)) |
| 23 | | cle 11296 |
. . . . . . . 8
class
≤ |
| 24 | 16, 22, 23 | wbr 5143 |
. . . . . . 7
wff
((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥)) |
| 25 | | cbs 17247 |
. . . . . . . 8
class
Base |
| 26 | 6, 25 | cfv 6561 |
. . . . . . 7
class
(Base‘𝑠) |
| 27 | 24, 10, 26 | wral 3061 |
. . . . . 6
wff
∀𝑥 ∈
(Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥)) |
| 28 | | cc0 11155 |
. . . . . . 7
class
0 |
| 29 | | cpnf 11292 |
. . . . . . 7
class
+∞ |
| 30 | | cico 13389 |
. . . . . . 7
class
[,) |
| 31 | 28, 29, 30 | co 7431 |
. . . . . 6
class
(0[,)+∞) |
| 32 | 27, 17, 31 | crab 3436 |
. . . . 5
class {𝑟 ∈ (0[,)+∞) ∣
∀𝑥 ∈
(Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))} |
| 33 | | cxr 11294 |
. . . . 5
class
ℝ* |
| 34 | | clt 11295 |
. . . . 5
class
< |
| 35 | 32, 33, 34 | cinf 9481 |
. . . 4
class
inf({𝑟 ∈
(0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, <
) |
| 36 | 5, 9, 35 | cmpt 5225 |
. . 3
class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, <
)) |
| 37 | 2, 3, 4, 4, 36 | cmpo 7433 |
. 2
class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, <
))) |
| 38 | 1, 37 | wceq 1540 |
1
wff normOp =
(𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, <
))) |