Step | Hyp | Ref
| Expression |
1 | | nlmngp 24194 |
. . . . . . 7
β’ (πΊ β NrmMod β πΊ β NrmGrp) |
2 | | ngpocelbl.x |
. . . . . . . 8
β’ π = (BaseβπΊ) |
3 | | ngpocelbl.d |
. . . . . . . 8
β’ π· = ((distβπΊ) βΎ (π Γ π)) |
4 | 2, 3 | ngpmet 24112 |
. . . . . . 7
β’ (πΊ β NrmGrp β π· β (Metβπ)) |
5 | | metxmet 23840 |
. . . . . . 7
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
6 | 1, 4, 5 | 3syl 18 |
. . . . . 6
β’ (πΊ β NrmMod β π· β (βMetβπ)) |
7 | 6 | anim1i 616 |
. . . . 5
β’ ((πΊ β NrmMod β§ π
β β*)
β (π· β
(βMetβπ) β§
π
β
β*)) |
8 | 7 | 3adant3 1133 |
. . . 4
β’ ((πΊ β NrmMod β§ π
β β*
β§ (π β π β§ π΄ β π)) β (π· β (βMetβπ) β§ π
β
β*)) |
9 | | simp3l 1202 |
. . . . 5
β’ ((πΊ β NrmMod β§ π
β β*
β§ (π β π β§ π΄ β π)) β π β π) |
10 | | ngpgrp 24108 |
. . . . . . . . 9
β’ (πΊ β NrmGrp β πΊ β Grp) |
11 | 1, 10 | syl 17 |
. . . . . . . 8
β’ (πΊ β NrmMod β πΊ β Grp) |
12 | 11 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((πΊ β NrmMod β§ π
β β*
β§ (π β π β§ π΄ β π)) β πΊ β Grp) |
13 | | simp3 1139 |
. . . . . . 7
β’ ((πΊ β NrmMod β§ π
β β*
β§ (π β π β§ π΄ β π)) β (π β π β§ π΄ β π)) |
14 | | 3anass 1096 |
. . . . . . 7
β’ ((πΊ β Grp β§ π β π β§ π΄ β π) β (πΊ β Grp β§ (π β π β§ π΄ β π))) |
15 | 12, 13, 14 | sylanbrc 584 |
. . . . . 6
β’ ((πΊ β NrmMod β§ π
β β*
β§ (π β π β§ π΄ β π)) β (πΊ β Grp β§ π β π β§ π΄ β π)) |
16 | | ngpocelbl.p |
. . . . . . 7
β’ + =
(+gβπΊ) |
17 | 2, 16 | grpcl 18827 |
. . . . . 6
β’ ((πΊ β Grp β§ π β π β§ π΄ β π) β (π + π΄) β π) |
18 | 15, 17 | syl 17 |
. . . . 5
β’ ((πΊ β NrmMod β§ π
β β*
β§ (π β π β§ π΄ β π)) β (π + π΄) β π) |
19 | 9, 18 | jca 513 |
. . . 4
β’ ((πΊ β NrmMod β§ π
β β*
β§ (π β π β§ π΄ β π)) β (π β π β§ (π + π΄) β π)) |
20 | 8, 19 | jca 513 |
. . 3
β’ ((πΊ β NrmMod β§ π
β β*
β§ (π β π β§ π΄ β π)) β ((π· β (βMetβπ) β§ π
β β*) β§ (π β π β§ (π + π΄) β π))) |
21 | | elbl2 23896 |
. . 3
β’ (((π· β (βMetβπ) β§ π
β β*) β§ (π β π β§ (π + π΄) β π)) β ((π + π΄) β (π(ballβπ·)π
) β (ππ·(π + π΄)) < π
)) |
22 | 20, 21 | syl 17 |
. 2
β’ ((πΊ β NrmMod β§ π
β β*
β§ (π β π β§ π΄ β π)) β ((π + π΄) β (π(ballβπ·)π
) β (ππ·(π + π΄)) < π
)) |
23 | 3 | oveqi 7422 |
. . . . . 6
β’ (ππ·(π + π΄)) = (π((distβπΊ) βΎ (π Γ π))(π + π΄)) |
24 | | ovres 7573 |
. . . . . 6
β’ ((π β π β§ (π + π΄) β π) β (π((distβπΊ) βΎ (π Γ π))(π + π΄)) = (π(distβπΊ)(π + π΄))) |
25 | 23, 24 | eqtrid 2785 |
. . . . 5
β’ ((π β π β§ (π + π΄) β π) β (ππ·(π + π΄)) = (π(distβπΊ)(π + π΄))) |
26 | 19, 25 | syl 17 |
. . . 4
β’ ((πΊ β NrmMod β§ π
β β*
β§ (π β π β§ π΄ β π)) β (ππ·(π + π΄)) = (π(distβπΊ)(π + π΄))) |
27 | 1 | 3ad2ant1 1134 |
. . . . 5
β’ ((πΊ β NrmMod β§ π
β β*
β§ (π β π β§ π΄ β π)) β πΊ β NrmGrp) |
28 | | ngpocelbl.n |
. . . . . 6
β’ π = (normβπΊ) |
29 | | eqid 2733 |
. . . . . 6
β’
(-gβπΊ) = (-gβπΊ) |
30 | | eqid 2733 |
. . . . . 6
β’
(distβπΊ) =
(distβπΊ) |
31 | 28, 2, 29, 30 | ngpdsr 24114 |
. . . . 5
β’ ((πΊ β NrmGrp β§ π β π β§ (π + π΄) β π) β (π(distβπΊ)(π + π΄)) = (πβ((π + π΄)(-gβπΊ)π))) |
32 | 27, 9, 18, 31 | syl3anc 1372 |
. . . 4
β’ ((πΊ β NrmMod β§ π
β β*
β§ (π β π β§ π΄ β π)) β (π(distβπΊ)(π + π΄)) = (πβ((π + π΄)(-gβπΊ)π))) |
33 | | nlmlmod 24195 |
. . . . . . . . 9
β’ (πΊ β NrmMod β πΊ β LMod) |
34 | | lmodabl 20519 |
. . . . . . . . 9
β’ (πΊ β LMod β πΊ β Abel) |
35 | 33, 34 | syl 17 |
. . . . . . . 8
β’ (πΊ β NrmMod β πΊ β Abel) |
36 | 35 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((πΊ β NrmMod β§ π
β β*
β§ (π β π β§ π΄ β π)) β πΊ β Abel) |
37 | | 3anass 1096 |
. . . . . . 7
β’ ((πΊ β Abel β§ π β π β§ π΄ β π) β (πΊ β Abel β§ (π β π β§ π΄ β π))) |
38 | 36, 13, 37 | sylanbrc 584 |
. . . . . 6
β’ ((πΊ β NrmMod β§ π
β β*
β§ (π β π β§ π΄ β π)) β (πΊ β Abel β§ π β π β§ π΄ β π)) |
39 | 2, 16, 29 | ablpncan2 19683 |
. . . . . 6
β’ ((πΊ β Abel β§ π β π β§ π΄ β π) β ((π + π΄)(-gβπΊ)π) = π΄) |
40 | 38, 39 | syl 17 |
. . . . 5
β’ ((πΊ β NrmMod β§ π
β β*
β§ (π β π β§ π΄ β π)) β ((π + π΄)(-gβπΊ)π) = π΄) |
41 | 40 | fveq2d 6896 |
. . . 4
β’ ((πΊ β NrmMod β§ π
β β*
β§ (π β π β§ π΄ β π)) β (πβ((π + π΄)(-gβπΊ)π)) = (πβπ΄)) |
42 | 26, 32, 41 | 3eqtrd 2777 |
. . 3
β’ ((πΊ β NrmMod β§ π
β β*
β§ (π β π β§ π΄ β π)) β (ππ·(π + π΄)) = (πβπ΄)) |
43 | 42 | breq1d 5159 |
. 2
β’ ((πΊ β NrmMod β§ π
β β*
β§ (π β π β§ π΄ β π)) β ((ππ·(π + π΄)) < π
β (πβπ΄) < π
)) |
44 | 22, 43 | bitrd 279 |
1
β’ ((πΊ β NrmMod β§ π
β β*
β§ (π β π β§ π΄ β π)) β ((π + π΄) β (π(ballβπ·)π
) β (πβπ΄) < π
)) |