Step | Hyp | Ref
| Expression |
1 | | cnvimass 6038 |
. . . 4
β’ (β‘π β β) β dom π |
2 | | eqid 2737 |
. . . . . 6
β’
(BaseβπΊ) =
(BaseβπΊ) |
3 | | torsubg.1 |
. . . . . 6
β’ π = (odβπΊ) |
4 | 2, 3 | odf 19326 |
. . . . 5
β’ π:(BaseβπΊ)βΆβ0 |
5 | 4 | fdmi 6685 |
. . . 4
β’ dom π = (BaseβπΊ) |
6 | 1, 5 | sseqtri 3985 |
. . 3
β’ (β‘π β β) β (BaseβπΊ) |
7 | 6 | a1i 11 |
. 2
β’ (πΊ β Abel β (β‘π β β) β (BaseβπΊ)) |
8 | | ablgrp 19574 |
. . . . 5
β’ (πΊ β Abel β πΊ β Grp) |
9 | | eqid 2737 |
. . . . . 6
β’
(0gβπΊ) = (0gβπΊ) |
10 | 2, 9 | grpidcl 18785 |
. . . . 5
β’ (πΊ β Grp β
(0gβπΊ)
β (BaseβπΊ)) |
11 | 8, 10 | syl 17 |
. . . 4
β’ (πΊ β Abel β
(0gβπΊ)
β (BaseβπΊ)) |
12 | 3, 9 | od1 19348 |
. . . . . 6
β’ (πΊ β Grp β (πβ(0gβπΊ)) = 1) |
13 | 8, 12 | syl 17 |
. . . . 5
β’ (πΊ β Abel β (πβ(0gβπΊ)) = 1) |
14 | | 1nn 12171 |
. . . . 5
β’ 1 β
β |
15 | 13, 14 | eqeltrdi 2846 |
. . . 4
β’ (πΊ β Abel β (πβ(0gβπΊ)) β
β) |
16 | | ffn 6673 |
. . . . . 6
β’ (π:(BaseβπΊ)βΆβ0 β π Fn (BaseβπΊ)) |
17 | 4, 16 | ax-mp 5 |
. . . . 5
β’ π Fn (BaseβπΊ) |
18 | | elpreima 7013 |
. . . . 5
β’ (π Fn (BaseβπΊ) β
((0gβπΊ)
β (β‘π β β) β
((0gβπΊ)
β (BaseβπΊ) β§
(πβ(0gβπΊ)) β
β))) |
19 | 17, 18 | ax-mp 5 |
. . . 4
β’
((0gβπΊ) β (β‘π β β) β
((0gβπΊ)
β (BaseβπΊ) β§
(πβ(0gβπΊ)) β
β)) |
20 | 11, 15, 19 | sylanbrc 584 |
. . 3
β’ (πΊ β Abel β
(0gβπΊ)
β (β‘π β β)) |
21 | 20 | ne0d 4300 |
. 2
β’ (πΊ β Abel β (β‘π β β) β
β
) |
22 | 8 | ad2antrr 725 |
. . . . . . 7
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β πΊ β Grp) |
23 | 6 | sseli 3945 |
. . . . . . . 8
β’ (π₯ β (β‘π β β) β π₯ β (BaseβπΊ)) |
24 | 23 | ad2antlr 726 |
. . . . . . 7
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β π₯ β (BaseβπΊ)) |
25 | 6 | sseli 3945 |
. . . . . . . 8
β’ (π¦ β (β‘π β β) β π¦ β (BaseβπΊ)) |
26 | 25 | adantl 483 |
. . . . . . 7
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β π¦ β (BaseβπΊ)) |
27 | | eqid 2737 |
. . . . . . . 8
β’
(+gβπΊ) = (+gβπΊ) |
28 | 2, 27 | grpcl 18763 |
. . . . . . 7
β’ ((πΊ β Grp β§ π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ)) β (π₯(+gβπΊ)π¦) β (BaseβπΊ)) |
29 | 22, 24, 26, 28 | syl3anc 1372 |
. . . . . 6
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β (π₯(+gβπΊ)π¦) β (BaseβπΊ)) |
30 | | 0nnn 12196 |
. . . . . . . . 9
β’ Β¬ 0
β β |
31 | 2, 3 | odcl 19325 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (BaseβπΊ) β (πβπ₯) β
β0) |
32 | 24, 31 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β (πβπ₯) β
β0) |
33 | 32 | nn0zd 12532 |
. . . . . . . . . . . . . . 15
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β (πβπ₯) β β€) |
34 | 2, 3 | odcl 19325 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β (BaseβπΊ) β (πβπ¦) β
β0) |
35 | 26, 34 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β (πβπ¦) β
β0) |
36 | 35 | nn0zd 12532 |
. . . . . . . . . . . . . . 15
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β (πβπ¦) β β€) |
37 | 33, 36 | gcdcld 16395 |
. . . . . . . . . . . . . 14
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β ((πβπ₯) gcd (πβπ¦)) β
β0) |
38 | 37 | nn0cnd 12482 |
. . . . . . . . . . . . 13
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β ((πβπ₯) gcd (πβπ¦)) β β) |
39 | 38 | mul02d 11360 |
. . . . . . . . . . . 12
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β (0 Β·
((πβπ₯) gcd (πβπ¦))) = 0) |
40 | 39 | breq1d 5120 |
. . . . . . . . . . 11
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β ((0 Β·
((πβπ₯) gcd (πβπ¦))) β₯ ((πβπ₯) Β· (πβπ¦)) β 0 β₯ ((πβπ₯) Β· (πβπ¦)))) |
41 | 33, 36 | zmulcld 12620 |
. . . . . . . . . . . 12
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β ((πβπ₯) Β· (πβπ¦)) β β€) |
42 | | 0dvds 16166 |
. . . . . . . . . . . 12
β’ (((πβπ₯) Β· (πβπ¦)) β β€ β (0 β₯ ((πβπ₯) Β· (πβπ¦)) β ((πβπ₯) Β· (πβπ¦)) = 0)) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . 11
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β (0 β₯ ((πβπ₯) Β· (πβπ¦)) β ((πβπ₯) Β· (πβπ¦)) = 0)) |
44 | 40, 43 | bitrd 279 |
. . . . . . . . . 10
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β ((0 Β·
((πβπ₯) gcd (πβπ¦))) β₯ ((πβπ₯) Β· (πβπ¦)) β ((πβπ₯) Β· (πβπ¦)) = 0)) |
45 | | elpreima 7013 |
. . . . . . . . . . . . . . 15
β’ (π Fn (BaseβπΊ) β (π₯ β (β‘π β β) β (π₯ β (BaseβπΊ) β§ (πβπ₯) β β))) |
46 | 17, 45 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ (π₯ β (β‘π β β) β (π₯ β (BaseβπΊ) β§ (πβπ₯) β β)) |
47 | 46 | simprbi 498 |
. . . . . . . . . . . . 13
β’ (π₯ β (β‘π β β) β (πβπ₯) β β) |
48 | 47 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β (πβπ₯) β β) |
49 | | elpreima 7013 |
. . . . . . . . . . . . . . 15
β’ (π Fn (BaseβπΊ) β (π¦ β (β‘π β β) β (π¦ β (BaseβπΊ) β§ (πβπ¦) β β))) |
50 | 17, 49 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ (π¦ β (β‘π β β) β (π¦ β (BaseβπΊ) β§ (πβπ¦) β β)) |
51 | 50 | simprbi 498 |
. . . . . . . . . . . . 13
β’ (π¦ β (β‘π β β) β (πβπ¦) β β) |
52 | 51 | adantl 483 |
. . . . . . . . . . . 12
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β (πβπ¦) β β) |
53 | 48, 52 | nnmulcld 12213 |
. . . . . . . . . . 11
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β ((πβπ₯) Β· (πβπ¦)) β β) |
54 | | eleq1 2826 |
. . . . . . . . . . 11
β’ (((πβπ₯) Β· (πβπ¦)) = 0 β (((πβπ₯) Β· (πβπ¦)) β β β 0 β
β)) |
55 | 53, 54 | syl5ibcom 244 |
. . . . . . . . . 10
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β (((πβπ₯) Β· (πβπ¦)) = 0 β 0 β
β)) |
56 | 44, 55 | sylbid 239 |
. . . . . . . . 9
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β ((0 Β·
((πβπ₯) gcd (πβπ¦))) β₯ ((πβπ₯) Β· (πβπ¦)) β 0 β β)) |
57 | 30, 56 | mtoi 198 |
. . . . . . . 8
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β Β¬ (0 Β·
((πβπ₯) gcd (πβπ¦))) β₯ ((πβπ₯) Β· (πβπ¦))) |
58 | | simpll 766 |
. . . . . . . . . 10
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β πΊ β Abel) |
59 | 3, 2, 27 | odadd1 19633 |
. . . . . . . . . 10
β’ ((πΊ β Abel β§ π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ)) β ((πβ(π₯(+gβπΊ)π¦)) Β· ((πβπ₯) gcd (πβπ¦))) β₯ ((πβπ₯) Β· (πβπ¦))) |
60 | 58, 24, 26, 59 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β ((πβ(π₯(+gβπΊ)π¦)) Β· ((πβπ₯) gcd (πβπ¦))) β₯ ((πβπ₯) Β· (πβπ¦))) |
61 | | oveq1 7369 |
. . . . . . . . . 10
β’ ((πβ(π₯(+gβπΊ)π¦)) = 0 β ((πβ(π₯(+gβπΊ)π¦)) Β· ((πβπ₯) gcd (πβπ¦))) = (0 Β· ((πβπ₯) gcd (πβπ¦)))) |
62 | 61 | breq1d 5120 |
. . . . . . . . 9
β’ ((πβ(π₯(+gβπΊ)π¦)) = 0 β (((πβ(π₯(+gβπΊ)π¦)) Β· ((πβπ₯) gcd (πβπ¦))) β₯ ((πβπ₯) Β· (πβπ¦)) β (0 Β· ((πβπ₯) gcd (πβπ¦))) β₯ ((πβπ₯) Β· (πβπ¦)))) |
63 | 60, 62 | syl5ibcom 244 |
. . . . . . . 8
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β ((πβ(π₯(+gβπΊ)π¦)) = 0 β (0 Β· ((πβπ₯) gcd (πβπ¦))) β₯ ((πβπ₯) Β· (πβπ¦)))) |
64 | 57, 63 | mtod 197 |
. . . . . . 7
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β Β¬ (πβ(π₯(+gβπΊ)π¦)) = 0) |
65 | 2, 3 | odcl 19325 |
. . . . . . . . . 10
β’ ((π₯(+gβπΊ)π¦) β (BaseβπΊ) β (πβ(π₯(+gβπΊ)π¦)) β
β0) |
66 | 29, 65 | syl 17 |
. . . . . . . . 9
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β (πβ(π₯(+gβπΊ)π¦)) β
β0) |
67 | | elnn0 12422 |
. . . . . . . . 9
β’ ((πβ(π₯(+gβπΊ)π¦)) β β0 β ((πβ(π₯(+gβπΊ)π¦)) β β β¨ (πβ(π₯(+gβπΊ)π¦)) = 0)) |
68 | 66, 67 | sylib 217 |
. . . . . . . 8
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β ((πβ(π₯(+gβπΊ)π¦)) β β β¨ (πβ(π₯(+gβπΊ)π¦)) = 0)) |
69 | 68 | ord 863 |
. . . . . . 7
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β (Β¬ (πβ(π₯(+gβπΊ)π¦)) β β β (πβ(π₯(+gβπΊ)π¦)) = 0)) |
70 | 64, 69 | mt3d 148 |
. . . . . 6
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β (πβ(π₯(+gβπΊ)π¦)) β β) |
71 | | elpreima 7013 |
. . . . . . 7
β’ (π Fn (BaseβπΊ) β ((π₯(+gβπΊ)π¦) β (β‘π β β) β ((π₯(+gβπΊ)π¦) β (BaseβπΊ) β§ (πβ(π₯(+gβπΊ)π¦)) β β))) |
72 | 17, 71 | ax-mp 5 |
. . . . . 6
β’ ((π₯(+gβπΊ)π¦) β (β‘π β β) β ((π₯(+gβπΊ)π¦) β (BaseβπΊ) β§ (πβ(π₯(+gβπΊ)π¦)) β β)) |
73 | 29, 70, 72 | sylanbrc 584 |
. . . . 5
β’ (((πΊ β Abel β§ π₯ β (β‘π β β)) β§ π¦ β (β‘π β β)) β (π₯(+gβπΊ)π¦) β (β‘π β β)) |
74 | 73 | ralrimiva 3144 |
. . . 4
β’ ((πΊ β Abel β§ π₯ β (β‘π β β)) β βπ¦ β (β‘π β β)(π₯(+gβπΊ)π¦) β (β‘π β β)) |
75 | | eqid 2737 |
. . . . . . 7
β’
(invgβπΊ) = (invgβπΊ) |
76 | 2, 75 | grpinvcl 18805 |
. . . . . 6
β’ ((πΊ β Grp β§ π₯ β (BaseβπΊ)) β
((invgβπΊ)βπ₯) β (BaseβπΊ)) |
77 | 8, 23, 76 | syl2an 597 |
. . . . 5
β’ ((πΊ β Abel β§ π₯ β (β‘π β β)) β
((invgβπΊ)βπ₯) β (BaseβπΊ)) |
78 | 3, 75, 2 | odinv 19350 |
. . . . . . 7
β’ ((πΊ β Grp β§ π₯ β (BaseβπΊ)) β (πβ((invgβπΊ)βπ₯)) = (πβπ₯)) |
79 | 8, 23, 78 | syl2an 597 |
. . . . . 6
β’ ((πΊ β Abel β§ π₯ β (β‘π β β)) β (πβ((invgβπΊ)βπ₯)) = (πβπ₯)) |
80 | 47 | adantl 483 |
. . . . . 6
β’ ((πΊ β Abel β§ π₯ β (β‘π β β)) β (πβπ₯) β β) |
81 | 79, 80 | eqeltrd 2838 |
. . . . 5
β’ ((πΊ β Abel β§ π₯ β (β‘π β β)) β (πβ((invgβπΊ)βπ₯)) β β) |
82 | | elpreima 7013 |
. . . . . 6
β’ (π Fn (BaseβπΊ) β
(((invgβπΊ)βπ₯) β (β‘π β β) β
(((invgβπΊ)βπ₯) β (BaseβπΊ) β§ (πβ((invgβπΊ)βπ₯)) β β))) |
83 | 17, 82 | ax-mp 5 |
. . . . 5
β’
(((invgβπΊ)βπ₯) β (β‘π β β) β
(((invgβπΊ)βπ₯) β (BaseβπΊ) β§ (πβ((invgβπΊ)βπ₯)) β β)) |
84 | 77, 81, 83 | sylanbrc 584 |
. . . 4
β’ ((πΊ β Abel β§ π₯ β (β‘π β β)) β
((invgβπΊ)βπ₯) β (β‘π β β)) |
85 | 74, 84 | jca 513 |
. . 3
β’ ((πΊ β Abel β§ π₯ β (β‘π β β)) β (βπ¦ β (β‘π β β)(π₯(+gβπΊ)π¦) β (β‘π β β) β§
((invgβπΊ)βπ₯) β (β‘π β β))) |
86 | 85 | ralrimiva 3144 |
. 2
β’ (πΊ β Abel β
βπ₯ β (β‘π β β)(βπ¦ β (β‘π β β)(π₯(+gβπΊ)π¦) β (β‘π β β) β§
((invgβπΊ)βπ₯) β (β‘π β β))) |
87 | 2, 27, 75 | issubg2 18950 |
. . 3
β’ (πΊ β Grp β ((β‘π β β) β (SubGrpβπΊ) β ((β‘π β β) β (BaseβπΊ) β§ (β‘π β β) β β
β§
βπ₯ β (β‘π β β)(βπ¦ β (β‘π β β)(π₯(+gβπΊ)π¦) β (β‘π β β) β§
((invgβπΊ)βπ₯) β (β‘π β β))))) |
88 | 8, 87 | syl 17 |
. 2
β’ (πΊ β Abel β ((β‘π β β) β (SubGrpβπΊ) β ((β‘π β β) β (BaseβπΊ) β§ (β‘π β β) β β
β§
βπ₯ β (β‘π β β)(βπ¦ β (β‘π β β)(π₯(+gβπΊ)π¦) β (β‘π β β) β§
((invgβπΊ)βπ₯) β (β‘π β β))))) |
89 | 7, 21, 86, 88 | mpbir3and 1343 |
1
β’ (πΊ β Abel β (β‘π β β) β (SubGrpβπΊ)) |