Step |
Hyp |
Ref |
Expression |
0 |
|
cnmo |
⊢ normOp |
1 |
|
vs |
⊢ 𝑠 |
2 |
|
cngp |
⊢ NrmGrp |
3 |
|
vt |
⊢ 𝑡 |
4 |
|
vf |
⊢ 𝑓 |
5 |
1
|
cv |
⊢ 𝑠 |
6 |
|
cghm |
⊢ GrpHom |
7 |
3
|
cv |
⊢ 𝑡 |
8 |
5 7 6
|
co |
⊢ ( 𝑠 GrpHom 𝑡 ) |
9 |
|
vr |
⊢ 𝑟 |
10 |
|
cc0 |
⊢ 0 |
11 |
|
cico |
⊢ [,) |
12 |
|
cpnf |
⊢ +∞ |
13 |
10 12 11
|
co |
⊢ ( 0 [,) +∞ ) |
14 |
|
vx |
⊢ 𝑥 |
15 |
|
cbs |
⊢ Base |
16 |
5 15
|
cfv |
⊢ ( Base ‘ 𝑠 ) |
17 |
|
cnm |
⊢ norm |
18 |
7 17
|
cfv |
⊢ ( norm ‘ 𝑡 ) |
19 |
4
|
cv |
⊢ 𝑓 |
20 |
14
|
cv |
⊢ 𝑥 |
21 |
20 19
|
cfv |
⊢ ( 𝑓 ‘ 𝑥 ) |
22 |
21 18
|
cfv |
⊢ ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) |
23 |
|
cle |
⊢ ≤ |
24 |
9
|
cv |
⊢ 𝑟 |
25 |
|
cmul |
⊢ · |
26 |
5 17
|
cfv |
⊢ ( norm ‘ 𝑠 ) |
27 |
20 26
|
cfv |
⊢ ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) |
28 |
24 27 25
|
co |
⊢ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) |
29 |
22 28 23
|
wbr |
⊢ ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) |
30 |
29 14 16
|
wral |
⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) |
31 |
30 9 13
|
crab |
⊢ { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } |
32 |
|
cxr |
⊢ ℝ* |
33 |
|
clt |
⊢ < |
34 |
31 32 33
|
cinf |
⊢ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) |
35 |
4 8 34
|
cmpt |
⊢ ( 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) ) |
36 |
1 3 2 2 35
|
cmpo |
⊢ ( 𝑠 ∈ NrmGrp , 𝑡 ∈ NrmGrp ↦ ( 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) ) ) |
37 |
0 36
|
wceq |
⊢ normOp = ( 𝑠 ∈ NrmGrp , 𝑡 ∈ NrmGrp ↦ ( 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) ) ) |