Step | Hyp | Ref
| Expression |
1 | | elrege0 13380 |
. . 3
β’ (π΄ β (0[,)+β) β
(π΄ β β β§ 0
β€ π΄)) |
2 | | nmofval.1 |
. . . . . . . 8
β’ π = (π normOp π) |
3 | | nmofval.2 |
. . . . . . . 8
β’ π = (Baseβπ) |
4 | | nmofval.3 |
. . . . . . . 8
β’ πΏ = (normβπ) |
5 | | nmofval.4 |
. . . . . . . 8
β’ π = (normβπ) |
6 | 2, 3, 4, 5 | nmoval 24102 |
. . . . . . 7
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β (πβπΉ) = inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, <
)) |
7 | | ssrab2 4041 |
. . . . . . . . 9
β’ {π β (0[,)+β) β£
βπ₯ β π (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯))} β (0[,)+β) |
8 | | icossxr 13358 |
. . . . . . . . 9
β’
(0[,)+β) β β* |
9 | 7, 8 | sstri 3957 |
. . . . . . . 8
β’ {π β (0[,)+β) β£
βπ₯ β π (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯))} β
β* |
10 | | infxrcl 13261 |
. . . . . . . 8
β’ ({π β (0[,)+β) β£
βπ₯ β π (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯))} β β* β
inf({π β
(0[,)+β) β£ βπ₯ β π (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, < ) β
β*) |
11 | 9, 10 | mp1i 13 |
. . . . . . 7
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, < ) β
β*) |
12 | 6, 11 | eqeltrd 2834 |
. . . . . 6
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β (πβπΉ) β
β*) |
13 | 12 | xrleidd 13080 |
. . . . 5
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β (πβπΉ) β€ (πβπΉ)) |
14 | 2, 3, 4, 5 | nmogelb 24103 |
. . . . . 6
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) β β*) β ((πβπΉ) β€ (πβπΉ) β βπ β (0[,)+β)(βπ₯ β π (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯)) β (πβπΉ) β€ π))) |
15 | 12, 14 | mpdan 686 |
. . . . 5
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β ((πβπΉ) β€ (πβπΉ) β βπ β (0[,)+β)(βπ₯ β π (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯)) β (πβπΉ) β€ π))) |
16 | 13, 15 | mpbid 231 |
. . . 4
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β βπ β (0[,)+β)(βπ₯ β π (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯)) β (πβπΉ) β€ π)) |
17 | | oveq1 7368 |
. . . . . . . 8
β’ (π = π΄ β (π Β· (πΏβπ₯)) = (π΄ Β· (πΏβπ₯))) |
18 | 17 | breq2d 5121 |
. . . . . . 7
β’ (π = π΄ β ((πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯)) β (πβ(πΉβπ₯)) β€ (π΄ Β· (πΏβπ₯)))) |
19 | 18 | ralbidv 3171 |
. . . . . 6
β’ (π = π΄ β (βπ₯ β π (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯)) β βπ₯ β π (πβ(πΉβπ₯)) β€ (π΄ Β· (πΏβπ₯)))) |
20 | | breq2 5113 |
. . . . . 6
β’ (π = π΄ β ((πβπΉ) β€ π β (πβπΉ) β€ π΄)) |
21 | 19, 20 | imbi12d 345 |
. . . . 5
β’ (π = π΄ β ((βπ₯ β π (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯)) β (πβπΉ) β€ π) β (βπ₯ β π (πβ(πΉβπ₯)) β€ (π΄ Β· (πΏβπ₯)) β (πβπΉ) β€ π΄))) |
22 | 21 | rspccv 3580 |
. . . 4
β’
(βπ β
(0[,)+β)(βπ₯
β π (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯)) β (πβπΉ) β€ π) β (π΄ β (0[,)+β) β (βπ₯ β π (πβ(πΉβπ₯)) β€ (π΄ Β· (πΏβπ₯)) β (πβπΉ) β€ π΄))) |
23 | 16, 22 | syl 17 |
. . 3
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β (π΄ β (0[,)+β) β (βπ₯ β π (πβ(πΉβπ₯)) β€ (π΄ Β· (πΏβπ₯)) β (πβπΉ) β€ π΄))) |
24 | 1, 23 | biimtrrid 242 |
. 2
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β ((π΄ β β β§ 0 β€ π΄) β (βπ₯ β π (πβ(πΉβπ₯)) β€ (π΄ Β· (πΏβπ₯)) β (πβπΉ) β€ π΄))) |
25 | 24 | 3impib 1117 |
1
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π΄ β β β§ 0 β€ π΄) β (βπ₯ β π (πβ(πΉβπ₯)) β€ (π΄ Β· (πΏβπ₯)) β (πβπΉ) β€ π΄)) |