Step | Hyp | Ref
| Expression |
1 | | isogrp 29702 |
. . . . 5
oGrp oMnd |
2 | 1 | simprbi 480 |
. . . 4
oGrp oMnd |
3 | | omndtos 29705 |
. . . 4
oMnd Toset |
4 | 2, 3 | syl 17 |
. . 3
oGrp Toset |
5 | | grpmnd 17429 |
. . . . 5
|
6 | 5 | adantr 481 |
. . . 4
oMnd |
7 | 1, 6 | sylbi 207 |
. . 3
oGrp |
8 | | isarchi3.b |
. . . 4
|
9 | | isarchi3.0 |
. . . 4
|
10 | | isarchi3.x |
. . . 4
.g |
11 | | eqid 2622 |
. . . 4
|
12 | | isarchi3.i |
. . . 4
|
13 | 8, 9, 10, 11, 12 | isarchi2 29739 |
. . 3
Toset
Archi
|
14 | 4, 7, 13 | syl2anc 693 |
. 2
oGrp Archi
|
15 | | simpr 477 |
. . . . . . . . . . 11
oGrp
|
16 | 15 | adantr 481 |
. . . . . . . . . 10
oGrp
|
17 | 16 | peano2nnd 11037 |
. . . . . . . . 9
oGrp |
18 | | simp-4l 806 |
. . . . . . . . . . . . 13
oGrp
oGrp |
19 | 18 | adantr 481 |
. . . . . . . . . . . 12
oGrp
oGrp |
20 | | ogrpgrp 29703 |
. . . . . . . . . . . . 13
oGrp |
21 | 8, 9 | grpidcl 17450 |
. . . . . . . . . . . . 13
|
22 | 19, 20, 21 | 3syl 18 |
. . . . . . . . . . . 12
oGrp |
23 | | simp-4r 807 |
. . . . . . . . . . . . 13
oGrp
|
24 | 23 | adantr 481 |
. . . . . . . . . . . 12
oGrp
|
25 | 20 | ad4antr 768 |
. . . . . . . . . . . . . 14
oGrp
|
26 | 15 | nnzd 11481 |
. . . . . . . . . . . . . 14
oGrp
|
27 | 8, 10 | mulgcl 17559 |
. . . . . . . . . . . . . 14
|
28 | 25, 26, 23, 27 | syl3anc 1326 |
. . . . . . . . . . . . 13
oGrp
|
29 | 28 | adantr 481 |
. . . . . . . . . . . 12
oGrp |
30 | | simpllr 799 |
. . . . . . . . . . . 12
oGrp |
31 | | eqid 2622 |
. . . . . . . . . . . . 13
|
32 | 8, 12, 31 | ogrpaddlt 29718 |
. . . . . . . . . . . 12
oGrp
|
33 | 19, 22, 24, 29, 30, 32 | syl131anc 1339 |
. . . . . . . . . . 11
oGrp |
34 | 19, 20 | syl 17 |
. . . . . . . . . . . 12
oGrp
|
35 | 8, 31, 9 | grplid 17452 |
. . . . . . . . . . . 12
|
36 | 34, 29, 35 | syl2anc 693 |
. . . . . . . . . . 11
oGrp |
37 | | nncn 11028 |
. . . . . . . . . . . . . . 15
|
38 | | ax-1cn 9994 |
. . . . . . . . . . . . . . 15
|
39 | | addcom 10222 |
. . . . . . . . . . . . . . 15
|
40 | 37, 38, 39 | sylancl 694 |
. . . . . . . . . . . . . 14
|
41 | 40 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
42 | 16, 41 | syl 17 |
. . . . . . . . . . . 12
oGrp |
43 | | grpsgrp 17446 |
. . . . . . . . . . . . . 14
SGrp |
44 | 19, 20, 43 | 3syl 18 |
. . . . . . . . . . . . 13
oGrp
SGrp |
45 | | 1nn 11031 |
. . . . . . . . . . . . . 14
|
46 | 45 | a1i 11 |
. . . . . . . . . . . . 13
oGrp |
47 | 8, 10, 31 | mulgnndir 17569 |
. . . . . . . . . . . . 13
SGrp
|
48 | 44, 46, 16, 24, 47 | syl13anc 1328 |
. . . . . . . . . . . 12
oGrp |
49 | 8, 10 | mulg1 17548 |
. . . . . . . . . . . . . 14
|
50 | 24, 49 | syl 17 |
. . . . . . . . . . . . 13
oGrp |
51 | 50 | oveq1d 6665 |
. . . . . . . . . . . 12
oGrp |
52 | 42, 48, 51 | 3eqtrrd 2661 |
. . . . . . . . . . 11
oGrp |
53 | 33, 36, 52 | 3brtr3d 4684 |
. . . . . . . . . 10
oGrp |
54 | | tospos 29658 |
. . . . . . . . . . . . 13
Toset |
55 | 18, 4, 54 | 3syl 18 |
. . . . . . . . . . . 12
oGrp
|
56 | | simpllr 799 |
. . . . . . . . . . . 12
oGrp
|
57 | 26 | peano2zd 11485 |
. . . . . . . . . . . . 13
oGrp
|
58 | 8, 10 | mulgcl 17559 |
. . . . . . . . . . . . 13
|
59 | 25, 57, 23, 58 | syl3anc 1326 |
. . . . . . . . . . . 12
oGrp
|
60 | 8, 11, 12 | plelttr 16972 |
. . . . . . . . . . . 12
|
61 | 55, 56, 28, 59, 60 | syl13anc 1328 |
. . . . . . . . . . 11
oGrp
|
62 | 61 | impl 650 |
. . . . . . . . . 10
oGrp
|
63 | 53, 62 | mpdan 702 |
. . . . . . . . 9
oGrp |
64 | | oveq1 6657 |
. . . . . . . . . . 11
|
65 | 64 | breq2d 4665 |
. . . . . . . . . 10
|
66 | 65 | rspcev 3309 |
. . . . . . . . 9
|
67 | 17, 63, 66 | syl2anc 693 |
. . . . . . . 8
oGrp
|
68 | 67 | r19.29an 3077 |
. . . . . . 7
oGrp
|
69 | | oveq1 6657 |
. . . . . . . . 9
|
70 | 69 | breq2d 4665 |
. . . . . . . 8
|
71 | 70 | cbvrexv 3172 |
. . . . . . 7
|
72 | 68, 71 | sylib 208 |
. . . . . 6
oGrp
|
73 | 11, 12 | pltle 16961 |
. . . . . . . . 9
oGrp
|
74 | 18, 56, 28, 73 | syl3anc 1326 |
. . . . . . . 8
oGrp
|
75 | 74 | reximdva 3017 |
. . . . . . 7
oGrp
|
76 | 75 | imp 445 |
. . . . . 6
oGrp
|
77 | 72, 76 | impbida 877 |
. . . . 5
oGrp
|
78 | 77 | pm5.74da 723 |
. . . 4
oGrp
|
79 | 78 | ralbidva 2985 |
. . 3
oGrp
|
80 | 79 | ralbidva 2985 |
. 2
oGrp
|
81 | 14, 80 | bitrd 268 |
1
oGrp Archi
|