Step |
Hyp |
Ref |
Expression |
0 |
|
cnmo |
|- normOp |
1 |
|
vs |
|- s |
2 |
|
cngp |
|- NrmGrp |
3 |
|
vt |
|- t |
4 |
|
vf |
|- f |
5 |
1
|
cv |
|- s |
6 |
|
cghm |
|- GrpHom |
7 |
3
|
cv |
|- t |
8 |
5 7 6
|
co |
|- ( s GrpHom t ) |
9 |
|
vr |
|- r |
10 |
|
cc0 |
|- 0 |
11 |
|
cico |
|- [,) |
12 |
|
cpnf |
|- +oo |
13 |
10 12 11
|
co |
|- ( 0 [,) +oo ) |
14 |
|
vx |
|- x |
15 |
|
cbs |
|- Base |
16 |
5 15
|
cfv |
|- ( Base ` s ) |
17 |
|
cnm |
|- norm |
18 |
7 17
|
cfv |
|- ( norm ` t ) |
19 |
4
|
cv |
|- f |
20 |
14
|
cv |
|- x |
21 |
20 19
|
cfv |
|- ( f ` x ) |
22 |
21 18
|
cfv |
|- ( ( norm ` t ) ` ( f ` x ) ) |
23 |
|
cle |
|- <_ |
24 |
9
|
cv |
|- r |
25 |
|
cmul |
|- x. |
26 |
5 17
|
cfv |
|- ( norm ` s ) |
27 |
20 26
|
cfv |
|- ( ( norm ` s ) ` x ) |
28 |
24 27 25
|
co |
|- ( r x. ( ( norm ` s ) ` x ) ) |
29 |
22 28 23
|
wbr |
|- ( ( norm ` t ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` s ) ` x ) ) |
30 |
29 14 16
|
wral |
|- A. x e. ( Base ` s ) ( ( norm ` t ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` s ) ` x ) ) |
31 |
30 9 13
|
crab |
|- { r e. ( 0 [,) +oo ) | A. x e. ( Base ` s ) ( ( norm ` t ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` s ) ` x ) ) } |
32 |
|
cxr |
|- RR* |
33 |
|
clt |
|- < |
34 |
31 32 33
|
cinf |
|- inf ( { r e. ( 0 [,) +oo ) | A. x e. ( Base ` s ) ( ( norm ` t ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` s ) ` x ) ) } , RR* , < ) |
35 |
4 8 34
|
cmpt |
|- ( f e. ( s GrpHom t ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. ( Base ` s ) ( ( norm ` t ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` s ) ` x ) ) } , RR* , < ) ) |
36 |
1 3 2 2 35
|
cmpo |
|- ( s e. NrmGrp , t e. NrmGrp |-> ( f e. ( s GrpHom t ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. ( Base ` s ) ( ( norm ` t ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` s ) ` x ) ) } , RR* , < ) ) ) |
37 |
0 36
|
wceq |
|- normOp = ( s e. NrmGrp , t e. NrmGrp |-> ( f e. ( s GrpHom t ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. ( Base ` s ) ( ( norm ` t ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` s ) ` x ) ) } , RR* , < ) ) ) |