Step | Hyp | Ref
| Expression |
1 | | pgpfac1.g |
. . 3
β’ (π β πΊ β Abel) |
2 | | pgpfac1.w |
. . 3
β’ (π β π β (SubGrpβπΊ)) |
3 | | ablgrp 19574 |
. . . . . 6
β’ (πΊ β Abel β πΊ β Grp) |
4 | 1, 3 | syl 17 |
. . . . 5
β’ (π β πΊ β Grp) |
5 | | pgpfac1.b |
. . . . . 6
β’ π΅ = (BaseβπΊ) |
6 | 5 | subgacs 18970 |
. . . . 5
β’ (πΊ β Grp β
(SubGrpβπΊ) β
(ACSβπ΅)) |
7 | | acsmre 17539 |
. . . . 5
β’
((SubGrpβπΊ)
β (ACSβπ΅) β
(SubGrpβπΊ) β
(Mooreβπ΅)) |
8 | 4, 6, 7 | 3syl 18 |
. . . 4
β’ (π β (SubGrpβπΊ) β (Mooreβπ΅)) |
9 | | pgpfac1.u |
. . . . . 6
β’ (π β π β (SubGrpβπΊ)) |
10 | 5 | subgss 18936 |
. . . . . 6
β’ (π β (SubGrpβπΊ) β π β π΅) |
11 | 9, 10 | syl 17 |
. . . . 5
β’ (π β π β π΅) |
12 | | pgpfac1.d |
. . . . . 6
β’ π· = (πΆ(+gβπΊ)((π / π) Β· π΄)) |
13 | | pgpfac1.c |
. . . . . . . 8
β’ (π β πΆ β (π β (π β π))) |
14 | 13 | eldifad 3927 |
. . . . . . 7
β’ (π β πΆ β π) |
15 | | pgpfac1.s |
. . . . . . . . . . 11
β’ π = (πΎβ{π΄}) |
16 | | pgpfac1.au |
. . . . . . . . . . . . 13
β’ (π β π΄ β π) |
17 | 11, 16 | sseldd 3950 |
. . . . . . . . . . . 12
β’ (π β π΄ β π΅) |
18 | | pgpfac1.k |
. . . . . . . . . . . . 13
β’ πΎ =
(mrClsβ(SubGrpβπΊ)) |
19 | 18 | mrcsncl 17499 |
. . . . . . . . . . . 12
β’
(((SubGrpβπΊ)
β (Mooreβπ΅)
β§ π΄ β π΅) β (πΎβ{π΄}) β (SubGrpβπΊ)) |
20 | 8, 17, 19 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (πΎβ{π΄}) β (SubGrpβπΊ)) |
21 | 15, 20 | eqeltrid 2842 |
. . . . . . . . . 10
β’ (π β π β (SubGrpβπΊ)) |
22 | | pgpfac1.l |
. . . . . . . . . . 11
β’ β =
(LSSumβπΊ) |
23 | 22 | lsmub1 19446 |
. . . . . . . . . 10
β’ ((π β (SubGrpβπΊ) β§ π β (SubGrpβπΊ)) β π β (π β π)) |
24 | 21, 2, 23 | syl2anc 585 |
. . . . . . . . 9
β’ (π β π β (π β π)) |
25 | | pgpfac1.ss |
. . . . . . . . 9
β’ (π β (π β π) β π) |
26 | 24, 25 | sstrd 3959 |
. . . . . . . 8
β’ (π β π β π) |
27 | | pgpfac1.o |
. . . . . . . . . . . 12
β’ π = (odβπΊ) |
28 | | pgpfac1.e |
. . . . . . . . . . . 12
β’ πΈ = (gExβπΊ) |
29 | | pgpfac1.z |
. . . . . . . . . . . 12
β’ 0 =
(0gβπΊ) |
30 | | pgpfac1.p |
. . . . . . . . . . . 12
β’ (π β π pGrp πΊ) |
31 | | pgpfac1.n |
. . . . . . . . . . . 12
β’ (π β π΅ β Fin) |
32 | | pgpfac1.oe |
. . . . . . . . . . . 12
β’ (π β (πβπ΄) = πΈ) |
33 | | pgpfac1.i |
. . . . . . . . . . . 12
β’ (π β (π β© π) = { 0 }) |
34 | | pgpfac1.2 |
. . . . . . . . . . . 12
β’ (π β βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ (π β π) β π€)) |
35 | | pgpfac1.mg |
. . . . . . . . . . . 12
β’ Β· =
(.gβπΊ) |
36 | | pgpfac1.m |
. . . . . . . . . . . 12
β’ (π β π β β€) |
37 | | pgpfac1.mw |
. . . . . . . . . . . 12
β’ (π β ((π Β· πΆ)(+gβπΊ)(π Β· π΄)) β π) |
38 | 18, 15, 5, 27, 28, 29, 22, 30, 1, 31, 32, 9, 16, 2, 33, 25, 34, 13, 35, 36, 37 | pgpfac1lem3a 19862 |
. . . . . . . . . . 11
β’ (π β (π β₯ πΈ β§ π β₯ π)) |
39 | 38 | simprd 497 |
. . . . . . . . . 10
β’ (π β π β₯ π) |
40 | | pgpprm 19382 |
. . . . . . . . . . . . 13
β’ (π pGrp πΊ β π β β) |
41 | 30, 40 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π β β) |
42 | | prmz 16558 |
. . . . . . . . . . . 12
β’ (π β β β π β
β€) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . 11
β’ (π β π β β€) |
44 | | prmnn 16557 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β) |
45 | 41, 44 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π β β) |
46 | 45 | nnne0d 12210 |
. . . . . . . . . . 11
β’ (π β π β 0) |
47 | | dvdsval2 16146 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π β 0 β§ π β β€) β (π β₯ π β (π / π) β β€)) |
48 | 43, 46, 36, 47 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β (π β₯ π β (π / π) β β€)) |
49 | 39, 48 | mpbid 231 |
. . . . . . . . 9
β’ (π β (π / π) β β€) |
50 | 17 | snssd 4774 |
. . . . . . . . . . . 12
β’ (π β {π΄} β π΅) |
51 | 8, 18, 50 | mrcssidd 17512 |
. . . . . . . . . . 11
β’ (π β {π΄} β (πΎβ{π΄})) |
52 | 51, 15 | sseqtrrdi 4000 |
. . . . . . . . . 10
β’ (π β {π΄} β π) |
53 | | snssg 4749 |
. . . . . . . . . . 11
β’ (π΄ β π β (π΄ β π β {π΄} β π)) |
54 | 16, 53 | syl 17 |
. . . . . . . . . 10
β’ (π β (π΄ β π β {π΄} β π)) |
55 | 52, 54 | mpbird 257 |
. . . . . . . . 9
β’ (π β π΄ β π) |
56 | 35 | subgmulgcl 18948 |
. . . . . . . . 9
β’ ((π β (SubGrpβπΊ) β§ (π / π) β β€ β§ π΄ β π) β ((π / π) Β· π΄) β π) |
57 | 21, 49, 55, 56 | syl3anc 1372 |
. . . . . . . 8
β’ (π β ((π / π) Β· π΄) β π) |
58 | 26, 57 | sseldd 3950 |
. . . . . . 7
β’ (π β ((π / π) Β· π΄) β π) |
59 | | eqid 2737 |
. . . . . . . 8
β’
(+gβπΊ) = (+gβπΊ) |
60 | 59 | subgcl 18945 |
. . . . . . 7
β’ ((π β (SubGrpβπΊ) β§ πΆ β π β§ ((π / π) Β· π΄) β π) β (πΆ(+gβπΊ)((π / π) Β· π΄)) β π) |
61 | 9, 14, 58, 60 | syl3anc 1372 |
. . . . . 6
β’ (π β (πΆ(+gβπΊ)((π / π) Β· π΄)) β π) |
62 | 12, 61 | eqeltrid 2842 |
. . . . 5
β’ (π β π· β π) |
63 | 11, 62 | sseldd 3950 |
. . . 4
β’ (π β π· β π΅) |
64 | 18 | mrcsncl 17499 |
. . . 4
β’
(((SubGrpβπΊ)
β (Mooreβπ΅)
β§ π· β π΅) β (πΎβ{π·}) β (SubGrpβπΊ)) |
65 | 8, 63, 64 | syl2anc 585 |
. . 3
β’ (π β (πΎβ{π·}) β (SubGrpβπΊ)) |
66 | 22 | lsmsubg2 19644 |
. . 3
β’ ((πΊ β Abel β§ π β (SubGrpβπΊ) β§ (πΎβ{π·}) β (SubGrpβπΊ)) β (π β (πΎβ{π·})) β (SubGrpβπΊ)) |
67 | 1, 2, 65, 66 | syl3anc 1372 |
. 2
β’ (π β (π β (πΎβ{π·})) β (SubGrpβπΊ)) |
68 | | eqid 2737 |
. . . . . . . . . . 11
β’
(-gβπΊ) = (-gβπΊ) |
69 | 68, 22, 2, 65 | lsmelvalm 19440 |
. . . . . . . . . 10
β’ (π β (π₯ β (π β (πΎβ{π·})) β βπ€ β π βπ¦ β (πΎβ{π·})π₯ = (π€(-gβπΊ)π¦))) |
70 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’ (π β β€ β¦ (π Β· π·)) = (π β β€ β¦ (π Β· π·)) |
71 | 5, 35, 70, 18 | cycsubg2 19010 |
. . . . . . . . . . . . . 14
β’ ((πΊ β Grp β§ π· β π΅) β (πΎβ{π·}) = ran (π β β€ β¦ (π Β· π·))) |
72 | 4, 63, 71 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β (πΎβ{π·}) = ran (π β β€ β¦ (π Β· π·))) |
73 | 72 | rexeqdv 3317 |
. . . . . . . . . . . 12
β’ (π β (βπ¦ β (πΎβ{π·})π₯ = (π€(-gβπΊ)π¦) β βπ¦ β ran (π β β€ β¦ (π Β· π·))π₯ = (π€(-gβπΊ)π¦))) |
74 | | ovex 7395 |
. . . . . . . . . . . . . 14
β’ (π Β· π·) β V |
75 | 74 | rgenw 3069 |
. . . . . . . . . . . . 13
β’
βπ β
β€ (π Β· π·) β V |
76 | | oveq2 7370 |
. . . . . . . . . . . . . . 15
β’ (π¦ = (π Β· π·) β (π€(-gβπΊ)π¦) = (π€(-gβπΊ)(π Β· π·))) |
77 | 76 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
β’ (π¦ = (π Β· π·) β (π₯ = (π€(-gβπΊ)π¦) β π₯ = (π€(-gβπΊ)(π Β· π·)))) |
78 | 70, 77 | rexrnmptw 7050 |
. . . . . . . . . . . . 13
β’
(βπ β
β€ (π Β· π·) β V β (βπ¦ β ran (π β β€ β¦ (π Β· π·))π₯ = (π€(-gβπΊ)π¦) β βπ β β€ π₯ = (π€(-gβπΊ)(π Β· π·)))) |
79 | 75, 78 | ax-mp 5 |
. . . . . . . . . . . 12
β’
(βπ¦ β ran
(π β β€ β¦
(π Β· π·))π₯ = (π€(-gβπΊ)π¦) β βπ β β€ π₯ = (π€(-gβπΊ)(π Β· π·))) |
80 | 73, 79 | bitrdi 287 |
. . . . . . . . . . 11
β’ (π β (βπ¦ β (πΎβ{π·})π₯ = (π€(-gβπΊ)π¦) β βπ β β€ π₯ = (π€(-gβπΊ)(π Β· π·)))) |
81 | 80 | rexbidv 3176 |
. . . . . . . . . 10
β’ (π β (βπ€ β π βπ¦ β (πΎβ{π·})π₯ = (π€(-gβπΊ)π¦) β βπ€ β π βπ β β€ π₯ = (π€(-gβπΊ)(π Β· π·)))) |
82 | 69, 81 | bitrd 279 |
. . . . . . . . 9
β’ (π β (π₯ β (π β (πΎβ{π·})) β βπ€ β π βπ β β€ π₯ = (π€(-gβπΊ)(π Β· π·)))) |
83 | 82 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (π₯ β (π β (πΎβ{π·})) β βπ€ β π βπ β β€ π₯ = (π€(-gβπΊ)(π Β· π·)))) |
84 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β π₯ = (π€(-gβπΊ)(π Β· π·))) |
85 | 2 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β π β (SubGrpβπΊ)) |
86 | | simplrl 776 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β π€ β π) |
87 | | simplrr 777 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β π β β€) |
88 | 87 | zcnd 12615 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β π β β) |
89 | 45 | nncnd 12176 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β) |
90 | 89 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β π β β) |
91 | 46 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β π β 0) |
92 | 88, 90, 91 | divcan1d 11939 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β ((π / π) Β· π) = π) |
93 | 92 | oveq1d 7377 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β (((π / π) Β· π) Β· π·) = (π Β· π·)) |
94 | 4 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β πΊ β Grp) |
95 | 13 | eldifbd 3928 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Β¬ πΆ β (π β π)) |
96 | 22 | lsmsubg2 19644 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΊ β Abel β§ π β (SubGrpβπΊ) β§ π β (SubGrpβπΊ)) β (π β π) β (SubGrpβπΊ)) |
97 | 1, 21, 2, 96 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π β π) β (SubGrpβπΊ)) |
98 | 24, 57 | sseldd 3950 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((π / π) Β· π΄) β (π β π)) |
99 | 68 | subgsubcl 18946 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β π) β (SubGrpβπΊ) β§ π· β (π β π) β§ ((π / π) Β· π΄) β (π β π)) β (π·(-gβπΊ)((π / π) Β· π΄)) β (π β π)) |
100 | 99 | 3expia 1122 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β π) β (SubGrpβπΊ) β§ π· β (π β π)) β (((π / π) Β· π΄) β (π β π) β (π·(-gβπΊ)((π / π) Β· π΄)) β (π β π))) |
101 | 100 | impancom 453 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β π) β (SubGrpβπΊ) β§ ((π / π) Β· π΄) β (π β π)) β (π· β (π β π) β (π·(-gβπΊ)((π / π) Β· π΄)) β (π β π))) |
102 | 97, 98, 101 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π· β (π β π) β (π·(-gβπΊ)((π / π) Β· π΄)) β (π β π))) |
103 | 12 | oveq1i 7372 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π·(-gβπΊ)((π / π) Β· π΄)) = ((πΆ(+gβπΊ)((π / π) Β· π΄))(-gβπΊ)((π / π) Β· π΄)) |
104 | 11, 14 | sseldd 3950 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β πΆ β π΅) |
105 | 5 | subgss 18936 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (SubGrpβπΊ) β π β π΅) |
106 | 21, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π β π΅) |
107 | 106, 57 | sseldd 3950 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β ((π / π) Β· π΄) β π΅) |
108 | 5, 59, 68 | grppncan 18845 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πΊ β Grp β§ πΆ β π΅ β§ ((π / π) Β· π΄) β π΅) β ((πΆ(+gβπΊ)((π / π) Β· π΄))(-gβπΊ)((π / π) Β· π΄)) = πΆ) |
109 | 4, 104, 107, 108 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((πΆ(+gβπΊ)((π / π) Β· π΄))(-gβπΊ)((π / π) Β· π΄)) = πΆ) |
110 | 103, 109 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π·(-gβπΊ)((π / π) Β· π΄)) = πΆ) |
111 | 110 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π·(-gβπΊ)((π / π) Β· π΄)) β (π β π) β πΆ β (π β π))) |
112 | 102, 111 | sylibd 238 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π· β (π β π) β πΆ β (π β π))) |
113 | 95, 112 | mtod 197 |
. . . . . . . . . . . . . . . . . 18
β’ (π β Β¬ π· β (π β π)) |
114 | 113 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β Β¬ π· β (π β π)) |
115 | 41 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β π β β) |
116 | | coprm 16594 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β€) β (Β¬
π β₯ π β (π gcd π) = 1)) |
117 | 115, 87, 116 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β (Β¬ π β₯ π β (π gcd π) = 1)) |
118 | 43 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β π β β€) |
119 | | bezout 16431 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β€ β§ π β β€) β
βπ β β€
βπ β β€
(π gcd π) = ((π Β· π) + (π Β· π))) |
120 | 118, 87, 119 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β βπ β β€ βπ β β€ (π gcd π) = ((π Β· π) + (π Β· π))) |
121 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π gcd π) = 1 β ((π gcd π) = ((π Β· π) + (π Β· π)) β 1 = ((π Β· π) + (π Β· π)))) |
122 | 121 | 2rexbidv 3214 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π gcd π) = 1 β (βπ β β€ βπ β β€ (π gcd π) = ((π Β· π) + (π Β· π)) β βπ β β€ βπ β β€ 1 = ((π Β· π) + (π Β· π)))) |
123 | 120, 122 | syl5ibcom 244 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β ((π gcd π) = 1 β βπ β β€ βπ β β€ 1 = ((π Β· π) + (π Β· π)))) |
124 | 94 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β πΊ β Grp) |
125 | 118 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β π β β€) |
126 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β π β β€) |
127 | 125, 126 | zmulcld 12620 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β (π Β· π) β β€) |
128 | 87 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β π β β€) |
129 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β π β β€) |
130 | 128, 129 | zmulcld 12620 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β (π Β· π) β β€) |
131 | 63 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β π· β π΅) |
132 | 131 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β π· β π΅) |
133 | 5, 35, 59 | mulgdir 18915 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΊ β Grp β§ ((π Β· π) β β€ β§ (π Β· π) β β€ β§ π· β π΅)) β (((π Β· π) + (π Β· π)) Β· π·) = (((π Β· π) Β· π·)(+gβπΊ)((π Β· π) Β· π·))) |
134 | 124, 127,
130, 132, 133 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β (((π Β· π) + (π Β· π)) Β· π·) = (((π Β· π) Β· π·)(+gβπΊ)((π Β· π) Β· π·))) |
135 | 97 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β (π β π) β (SubGrpβπΊ)) |
136 | 135 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β (π β π) β (SubGrpβπΊ)) |
137 | 90 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β π β β) |
138 | | zcn 12511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β β€ β π β
β) |
139 | 138 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β π β β) |
140 | 137, 139 | mulcomd 11183 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β (π Β· π) = (π Β· π)) |
141 | 140 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β ((π Β· π) Β· π·) = ((π Β· π) Β· π·)) |
142 | 5, 35 | mulgass 18920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πΊ β Grp β§ (π β β€ β§ π β β€ β§ π· β π΅)) β ((π Β· π) Β· π·) = (π Β· (π Β· π·))) |
143 | 124, 126,
125, 132, 142 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β ((π Β· π) Β· π·) = (π Β· (π Β· π·))) |
144 | 141, 143 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β ((π Β· π) Β· π·) = (π Β· (π Β· π·))) |
145 | 22 | lsmub2 19447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β (SubGrpβπΊ) β§ π β (SubGrpβπΊ)) β π β (π β π)) |
146 | 21, 2, 145 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β π β (π β π)) |
147 | 12 | oveq2i 7373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π Β· π·) = (π Β· (πΆ(+gβπΊ)((π / π) Β· π΄))) |
148 | 5, 35, 59 | mulgdi 19612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((πΊ β Abel β§ (π β β€ β§ πΆ β π΅ β§ ((π / π) Β· π΄) β π΅)) β (π Β· (πΆ(+gβπΊ)((π / π) Β· π΄))) = ((π Β· πΆ)(+gβπΊ)(π Β· ((π / π) Β· π΄)))) |
149 | 1, 43, 104, 107, 148 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β (π Β· (πΆ(+gβπΊ)((π / π) Β· π΄))) = ((π Β· πΆ)(+gβπΊ)(π Β· ((π / π) Β· π΄)))) |
150 | 147, 149 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β (π Β· π·) = ((π Β· πΆ)(+gβπΊ)(π Β· ((π / π) Β· π΄)))) |
151 | 5, 35 | mulgass 18920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((πΊ β Grp β§ (π β β€ β§ (π / π) β β€ β§ π΄ β π΅)) β ((π Β· (π / π)) Β· π΄) = (π Β· ((π / π) Β· π΄))) |
152 | 4, 43, 49, 17, 151 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β ((π Β· (π / π)) Β· π΄) = (π Β· ((π / π) Β· π΄))) |
153 | 36 | zcnd 12615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β π β β) |
154 | 153, 89, 46 | divcan2d 11940 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β (π Β· (π / π)) = π) |
155 | 154 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β ((π Β· (π / π)) Β· π΄) = (π Β· π΄)) |
156 | 152, 155 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β (π Β· ((π / π) Β· π΄)) = (π Β· π΄)) |
157 | 156 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β ((π Β· πΆ)(+gβπΊ)(π Β· ((π / π) Β· π΄))) = ((π Β· πΆ)(+gβπΊ)(π Β· π΄))) |
158 | 150, 157 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β (π Β· π·) = ((π Β· πΆ)(+gβπΊ)(π Β· π΄))) |
159 | 158, 37 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (π Β· π·) β π) |
160 | 146, 159 | sseldd 3950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (π Β· π·) β (π β π)) |
161 | 160 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β (π Β· π·) β (π β π)) |
162 | 161 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β (π Β· π·) β (π β π)) |
163 | 35 | subgmulgcl 18948 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β π) β (SubGrpβπΊ) β§ π β β€ β§ (π Β· π·) β (π β π)) β (π Β· (π Β· π·)) β (π β π)) |
164 | 136, 126,
162, 163 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β (π Β· (π Β· π·)) β (π β π)) |
165 | 144, 164 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β ((π Β· π) Β· π·) β (π β π)) |
166 | 88 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β π β β) |
167 | | zcn 12511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β β€ β π β
β) |
168 | 167 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β π β β) |
169 | 166, 168 | mulcomd 11183 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β (π Β· π) = (π Β· π)) |
170 | 169 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β ((π Β· π) Β· π·) = ((π Β· π) Β· π·)) |
171 | 5, 35 | mulgass 18920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πΊ β Grp β§ (π β β€ β§ π β β€ β§ π· β π΅)) β ((π Β· π) Β· π·) = (π Β· (π Β· π·))) |
172 | 124, 129,
128, 132, 171 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β ((π Β· π) Β· π·) = (π Β· (π Β· π·))) |
173 | 170, 172 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β ((π Β· π) Β· π·) = (π Β· (π Β· π·))) |
174 | 84 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β (π€(-gβπΊ)π₯) = (π€(-gβπΊ)(π€(-gβπΊ)(π Β· π·)))) |
175 | 1 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β πΊ β Abel) |
176 | 5 | subgss 18936 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β (SubGrpβπΊ) β π β π΅) |
177 | 85, 176 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β π β π΅) |
178 | 177, 86 | sseldd 3950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β π€ β π΅) |
179 | 5, 35 | mulgcl 18900 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((πΊ β Grp β§ π β β€ β§ π· β π΅) β (π Β· π·) β π΅) |
180 | 94, 87, 131, 179 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β (π Β· π·) β π΅) |
181 | 5, 68, 175, 178, 180 | ablnncan 19606 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β (π€(-gβπΊ)(π€(-gβπΊ)(π Β· π·))) = (π Β· π·)) |
182 | 174, 181 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β (π€(-gβπΊ)π₯) = (π Β· π·)) |
183 | 146 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β π β (π β π)) |
184 | 183, 86 | sseldd 3950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β π€ β (π β π)) |
185 | 24 | sselda 3949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π₯ β π) β π₯ β (π β π)) |
186 | 185 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β π₯ β (π β π)) |
187 | 68 | subgsubcl 18946 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β π) β (SubGrpβπΊ) β§ π€ β (π β π) β§ π₯ β (π β π)) β (π€(-gβπΊ)π₯) β (π β π)) |
188 | 135, 184,
186, 187 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β (π€(-gβπΊ)π₯) β (π β π)) |
189 | 182, 188 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β (π Β· π·) β (π β π)) |
190 | 189 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β (π Β· π·) β (π β π)) |
191 | 35 | subgmulgcl 18948 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β π) β (SubGrpβπΊ) β§ π β β€ β§ (π Β· π·) β (π β π)) β (π Β· (π Β· π·)) β (π β π)) |
192 | 136, 129,
190, 191 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β (π Β· (π Β· π·)) β (π β π)) |
193 | 173, 192 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β ((π Β· π) Β· π·) β (π β π)) |
194 | 59 | subgcl 18945 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β π) β (SubGrpβπΊ) β§ ((π Β· π) Β· π·) β (π β π) β§ ((π Β· π) Β· π·) β (π β π)) β (((π Β· π) Β· π·)(+gβπΊ)((π Β· π) Β· π·)) β (π β π)) |
195 | 136, 165,
193, 194 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β (((π Β· π) Β· π·)(+gβπΊ)((π Β· π) Β· π·)) β (π β π)) |
196 | 134, 195 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β (((π Β· π) + (π Β· π)) Β· π·) β (π β π)) |
197 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (1 =
((π Β· π) + (π Β· π)) β (1 Β· π·) = (((π Β· π) + (π Β· π)) Β· π·)) |
198 | 197 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (1 =
((π Β· π) + (π Β· π)) β ((1 Β· π·) β (π β π) β (((π Β· π) + (π Β· π)) Β· π·) β (π β π))) |
199 | 196, 198 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β§ (π β β€ β§ π β β€)) β (1 = ((π Β· π) + (π Β· π)) β (1 Β· π·) β (π β π))) |
200 | 199 | rexlimdvva 3206 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β (βπ β β€ βπ β β€ 1 = ((π Β· π) + (π Β· π)) β (1 Β· π·) β (π β π))) |
201 | 123, 200 | syld 47 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β ((π gcd π) = 1 β (1 Β· π·) β (π β π))) |
202 | 5, 35 | mulg1 18890 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π· β π΅ β (1 Β· π·) = π·) |
203 | 131, 202 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β (1 Β· π·) = π·) |
204 | 203 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β ((1 Β· π·) β (π β π) β π· β (π β π))) |
205 | 201, 204 | sylibd 238 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β ((π gcd π) = 1 β π· β (π β π))) |
206 | 117, 205 | sylbid 239 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β (Β¬ π β₯ π β π· β (π β π))) |
207 | 114, 206 | mt3d 148 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β π β₯ π) |
208 | | dvdsval2 16146 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β€ β§ π β 0 β§ π β β€) β (π β₯ π β (π / π) β β€)) |
209 | 118, 91, 87, 208 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β (π β₯ π β (π / π) β β€)) |
210 | 207, 209 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β (π / π) β β€) |
211 | 5, 35 | mulgass 18920 |
. . . . . . . . . . . . . . 15
β’ ((πΊ β Grp β§ ((π / π) β β€ β§ π β β€ β§ π· β π΅)) β (((π / π) Β· π) Β· π·) = ((π / π) Β· (π Β· π·))) |
212 | 94, 210, 118, 131, 211 | syl13anc 1373 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β (((π / π) Β· π) Β· π·) = ((π / π) Β· (π Β· π·))) |
213 | 93, 212 | eqtr3d 2779 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β (π Β· π·) = ((π / π) Β· (π Β· π·))) |
214 | 159 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β (π Β· π·) β π) |
215 | 35 | subgmulgcl 18948 |
. . . . . . . . . . . . . 14
β’ ((π β (SubGrpβπΊ) β§ (π / π) β β€ β§ (π Β· π·) β π) β ((π / π) Β· (π Β· π·)) β π) |
216 | 85, 210, 214, 215 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β ((π / π) Β· (π Β· π·)) β π) |
217 | 213, 216 | eqeltrd 2838 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β (π Β· π·) β π) |
218 | 68 | subgsubcl 18946 |
. . . . . . . . . . . 12
β’ ((π β (SubGrpβπΊ) β§ π€ β π β§ (π Β· π·) β π) β (π€(-gβπΊ)(π Β· π·)) β π) |
219 | 85, 86, 217, 218 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β (π€(-gβπΊ)(π Β· π·)) β π) |
220 | 84, 219 | eqeltrd 2838 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β§ π₯ = (π€(-gβπΊ)(π Β· π·))) β π₯ β π) |
221 | 220 | ex 414 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ (π€ β π β§ π β β€)) β (π₯ = (π€(-gβπΊ)(π Β· π·)) β π₯ β π)) |
222 | 221 | rexlimdvva 3206 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (βπ€ β π βπ β β€ π₯ = (π€(-gβπΊ)(π Β· π·)) β π₯ β π)) |
223 | 83, 222 | sylbid 239 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (π₯ β (π β (πΎβ{π·})) β π₯ β π)) |
224 | 223 | imdistanda 573 |
. . . . . 6
β’ (π β ((π₯ β π β§ π₯ β (π β (πΎβ{π·}))) β (π₯ β π β§ π₯ β π))) |
225 | | elin 3931 |
. . . . . 6
β’ (π₯ β (π β© (π β (πΎβ{π·}))) β (π₯ β π β§ π₯ β (π β (πΎβ{π·})))) |
226 | | elin 3931 |
. . . . . 6
β’ (π₯ β (π β© π) β (π₯ β π β§ π₯ β π)) |
227 | 224, 225,
226 | 3imtr4g 296 |
. . . . 5
β’ (π β (π₯ β (π β© (π β (πΎβ{π·}))) β π₯ β (π β© π))) |
228 | 227 | ssrdv 3955 |
. . . 4
β’ (π β (π β© (π β (πΎβ{π·}))) β (π β© π)) |
229 | 228, 33 | sseqtrd 3989 |
. . 3
β’ (π β (π β© (π β (πΎβ{π·}))) β { 0 }) |
230 | 29 | subg0cl 18943 |
. . . . . 6
β’ (π β (SubGrpβπΊ) β 0 β π) |
231 | 21, 230 | syl 17 |
. . . . 5
β’ (π β 0 β π) |
232 | 29 | subg0cl 18943 |
. . . . . 6
β’ ((π β (πΎβ{π·})) β (SubGrpβπΊ) β 0 β (π β (πΎβ{π·}))) |
233 | 67, 232 | syl 17 |
. . . . 5
β’ (π β 0 β (π β (πΎβ{π·}))) |
234 | 231, 233 | elind 4159 |
. . . 4
β’ (π β 0 β (π β© (π β (πΎβ{π·})))) |
235 | 234 | snssd 4774 |
. . 3
β’ (π β { 0 } β (π β© (π β (πΎβ{π·})))) |
236 | 229, 235 | eqssd 3966 |
. 2
β’ (π β (π β© (π β (πΎβ{π·}))) = { 0 }) |
237 | 22 | lsmass 19458 |
. . . 4
β’ ((π β (SubGrpβπΊ) β§ π β (SubGrpβπΊ) β§ (πΎβ{π·}) β (SubGrpβπΊ)) β ((π β π) β (πΎβ{π·})) = (π β (π β (πΎβ{π·})))) |
238 | 21, 2, 65, 237 | syl3anc 1372 |
. . 3
β’ (π β ((π β π) β (πΎβ{π·})) = (π β (π β (πΎβ{π·})))) |
239 | 62, 113 | eldifd 3926 |
. . . 4
β’ (π β π· β (π β (π β π))) |
240 | 18, 15, 5, 27, 28, 29, 22, 30, 1, 31, 32, 9, 16, 2, 33, 25, 34 | pgpfac1lem1 19860 |
. . . 4
β’ ((π β§ π· β (π β (π β π))) β ((π β π) β (πΎβ{π·})) = π) |
241 | 239, 240 | mpdan 686 |
. . 3
β’ (π β ((π β π) β (πΎβ{π·})) = π) |
242 | 238, 241 | eqtr3d 2779 |
. 2
β’ (π β (π β (π β (πΎβ{π·}))) = π) |
243 | | ineq2 4171 |
. . . . 5
β’ (π‘ = (π β (πΎβ{π·})) β (π β© π‘) = (π β© (π β (πΎβ{π·})))) |
244 | 243 | eqeq1d 2739 |
. . . 4
β’ (π‘ = (π β (πΎβ{π·})) β ((π β© π‘) = { 0 } β (π β© (π β (πΎβ{π·}))) = { 0 })) |
245 | | oveq2 7370 |
. . . . 5
β’ (π‘ = (π β (πΎβ{π·})) β (π β π‘) = (π β (π β (πΎβ{π·})))) |
246 | 245 | eqeq1d 2739 |
. . . 4
β’ (π‘ = (π β (πΎβ{π·})) β ((π β π‘) = π β (π β (π β (πΎβ{π·}))) = π)) |
247 | 244, 246 | anbi12d 632 |
. . 3
β’ (π‘ = (π β (πΎβ{π·})) β (((π β© π‘) = { 0 } β§ (π β π‘) = π) β ((π β© (π β (πΎβ{π·}))) = { 0 } β§ (π β (π β (πΎβ{π·}))) = π))) |
248 | 247 | rspcev 3584 |
. 2
β’ (((π β (πΎβ{π·})) β (SubGrpβπΊ) β§ ((π β© (π β (πΎβ{π·}))) = { 0 } β§ (π β (π β (πΎβ{π·}))) = π)) β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π)) |
249 | 67, 236, 242, 248 | syl12anc 836 |
1
β’ (π β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π)) |