Step | Hyp | Ref
| Expression |
1 | | cnmo 24092 |
. 2
class
normOp |
2 | | vs |
. . 3
setvar π |
3 | | vt |
. . 3
setvar π‘ |
4 | | cngp 23956 |
. . 3
class
NrmGrp |
5 | | vf |
. . . 4
setvar π |
6 | 2 | cv 1541 |
. . . . 5
class π |
7 | 3 | cv 1541 |
. . . . 5
class π‘ |
8 | | cghm 19013 |
. . . . 5
class
GrpHom |
9 | 6, 7, 8 | co 7361 |
. . . 4
class (π GrpHom π‘) |
10 | | vx |
. . . . . . . . . . 11
setvar π₯ |
11 | 10 | cv 1541 |
. . . . . . . . . 10
class π₯ |
12 | 5 | cv 1541 |
. . . . . . . . . 10
class π |
13 | 11, 12 | cfv 6500 |
. . . . . . . . 9
class (πβπ₯) |
14 | | cnm 23955 |
. . . . . . . . . 10
class
norm |
15 | 7, 14 | cfv 6500 |
. . . . . . . . 9
class
(normβπ‘) |
16 | 13, 15 | cfv 6500 |
. . . . . . . 8
class
((normβπ‘)β(πβπ₯)) |
17 | | vr |
. . . . . . . . . 10
setvar π |
18 | 17 | cv 1541 |
. . . . . . . . 9
class π |
19 | 6, 14 | cfv 6500 |
. . . . . . . . . 10
class
(normβπ ) |
20 | 11, 19 | cfv 6500 |
. . . . . . . . 9
class
((normβπ )βπ₯) |
21 | | cmul 11064 |
. . . . . . . . 9
class
Β· |
22 | 18, 20, 21 | co 7361 |
. . . . . . . 8
class (π Β· ((normβπ )βπ₯)) |
23 | | cle 11198 |
. . . . . . . 8
class
β€ |
24 | 16, 22, 23 | wbr 5109 |
. . . . . . 7
wff
((normβπ‘)β(πβπ₯)) β€ (π Β· ((normβπ )βπ₯)) |
25 | | cbs 17091 |
. . . . . . . 8
class
Base |
26 | 6, 25 | cfv 6500 |
. . . . . . 7
class
(Baseβπ ) |
27 | 24, 10, 26 | wral 3061 |
. . . . . 6
wff
βπ₯ β
(Baseβπ )((normβπ‘)β(πβπ₯)) β€ (π Β· ((normβπ )βπ₯)) |
28 | | cc0 11059 |
. . . . . . 7
class
0 |
29 | | cpnf 11194 |
. . . . . . 7
class
+β |
30 | | cico 13275 |
. . . . . . 7
class
[,) |
31 | 28, 29, 30 | co 7361 |
. . . . . 6
class
(0[,)+β) |
32 | 27, 17, 31 | crab 3406 |
. . . . 5
class {π β (0[,)+β) β£
βπ₯ β
(Baseβπ )((normβπ‘)β(πβπ₯)) β€ (π Β· ((normβπ )βπ₯))} |
33 | | cxr 11196 |
. . . . 5
class
β* |
34 | | clt 11197 |
. . . . 5
class
< |
35 | 32, 33, 34 | cinf 9385 |
. . . 4
class
inf({π β
(0[,)+β) β£ βπ₯ β (Baseβπ )((normβπ‘)β(πβπ₯)) β€ (π Β· ((normβπ )βπ₯))}, β*, <
) |
36 | 5, 9, 35 | cmpt 5192 |
. . 3
class (π β (π GrpHom π‘) β¦ inf({π β (0[,)+β) β£ βπ₯ β (Baseβπ )((normβπ‘)β(πβπ₯)) β€ (π Β· ((normβπ )βπ₯))}, β*, <
)) |
37 | 2, 3, 4, 4, 36 | cmpo 7363 |
. 2
class (π β NrmGrp, π‘ β NrmGrp β¦ (π β (π GrpHom π‘) β¦ inf({π β (0[,)+β) β£ βπ₯ β (Baseβπ )((normβπ‘)β(πβπ₯)) β€ (π Β· ((normβπ )βπ₯))}, β*, <
))) |
38 | 1, 37 | wceq 1542 |
1
wff normOp =
(π β NrmGrp, π‘ β NrmGrp β¦ (π β (π GrpHom π‘) β¦ inf({π β (0[,)+β) β£ βπ₯ β (Baseβπ )((normβπ‘)β(πβπ₯)) β€ (π Β· ((normβπ )βπ₯))}, β*, <
))) |