Step | Hyp | Ref
| Expression |
1 | | nmofval.1 |
. . . . 5
β’ π = (π normOp π) |
2 | | nmofval.2 |
. . . . 5
β’ π = (Baseβπ) |
3 | | nmofval.3 |
. . . . 5
β’ πΏ = (normβπ) |
4 | | nmofval.4 |
. . . . 5
β’ π = (normβπ) |
5 | 1, 2, 3, 4 | nmofval 24094 |
. . . 4
β’ ((π β NrmGrp β§ π β NrmGrp) β π = (π β (π GrpHom π) β¦ inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, <
))) |
6 | 5 | fveq1d 6849 |
. . 3
β’ ((π β NrmGrp β§ π β NrmGrp) β (πβπΉ) = ((π β (π GrpHom π) β¦ inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, < ))βπΉ)) |
7 | | fveq1 6846 |
. . . . . . . . 9
β’ (π = πΉ β (πβπ₯) = (πΉβπ₯)) |
8 | 7 | fveq2d 6851 |
. . . . . . . 8
β’ (π = πΉ β (πβ(πβπ₯)) = (πβ(πΉβπ₯))) |
9 | 8 | breq1d 5120 |
. . . . . . 7
β’ (π = πΉ β ((πβ(πβπ₯)) β€ (π Β· (πΏβπ₯)) β (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯)))) |
10 | 9 | ralbidv 3175 |
. . . . . 6
β’ (π = πΉ β (βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯)) β βπ₯ β π (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯)))) |
11 | 10 | rabbidv 3418 |
. . . . 5
β’ (π = πΉ β {π β (0[,)+β) β£ βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))} = {π β (0[,)+β) β£ βπ₯ β π (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯))}) |
12 | 11 | infeq1d 9420 |
. . . 4
β’ (π = πΉ β inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, < ) = inf({π β (0[,)+β) β£
βπ₯ β π (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, <
)) |
13 | | eqid 2737 |
. . . 4
β’ (π β (π GrpHom π) β¦ inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, < )) = (π β (π GrpHom π) β¦ inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, <
)) |
14 | | xrltso 13067 |
. . . . 5
β’ < Or
β* |
15 | 14 | infex 9436 |
. . . 4
β’
inf({π β
(0[,)+β) β£ βπ₯ β π (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, < ) β
V |
16 | 12, 13, 15 | fvmpt 6953 |
. . 3
β’ (πΉ β (π GrpHom π) β ((π β (π GrpHom π) β¦ inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, < ))βπΉ) = inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, <
)) |
17 | 6, 16 | sylan9eq 2797 |
. 2
β’ (((π β NrmGrp β§ π β NrmGrp) β§ πΉ β (π GrpHom π)) β (πβπΉ) = inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, <
)) |
18 | 17 | 3impa 1111 |
1
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β (πβπΉ) = inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, <
)) |