Step | Hyp | Ref
| Expression |
1 | | isogrp 32215 |
. . . . 5
β’ (π β oGrp β (π β Grp β§ π β oMnd)) |
2 | 1 | simprbi 497 |
. . . 4
β’ (π β oGrp β π β oMnd) |
3 | | omndtos 32218 |
. . . 4
β’ (π β oMnd β π β Toset) |
4 | 2, 3 | syl 17 |
. . 3
β’ (π β oGrp β π β Toset) |
5 | | grpmnd 18825 |
. . . . 5
β’ (π β Grp β π β Mnd) |
6 | 5 | adantr 481 |
. . . 4
β’ ((π β Grp β§ π β oMnd) β π β Mnd) |
7 | 1, 6 | sylbi 216 |
. . 3
β’ (π β oGrp β π β Mnd) |
8 | | isarchi3.b |
. . . 4
β’ π΅ = (Baseβπ) |
9 | | isarchi3.0 |
. . . 4
β’ 0 =
(0gβπ) |
10 | | isarchi3.x |
. . . 4
β’ Β· =
(.gβπ) |
11 | | eqid 2732 |
. . . 4
β’
(leβπ) =
(leβπ) |
12 | | isarchi3.i |
. . . 4
β’ < =
(ltβπ) |
13 | 8, 9, 10, 11, 12 | isarchi2 32326 |
. . 3
β’ ((π β Toset β§ π β Mnd) β (π β Archi β
βπ₯ β π΅ βπ¦ β π΅ ( 0 < π₯ β βπ β β π¦(leβπ)(π Β· π₯)))) |
14 | 4, 7, 13 | syl2anc 584 |
. 2
β’ (π β oGrp β (π β Archi β
βπ₯ β π΅ βπ¦ β π΅ ( 0 < π₯ β βπ β β π¦(leβπ)(π Β· π₯)))) |
15 | | simpr 485 |
. . . . . . . . . . 11
β’
(((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β π β β) |
16 | 15 | adantr 481 |
. . . . . . . . . 10
β’
((((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β§ π¦(leβπ)(π Β· π₯)) β π β β) |
17 | 16 | peano2nnd 12228 |
. . . . . . . . 9
β’
((((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β§ π¦(leβπ)(π Β· π₯)) β (π + 1) β β) |
18 | | simp-4l 781 |
. . . . . . . . . . . . 13
β’
(((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β π β oGrp) |
19 | 18 | adantr 481 |
. . . . . . . . . . . 12
β’
((((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β§ π¦(leβπ)(π Β· π₯)) β π β oGrp) |
20 | | ogrpgrp 32216 |
. . . . . . . . . . . . 13
β’ (π β oGrp β π β Grp) |
21 | 8, 9 | grpidcl 18849 |
. . . . . . . . . . . . 13
β’ (π β Grp β 0 β π΅) |
22 | 19, 20, 21 | 3syl 18 |
. . . . . . . . . . . 12
β’
((((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β§ π¦(leβπ)(π Β· π₯)) β 0 β π΅) |
23 | | simp-4r 782 |
. . . . . . . . . . . . 13
β’
(((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β π₯ β π΅) |
24 | 23 | adantr 481 |
. . . . . . . . . . . 12
β’
((((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β§ π¦(leβπ)(π Β· π₯)) β π₯ β π΅) |
25 | 20 | ad4antr 730 |
. . . . . . . . . . . . . 14
β’
(((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β π β Grp) |
26 | 15 | nnzd 12584 |
. . . . . . . . . . . . . 14
β’
(((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β π β β€) |
27 | 8, 10 | mulgcl 18970 |
. . . . . . . . . . . . . 14
β’ ((π β Grp β§ π β β€ β§ π₯ β π΅) β (π Β· π₯) β π΅) |
28 | 25, 26, 23, 27 | syl3anc 1371 |
. . . . . . . . . . . . 13
β’
(((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β (π Β· π₯) β π΅) |
29 | 28 | adantr 481 |
. . . . . . . . . . . 12
β’
((((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β§ π¦(leβπ)(π Β· π₯)) β (π Β· π₯) β π΅) |
30 | | simpllr 774 |
. . . . . . . . . . . 12
β’
((((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β§ π¦(leβπ)(π Β· π₯)) β 0 < π₯) |
31 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(+gβπ) = (+gβπ) |
32 | 8, 12, 31 | ogrpaddlt 32230 |
. . . . . . . . . . . 12
β’ ((π β oGrp β§ ( 0 β π΅ β§ π₯ β π΅ β§ (π Β· π₯) β π΅) β§ 0 < π₯) β ( 0 (+gβπ)(π Β· π₯)) < (π₯(+gβπ)(π Β· π₯))) |
33 | 19, 22, 24, 29, 30, 32 | syl131anc 1383 |
. . . . . . . . . . 11
β’
((((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β§ π¦(leβπ)(π Β· π₯)) β ( 0 (+gβπ)(π Β· π₯)) < (π₯(+gβπ)(π Β· π₯))) |
34 | 19, 20 | syl 17 |
. . . . . . . . . . . 12
β’
((((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β§ π¦(leβπ)(π Β· π₯)) β π β Grp) |
35 | 8, 31, 9 | grplid 18851 |
. . . . . . . . . . . 12
β’ ((π β Grp β§ (π Β· π₯) β π΅) β ( 0 (+gβπ)(π Β· π₯)) = (π Β· π₯)) |
36 | 34, 29, 35 | syl2anc 584 |
. . . . . . . . . . 11
β’
((((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β§ π¦(leβπ)(π Β· π₯)) β ( 0 (+gβπ)(π Β· π₯)) = (π Β· π₯)) |
37 | | nncn 12219 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β) |
38 | | ax-1cn 11167 |
. . . . . . . . . . . . . . 15
β’ 1 β
β |
39 | | addcom 11399 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ 1 β
β) β (π + 1) =
(1 + π)) |
40 | 37, 38, 39 | sylancl 586 |
. . . . . . . . . . . . . 14
β’ (π β β β (π + 1) = (1 + π)) |
41 | 40 | oveq1d 7423 |
. . . . . . . . . . . . 13
β’ (π β β β ((π + 1) Β· π₯) = ((1 + π) Β· π₯)) |
42 | 16, 41 | syl 17 |
. . . . . . . . . . . 12
β’
((((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β§ π¦(leβπ)(π Β· π₯)) β ((π + 1) Β· π₯) = ((1 + π) Β· π₯)) |
43 | | grpsgrp 18845 |
. . . . . . . . . . . . . 14
β’ (π β Grp β π β Smgrp) |
44 | 19, 20, 43 | 3syl 18 |
. . . . . . . . . . . . 13
β’
((((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β§ π¦(leβπ)(π Β· π₯)) β π β Smgrp) |
45 | | 1nn 12222 |
. . . . . . . . . . . . . 14
β’ 1 β
β |
46 | 45 | a1i 11 |
. . . . . . . . . . . . 13
β’
((((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β§ π¦(leβπ)(π Β· π₯)) β 1 β β) |
47 | 8, 10, 31 | mulgnndir 18982 |
. . . . . . . . . . . . 13
β’ ((π β Smgrp β§ (1 β
β β§ π β
β β§ π₯ β
π΅)) β ((1 + π) Β· π₯) = ((1 Β· π₯)(+gβπ)(π Β· π₯))) |
48 | 44, 46, 16, 24, 47 | syl13anc 1372 |
. . . . . . . . . . . 12
β’
((((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β§ π¦(leβπ)(π Β· π₯)) β ((1 + π) Β· π₯) = ((1 Β· π₯)(+gβπ)(π Β· π₯))) |
49 | 8, 10 | mulg1 18960 |
. . . . . . . . . . . . . 14
β’ (π₯ β π΅ β (1 Β· π₯) = π₯) |
50 | 24, 49 | syl 17 |
. . . . . . . . . . . . 13
β’
((((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β§ π¦(leβπ)(π Β· π₯)) β (1 Β· π₯) = π₯) |
51 | 50 | oveq1d 7423 |
. . . . . . . . . . . 12
β’
((((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β§ π¦(leβπ)(π Β· π₯)) β ((1 Β· π₯)(+gβπ)(π Β· π₯)) = (π₯(+gβπ)(π Β· π₯))) |
52 | 42, 48, 51 | 3eqtrrd 2777 |
. . . . . . . . . . 11
β’
((((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β§ π¦(leβπ)(π Β· π₯)) β (π₯(+gβπ)(π Β· π₯)) = ((π + 1) Β· π₯)) |
53 | 33, 36, 52 | 3brtr3d 5179 |
. . . . . . . . . 10
β’
((((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β§ π¦(leβπ)(π Β· π₯)) β (π Β· π₯) < ((π + 1) Β· π₯)) |
54 | | tospos 18372 |
. . . . . . . . . . . . 13
β’ (π β Toset β π β Poset) |
55 | 18, 4, 54 | 3syl 18 |
. . . . . . . . . . . 12
β’
(((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β π β Poset) |
56 | | simpllr 774 |
. . . . . . . . . . . 12
β’
(((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β π¦ β π΅) |
57 | 26 | peano2zd 12668 |
. . . . . . . . . . . . 13
β’
(((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β (π + 1) β β€) |
58 | 8, 10 | mulgcl 18970 |
. . . . . . . . . . . . 13
β’ ((π β Grp β§ (π + 1) β β€ β§ π₯ β π΅) β ((π + 1) Β· π₯) β π΅) |
59 | 25, 57, 23, 58 | syl3anc 1371 |
. . . . . . . . . . . 12
β’
(((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β ((π + 1) Β· π₯) β π΅) |
60 | 8, 11, 12 | plelttr 18296 |
. . . . . . . . . . . 12
β’ ((π β Poset β§ (π¦ β π΅ β§ (π Β· π₯) β π΅ β§ ((π + 1) Β· π₯) β π΅)) β ((π¦(leβπ)(π Β· π₯) β§ (π Β· π₯) < ((π + 1) Β· π₯)) β π¦ < ((π + 1) Β· π₯))) |
61 | 55, 56, 28, 59, 60 | syl13anc 1372 |
. . . . . . . . . . 11
β’
(((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β ((π¦(leβπ)(π Β· π₯) β§ (π Β· π₯) < ((π + 1) Β· π₯)) β π¦ < ((π + 1) Β· π₯))) |
62 | 61 | impl 456 |
. . . . . . . . . 10
β’
(((((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β§ π¦(leβπ)(π Β· π₯)) β§ (π Β· π₯) < ((π + 1) Β· π₯)) β π¦ < ((π + 1) Β· π₯)) |
63 | 53, 62 | mpdan 685 |
. . . . . . . . 9
β’
((((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β§ π¦(leβπ)(π Β· π₯)) β π¦ < ((π + 1) Β· π₯)) |
64 | | oveq1 7415 |
. . . . . . . . . . 11
β’ (π = (π + 1) β (π Β· π₯) = ((π + 1) Β· π₯)) |
65 | 64 | breq2d 5160 |
. . . . . . . . . 10
β’ (π = (π + 1) β (π¦ < (π Β· π₯) β π¦ < ((π + 1) Β· π₯))) |
66 | 65 | rspcev 3612 |
. . . . . . . . 9
β’ (((π + 1) β β β§ π¦ < ((π + 1) Β· π₯)) β βπ β β π¦ < (π Β· π₯)) |
67 | 17, 63, 66 | syl2anc 584 |
. . . . . . . 8
β’
((((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β§ π¦(leβπ)(π Β· π₯)) β βπ β β π¦ < (π Β· π₯)) |
68 | 67 | r19.29an 3158 |
. . . . . . 7
β’
(((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ βπ β β π¦(leβπ)(π Β· π₯)) β βπ β β π¦ < (π Β· π₯)) |
69 | | oveq1 7415 |
. . . . . . . . 9
β’ (π = π β (π Β· π₯) = (π Β· π₯)) |
70 | 69 | breq2d 5160 |
. . . . . . . 8
β’ (π = π β (π¦ < (π Β· π₯) β π¦ < (π Β· π₯))) |
71 | 70 | cbvrexvw 3235 |
. . . . . . 7
β’
(βπ β
β π¦ < (π Β· π₯) β βπ β β π¦ < (π Β· π₯)) |
72 | 68, 71 | sylib 217 |
. . . . . 6
β’
(((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ βπ β β π¦(leβπ)(π Β· π₯)) β βπ β β π¦ < (π Β· π₯)) |
73 | 11, 12 | pltle 18285 |
. . . . . . . . 9
β’ ((π β oGrp β§ π¦ β π΅ β§ (π Β· π₯) β π΅) β (π¦ < (π Β· π₯) β π¦(leβπ)(π Β· π₯))) |
74 | 18, 56, 28, 73 | syl3anc 1371 |
. . . . . . . 8
β’
(((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ π β β) β (π¦ < (π Β· π₯) β π¦(leβπ)(π Β· π₯))) |
75 | 74 | reximdva 3168 |
. . . . . . 7
β’ ((((π β oGrp β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β (βπ β β π¦ < (π Β· π₯) β βπ β β π¦(leβπ)(π Β· π₯))) |
76 | 75 | imp 407 |
. . . . . 6
β’
(((((π β oGrp
β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β§ βπ β β π¦ < (π Β· π₯)) β βπ β β π¦(leβπ)(π Β· π₯)) |
77 | 72, 76 | impbida 799 |
. . . . 5
β’ ((((π β oGrp β§ π₯ β π΅) β§ π¦ β π΅) β§ 0 < π₯) β (βπ β β π¦(leβπ)(π Β· π₯) β βπ β β π¦ < (π Β· π₯))) |
78 | 77 | pm5.74da 802 |
. . . 4
β’ (((π β oGrp β§ π₯ β π΅) β§ π¦ β π΅) β (( 0 < π₯ β βπ β β π¦(leβπ)(π Β· π₯)) β ( 0 < π₯ β βπ β β π¦ < (π Β· π₯)))) |
79 | 78 | ralbidva 3175 |
. . 3
β’ ((π β oGrp β§ π₯ β π΅) β (βπ¦ β π΅ ( 0 < π₯ β βπ β β π¦(leβπ)(π Β· π₯)) β βπ¦ β π΅ ( 0 < π₯ β βπ β β π¦ < (π Β· π₯)))) |
80 | 79 | ralbidva 3175 |
. 2
β’ (π β oGrp β
(βπ₯ β π΅ βπ¦ β π΅ ( 0 < π₯ β βπ β β π¦(leβπ)(π Β· π₯)) β βπ₯ β π΅ βπ¦ β π΅ ( 0 < π₯ β βπ β β π¦ < (π Β· π₯)))) |
81 | 14, 80 | bitrd 278 |
1
β’ (π β oGrp β (π β Archi β
βπ₯ β π΅ βπ¦ β π΅ ( 0 < π₯ β βπ β β π¦ < (π Β· π₯)))) |