Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . . . 8
โข (๐ = ๐ โ ๐ = ๐) |
2 | | oveq1 7369 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ pCnt (โฏโ๐ต)) = (๐ pCnt (โฏโ๐ต))) |
3 | 1, 2 | oveq12d 7380 |
. . . . . . 7
โข (๐ = ๐ โ (๐โ(๐ pCnt (โฏโ๐ต))) = (๐โ(๐ pCnt (โฏโ๐ต)))) |
4 | 3 | breq2d 5122 |
. . . . . 6
โข (๐ = ๐ โ ((๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต))) โ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต))))) |
5 | 4 | rabbidv 3418 |
. . . . 5
โข (๐ = ๐ โ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))} = {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) |
6 | | ablfac1.s |
. . . . 5
โข ๐ = (๐ โ ๐ด โฆ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) |
7 | | ablfac1.b |
. . . . . . 7
โข ๐ต = (Baseโ๐บ) |
8 | 7 | fvexi 6861 |
. . . . . 6
โข ๐ต โ V |
9 | 8 | rabex 5294 |
. . . . 5
โข {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))} โ V |
10 | 5, 6, 9 | fvmpt3i 6958 |
. . . 4
โข (๐ โ ๐ด โ (๐โ๐) = {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) |
11 | 10 | adantl 483 |
. . 3
โข ((๐ โง ๐ โ ๐ด) โ (๐โ๐) = {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) |
12 | 11 | fveq2d 6851 |
. 2
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ(๐โ๐)) = (โฏโ{๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))})) |
13 | | ablfac1.o |
. . . 4
โข ๐ = (odโ๐บ) |
14 | | eqid 2737 |
. . . 4
โข {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))} = {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))} |
15 | | eqid 2737 |
. . . 4
โข {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ((โฏโ๐ต) / (๐โ(๐ pCnt (โฏโ๐ต))))} = {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ((โฏโ๐ต) / (๐โ(๐ pCnt (โฏโ๐ต))))} |
16 | | ablfac1.g |
. . . . 5
โข (๐ โ ๐บ โ Abel) |
17 | 16 | adantr 482 |
. . . 4
โข ((๐ โง ๐ โ ๐ด) โ ๐บ โ Abel) |
18 | | ablfac1.f |
. . . . . . 7
โข (๐ โ ๐ต โ Fin) |
19 | | ablfac1.1 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
20 | | eqid 2737 |
. . . . . . 7
โข (๐โ(๐ pCnt (โฏโ๐ต))) = (๐โ(๐ pCnt (โฏโ๐ต))) |
21 | | eqid 2737 |
. . . . . . 7
โข
((โฏโ๐ต) /
(๐โ(๐ pCnt (โฏโ๐ต)))) = ((โฏโ๐ต) / (๐โ(๐ pCnt (โฏโ๐ต)))) |
22 | 7, 13, 6, 16, 18, 19, 20, 21 | ablfac1lem 19854 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ (((๐โ(๐ pCnt (โฏโ๐ต))) โ โ โง
((โฏโ๐ต) / (๐โ(๐ pCnt (โฏโ๐ต)))) โ โ) โง ((๐โ(๐ pCnt (โฏโ๐ต))) gcd ((โฏโ๐ต) / (๐โ(๐ pCnt (โฏโ๐ต))))) = 1 โง (โฏโ๐ต) = ((๐โ(๐ pCnt (โฏโ๐ต))) ยท ((โฏโ๐ต) / (๐โ(๐ pCnt (โฏโ๐ต))))))) |
23 | 22 | simp1d 1143 |
. . . . 5
โข ((๐ โง ๐ โ ๐ด) โ ((๐โ(๐ pCnt (โฏโ๐ต))) โ โ โง
((โฏโ๐ต) / (๐โ(๐ pCnt (โฏโ๐ต)))) โ โ)) |
24 | 23 | simpld 496 |
. . . 4
โข ((๐ โง ๐ โ ๐ด) โ (๐โ(๐ pCnt (โฏโ๐ต))) โ โ) |
25 | 23 | simprd 497 |
. . . 4
โข ((๐ โง ๐ โ ๐ด) โ ((โฏโ๐ต) / (๐โ(๐ pCnt (โฏโ๐ต)))) โ โ) |
26 | 22 | simp2d 1144 |
. . . 4
โข ((๐ โง ๐ โ ๐ด) โ ((๐โ(๐ pCnt (โฏโ๐ต))) gcd ((โฏโ๐ต) / (๐โ(๐ pCnt (โฏโ๐ต))))) = 1) |
27 | 22 | simp3d 1145 |
. . . 4
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ๐ต) = ((๐โ(๐ pCnt (โฏโ๐ต))) ยท ((โฏโ๐ต) / (๐โ(๐ pCnt (โฏโ๐ต)))))) |
28 | 7, 13, 14, 15, 17, 24, 25, 26, 27 | ablfacrp2 19853 |
. . 3
โข ((๐ โง ๐ โ ๐ด) โ ((โฏโ{๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) = (๐โ(๐ pCnt (โฏโ๐ต))) โง (โฏโ{๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ((โฏโ๐ต) / (๐โ(๐ pCnt (โฏโ๐ต))))}) = ((โฏโ๐ต) / (๐โ(๐ pCnt (โฏโ๐ต)))))) |
29 | 28 | simpld 496 |
. 2
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ{๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) = (๐โ(๐ pCnt (โฏโ๐ต)))) |
30 | 12, 29 | eqtrd 2777 |
1
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ(๐โ๐)) = (๐โ(๐ pCnt (โฏโ๐ต)))) |