Step | Hyp | Ref
| Expression |
1 | | nmofval.1 |
. 2
β’ π = (π normOp π) |
2 | | oveq12 7371 |
. . . 4
β’ ((π = π β§ π‘ = π) β (π GrpHom π‘) = (π GrpHom π)) |
3 | | simpl 484 |
. . . . . . . . 9
β’ ((π = π β§ π‘ = π) β π = π) |
4 | 3 | fveq2d 6851 |
. . . . . . . 8
β’ ((π = π β§ π‘ = π) β (Baseβπ ) = (Baseβπ)) |
5 | | nmofval.2 |
. . . . . . . 8
β’ π = (Baseβπ) |
6 | 4, 5 | eqtr4di 2795 |
. . . . . . 7
β’ ((π = π β§ π‘ = π) β (Baseβπ ) = π) |
7 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π = π β§ π‘ = π) β π‘ = π) |
8 | 7 | fveq2d 6851 |
. . . . . . . . . 10
β’ ((π = π β§ π‘ = π) β (normβπ‘) = (normβπ)) |
9 | | nmofval.4 |
. . . . . . . . . 10
β’ π = (normβπ) |
10 | 8, 9 | eqtr4di 2795 |
. . . . . . . . 9
β’ ((π = π β§ π‘ = π) β (normβπ‘) = π) |
11 | 10 | fveq1d 6849 |
. . . . . . . 8
β’ ((π = π β§ π‘ = π) β ((normβπ‘)β(πβπ₯)) = (πβ(πβπ₯))) |
12 | 3 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((π = π β§ π‘ = π) β (normβπ ) = (normβπ)) |
13 | | nmofval.3 |
. . . . . . . . . . 11
β’ πΏ = (normβπ) |
14 | 12, 13 | eqtr4di 2795 |
. . . . . . . . . 10
β’ ((π = π β§ π‘ = π) β (normβπ ) = πΏ) |
15 | 14 | fveq1d 6849 |
. . . . . . . . 9
β’ ((π = π β§ π‘ = π) β ((normβπ )βπ₯) = (πΏβπ₯)) |
16 | 15 | oveq2d 7378 |
. . . . . . . 8
β’ ((π = π β§ π‘ = π) β (π Β· ((normβπ )βπ₯)) = (π Β· (πΏβπ₯))) |
17 | 11, 16 | breq12d 5123 |
. . . . . . 7
β’ ((π = π β§ π‘ = π) β (((normβπ‘)β(πβπ₯)) β€ (π Β· ((normβπ )βπ₯)) β (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯)))) |
18 | 6, 17 | raleqbidv 3322 |
. . . . . 6
β’ ((π = π β§ π‘ = π) β (βπ₯ β (Baseβπ )((normβπ‘)β(πβπ₯)) β€ (π Β· ((normβπ )βπ₯)) β βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯)))) |
19 | 18 | rabbidv 3418 |
. . . . 5
β’ ((π = π β§ π‘ = π) β {π β (0[,)+β) β£ βπ₯ β (Baseβπ )((normβπ‘)β(πβπ₯)) β€ (π Β· ((normβπ )βπ₯))} = {π β (0[,)+β) β£ βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))}) |
20 | 19 | infeq1d 9420 |
. . . 4
β’ ((π = π β§ π‘ = π) β inf({π β (0[,)+β) β£ βπ₯ β (Baseβπ )((normβπ‘)β(πβπ₯)) β€ (π Β· ((normβπ )βπ₯))}, β*, < ) = inf({π β (0[,)+β) β£
βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, <
)) |
21 | 2, 20 | mpteq12dv 5201 |
. . 3
β’ ((π = π β§ π‘ = π) β (π β (π GrpHom π‘) β¦ inf({π β (0[,)+β) β£ βπ₯ β (Baseβπ )((normβπ‘)β(πβπ₯)) β€ (π Β· ((normβπ )βπ₯))}, β*, < )) = (π β (π GrpHom π) β¦ inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, <
))) |
22 | | df-nmo 24088 |
. . 3
β’ normOp =
(π β NrmGrp, π‘ β NrmGrp β¦ (π β (π GrpHom π‘) β¦ inf({π β (0[,)+β) β£ βπ₯ β (Baseβπ )((normβπ‘)β(πβπ₯)) β€ (π Β· ((normβπ )βπ₯))}, β*, <
))) |
23 | | eqid 2737 |
. . . . 5
β’ (π β (π GrpHom π) β¦ inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, < )) = (π β (π GrpHom π) β¦ inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, <
)) |
24 | | ssrab2 4042 |
. . . . . . 7
β’ {π β (0[,)+β) β£
βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))} β (0[,)+β) |
25 | | icossxr 13356 |
. . . . . . 7
β’
(0[,)+β) β β* |
26 | 24, 25 | sstri 3958 |
. . . . . 6
β’ {π β (0[,)+β) β£
βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))} β
β* |
27 | | infxrcl 13259 |
. . . . . 6
β’ ({π β (0[,)+β) β£
βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))} β β* β
inf({π β
(0[,)+β) β£ βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, < ) β
β*) |
28 | 26, 27 | mp1i 13 |
. . . . 5
β’ (π β (π GrpHom π) β inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, < ) β
β*) |
29 | 23, 28 | fmpti 7065 |
. . . 4
β’ (π β (π GrpHom π) β¦ inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, < )):(π GrpHom π)βΆβ* |
30 | | ovex 7395 |
. . . 4
β’ (π GrpHom π) β V |
31 | | xrex 12919 |
. . . 4
β’
β* β V |
32 | | fex2 7875 |
. . . 4
β’ (((π β (π GrpHom π) β¦ inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, < )):(π GrpHom π)βΆβ* β§ (π GrpHom π) β V β§ β* β
V) β (π β (π GrpHom π) β¦ inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, < )) β
V) |
33 | 29, 30, 31, 32 | mp3an 1462 |
. . 3
β’ (π β (π GrpHom π) β¦ inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, < )) β
V |
34 | 21, 22, 33 | ovmpoa 7515 |
. 2
β’ ((π β NrmGrp β§ π β NrmGrp) β (π normOp π) = (π β (π GrpHom π) β¦ inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, <
))) |
35 | 1, 34 | eqtrid 2789 |
1
β’ ((π β NrmGrp β§ π β NrmGrp) β π = (π β (π GrpHom π) β¦ inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, <
))) |