Step | Hyp | Ref
| Expression |
1 | | ablfac1eu.1 |
. . . . 5
โข (๐ โ (๐บdom DProd ๐ โง (๐บ DProd ๐) = ๐ต)) |
2 | 1 | simpld 496 |
. . . 4
โข (๐ โ ๐บdom DProd ๐) |
3 | | ablfac1eu.2 |
. . . 4
โข (๐ โ dom ๐ = ๐ด) |
4 | 2, 3 | dprdf2 19787 |
. . 3
โข (๐ โ ๐:๐ดโถ(SubGrpโ๐บ)) |
5 | 4 | ffnd 6670 |
. 2
โข (๐ โ ๐ Fn ๐ด) |
6 | | ablfac1.b |
. . . . 5
โข ๐ต = (Baseโ๐บ) |
7 | | ablfac1.o |
. . . . 5
โข ๐ = (odโ๐บ) |
8 | | ablfac1.s |
. . . . 5
โข ๐ = (๐ โ ๐ด โฆ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) |
9 | | ablfac1.g |
. . . . 5
โข (๐ โ ๐บ โ Abel) |
10 | | ablfac1.f |
. . . . 5
โข (๐ โ ๐ต โ Fin) |
11 | | ablfac1.1 |
. . . . 5
โข (๐ โ ๐ด โ โ) |
12 | 6, 7, 8, 9, 10, 11 | ablfac1b 19850 |
. . . 4
โข (๐ โ ๐บdom DProd ๐) |
13 | 6 | fvexi 6857 |
. . . . . . 7
โข ๐ต โ V |
14 | 13 | rabex 5290 |
. . . . . 6
โข {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))} โ V |
15 | 14, 8 | dmmpti 6646 |
. . . . 5
โข dom ๐ = ๐ด |
16 | 15 | a1i 11 |
. . . 4
โข (๐ โ dom ๐ = ๐ด) |
17 | 12, 16 | dprdf2 19787 |
. . 3
โข (๐ โ ๐:๐ดโถ(SubGrpโ๐บ)) |
18 | 17 | ffnd 6670 |
. 2
โข (๐ โ ๐ Fn ๐ด) |
19 | 10 | adantr 482 |
. . . 4
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ Fin) |
20 | 17 | ffvelcdmda 7036 |
. . . . 5
โข ((๐ โง ๐ โ ๐ด) โ (๐โ๐) โ (SubGrpโ๐บ)) |
21 | 6 | subgss 18930 |
. . . . 5
โข ((๐โ๐) โ (SubGrpโ๐บ) โ (๐โ๐) โ ๐ต) |
22 | 20, 21 | syl 17 |
. . . 4
โข ((๐ โง ๐ โ ๐ด) โ (๐โ๐) โ ๐ต) |
23 | 19, 22 | ssfid 9212 |
. . 3
โข ((๐ โง ๐ โ ๐ด) โ (๐โ๐) โ Fin) |
24 | 4 | ffvelcdmda 7036 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ (๐โ๐) โ (SubGrpโ๐บ)) |
25 | 6 | subgss 18930 |
. . . . . 6
โข ((๐โ๐) โ (SubGrpโ๐บ) โ (๐โ๐) โ ๐ต) |
26 | 24, 25 | syl 17 |
. . . . 5
โข ((๐ โง ๐ โ ๐ด) โ (๐โ๐) โ ๐ต) |
27 | 26 | sselda 3945 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐ด) โง ๐ฅ โ (๐โ๐)) โ ๐ฅ โ ๐ต) |
28 | 6, 7 | odcl 19319 |
. . . . . . . 8
โข (๐ฅ โ ๐ต โ (๐โ๐ฅ) โ
โ0) |
29 | 27, 28 | syl 17 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐ด) โง ๐ฅ โ (๐โ๐)) โ (๐โ๐ฅ) โ
โ0) |
30 | 29 | nn0zd 12526 |
. . . . . 6
โข (((๐ โง ๐ โ ๐ด) โง ๐ฅ โ (๐โ๐)) โ (๐โ๐ฅ) โ โค) |
31 | 19, 26 | ssfid 9212 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด) โ (๐โ๐) โ Fin) |
32 | | hashcl 14257 |
. . . . . . . . 9
โข ((๐โ๐) โ Fin โ (โฏโ(๐โ๐)) โ
โ0) |
33 | 31, 32 | syl 17 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ(๐โ๐)) โ
โ0) |
34 | 33 | nn0zd 12526 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ(๐โ๐)) โ โค) |
35 | 34 | adantr 482 |
. . . . . 6
โข (((๐ โง ๐ โ ๐ด) โง ๐ฅ โ (๐โ๐)) โ (โฏโ(๐โ๐)) โ โค) |
36 | 11 | sselda 3945 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ ๐ โ โ) |
37 | | prmnn 16551 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด) โ ๐ โ โ) |
39 | | ablgrp 19568 |
. . . . . . . . . . . . . 14
โข (๐บ โ Abel โ ๐บ โ Grp) |
40 | 9, 39 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ ๐บ โ Grp) |
41 | 6 | grpbn0 18780 |
. . . . . . . . . . . . 13
โข (๐บ โ Grp โ ๐ต โ โ
) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ ๐ต โ โ
) |
43 | | hashnncl 14267 |
. . . . . . . . . . . . 13
โข (๐ต โ Fin โ
((โฏโ๐ต) โ
โ โ ๐ต โ
โ
)) |
44 | 10, 43 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ ((โฏโ๐ต) โ โ โ ๐ต โ โ
)) |
45 | 42, 44 | mpbird 257 |
. . . . . . . . . . 11
โข (๐ โ (โฏโ๐ต) โ
โ) |
46 | 45 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ๐ต) โ โ) |
47 | 36, 46 | pccld 16723 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด) โ (๐ pCnt (โฏโ๐ต)) โ
โ0) |
48 | 38, 47 | nnexpcld 14149 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ (๐โ(๐ pCnt (โฏโ๐ต))) โ โ) |
49 | 48 | nnzd 12527 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด) โ (๐โ(๐ pCnt (โฏโ๐ต))) โ โค) |
50 | 49 | adantr 482 |
. . . . . 6
โข (((๐ โง ๐ โ ๐ด) โง ๐ฅ โ (๐โ๐)) โ (๐โ(๐ pCnt (โฏโ๐ต))) โ โค) |
51 | 24 | adantr 482 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐ด) โง ๐ฅ โ (๐โ๐)) โ (๐โ๐) โ (SubGrpโ๐บ)) |
52 | 31 | adantr 482 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐ด) โง ๐ฅ โ (๐โ๐)) โ (๐โ๐) โ Fin) |
53 | | simpr 486 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐ด) โง ๐ฅ โ (๐โ๐)) โ ๐ฅ โ (๐โ๐)) |
54 | 7 | odsubdvds 19354 |
. . . . . . 7
โข (((๐โ๐) โ (SubGrpโ๐บ) โง (๐โ๐) โ Fin โง ๐ฅ โ (๐โ๐)) โ (๐โ๐ฅ) โฅ (โฏโ(๐โ๐))) |
55 | 51, 52, 53, 54 | syl3anc 1372 |
. . . . . 6
โข (((๐ โง ๐ โ ๐ด) โง ๐ฅ โ (๐โ๐)) โ (๐โ๐ฅ) โฅ (โฏโ(๐โ๐))) |
56 | | ablfac1eu.4 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ(๐โ๐)) = (๐โ๐ถ)) |
57 | | prmz 16552 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โค) |
58 | 36, 57 | syl 17 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด) โ ๐ โ โค) |
59 | | ablfac1eu.3 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ
โ0) |
60 | 59 | nn0zd 12526 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โค) |
61 | 47 | nn0zd 12526 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ (๐ pCnt (โฏโ๐ต)) โ โค) |
62 | 6 | lagsubg 18993 |
. . . . . . . . . . . . 13
โข (((๐โ๐) โ (SubGrpโ๐บ) โง ๐ต โ Fin) โ (โฏโ(๐โ๐)) โฅ (โฏโ๐ต)) |
63 | 24, 19, 62 | syl2anc 585 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ(๐โ๐)) โฅ (โฏโ๐ต)) |
64 | 56, 63 | eqbrtrrd 5130 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ด) โ (๐โ๐ถ) โฅ (โฏโ๐ต)) |
65 | 46 | nnzd 12527 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ๐ต) โ โค) |
66 | | pcdvdsb 16742 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง
(โฏโ๐ต) โ
โค โง ๐ถ โ
โ0) โ (๐ถ โค (๐ pCnt (โฏโ๐ต)) โ (๐โ๐ถ) โฅ (โฏโ๐ต))) |
67 | 36, 65, 59, 66 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ด) โ (๐ถ โค (๐ pCnt (โฏโ๐ต)) โ (๐โ๐ถ) โฅ (โฏโ๐ต))) |
68 | 64, 67 | mpbird 257 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โค (๐ pCnt (โฏโ๐ต))) |
69 | | eluz2 12770 |
. . . . . . . . . 10
โข ((๐ pCnt (โฏโ๐ต)) โ
(โคโฅโ๐ถ) โ (๐ถ โ โค โง (๐ pCnt (โฏโ๐ต)) โ โค โง ๐ถ โค (๐ pCnt (โฏโ๐ต)))) |
70 | 60, 61, 68, 69 | syl3anbrc 1344 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด) โ (๐ pCnt (โฏโ๐ต)) โ
(โคโฅโ๐ถ)) |
71 | | dvdsexp 16211 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ถ โ โ0
โง (๐ pCnt
(โฏโ๐ต)) โ
(โคโฅโ๐ถ)) โ (๐โ๐ถ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))) |
72 | 58, 59, 70, 71 | syl3anc 1372 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ (๐โ๐ถ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))) |
73 | 56, 72 | eqbrtrd 5128 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ(๐โ๐)) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))) |
74 | 73 | adantr 482 |
. . . . . 6
โข (((๐ โง ๐ โ ๐ด) โง ๐ฅ โ (๐โ๐)) โ (โฏโ(๐โ๐)) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))) |
75 | 30, 35, 50, 55, 74 | dvdstrd 16178 |
. . . . 5
โข (((๐ โง ๐ โ ๐ด) โง ๐ฅ โ (๐โ๐)) โ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))) |
76 | 26, 75 | ssrabdv 4032 |
. . . 4
โข ((๐ โง ๐ โ ๐ด) โ (๐โ๐) โ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) |
77 | | id 22 |
. . . . . . . . 9
โข (๐ = ๐ โ ๐ = ๐) |
78 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ pCnt (โฏโ๐ต)) = (๐ pCnt (โฏโ๐ต))) |
79 | 77, 78 | oveq12d 7376 |
. . . . . . . 8
โข (๐ = ๐ โ (๐โ(๐ pCnt (โฏโ๐ต))) = (๐โ(๐ pCnt (โฏโ๐ต)))) |
80 | 79 | breq2d 5118 |
. . . . . . 7
โข (๐ = ๐ โ ((๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต))) โ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต))))) |
81 | 80 | rabbidv 3416 |
. . . . . 6
โข (๐ = ๐ โ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))} = {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) |
82 | 81, 8, 14 | fvmpt3i 6954 |
. . . . 5
โข (๐ โ ๐ด โ (๐โ๐) = {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) |
83 | 82 | adantl 483 |
. . . 4
โข ((๐ โง ๐ โ ๐ด) โ (๐โ๐) = {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) |
84 | 76, 83 | sseqtrrd 3986 |
. . 3
โข ((๐ โง ๐ โ ๐ด) โ (๐โ๐) โ (๐โ๐)) |
85 | 48 | nnnn0d 12474 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ (๐โ(๐ pCnt (โฏโ๐ต))) โ
โ0) |
86 | | pcdvds 16737 |
. . . . . . . . . 10
โข ((๐ โ โ โง
(โฏโ๐ต) โ
โ) โ (๐โ(๐ pCnt (โฏโ๐ต))) โฅ (โฏโ๐ต)) |
87 | 36, 46, 86 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด) โ (๐โ(๐ pCnt (โฏโ๐ต))) โฅ (โฏโ๐ต)) |
88 | 2 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ ๐ด) โ ๐บdom DProd ๐) |
89 | 3 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ ๐ด) โ dom ๐ = ๐ด) |
90 | | ablfac1.2 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ท โ ๐ด) |
91 | 90 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ ๐ด) โ ๐ท โ ๐ด) |
92 | 88, 89, 91 | dprdres 19808 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ๐ด) โ (๐บdom DProd (๐ โพ ๐ท) โง (๐บ DProd (๐ โพ ๐ท)) โ (๐บ DProd ๐))) |
93 | 92 | simpld 496 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐ด) โ ๐บdom DProd (๐ โพ ๐ท)) |
94 | 4 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ ๐ด) โ ๐:๐ดโถ(SubGrpโ๐บ)) |
95 | 94, 91 | fssresd 6710 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ๐ด) โ (๐ โพ ๐ท):๐ทโถ(SubGrpโ๐บ)) |
96 | 95 | fdmd 6680 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐ด) โ dom (๐ โพ ๐ท) = ๐ท) |
97 | | difssd 4093 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐ด) โ (๐ท โ {๐}) โ ๐ท) |
98 | 93, 96, 97 | dprdres 19808 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ด) โ (๐บdom DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})) โง (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))) โ (๐บ DProd (๐ โพ ๐ท)))) |
99 | 98 | simpld 496 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ด) โ ๐บdom DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))) |
100 | | dprdsubg 19804 |
. . . . . . . . . . 11
โข (๐บdom DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})) โ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))) โ (SubGrpโ๐บ)) |
101 | 99, 100 | syl 17 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))) โ (SubGrpโ๐บ)) |
102 | 6 | lagsubg 18993 |
. . . . . . . . . 10
โข (((๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))) โ (SubGrpโ๐บ) โง ๐ต โ Fin) โ (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))) โฅ (โฏโ๐ต)) |
103 | 101, 19, 102 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))) โฅ (โฏโ๐ต)) |
104 | | eqid 2737 |
. . . . . . . . . . . . . . 15
โข
(0gโ๐บ) = (0gโ๐บ) |
105 | 104 | subg0cl 18937 |
. . . . . . . . . . . . . 14
โข ((๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))) โ (SubGrpโ๐บ) โ (0gโ๐บ) โ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))) |
106 | 101, 105 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐ด) โ (0gโ๐บ) โ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))) |
107 | 106 | ne0d 4296 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ด) โ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))) โ โ
) |
108 | 6 | dprdssv 19796 |
. . . . . . . . . . . . . 14
โข (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))) โ ๐ต |
109 | | ssfi 9118 |
. . . . . . . . . . . . . 14
โข ((๐ต โ Fin โง (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))) โ ๐ต) โ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))) โ Fin) |
110 | 19, 108, 109 | sylancl 587 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐ด) โ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))) โ Fin) |
111 | | hashnncl 14267 |
. . . . . . . . . . . . 13
โข ((๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))) โ Fin โ ((โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))) โ โ โ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))) โ โ
)) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ด) โ ((โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))) โ โ โ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))) โ โ
)) |
113 | 107, 112 | mpbird 257 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))) โ โ) |
114 | 113 | nnzd 12527 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))) โ โค) |
115 | | id 22 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ โ ๐ฅ = ๐) |
116 | | sneq 4597 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ = ๐ โ {๐ฅ} = {๐}) |
117 | 116 | difeq2d 4083 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ = ๐ โ (๐ท โ {๐ฅ}) = (๐ท โ {๐})) |
118 | 117 | reseq2d 5938 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ = ๐ โ ((๐ โพ ๐ท) โพ (๐ท โ {๐ฅ})) = ((๐ โพ ๐ท) โพ (๐ท โ {๐}))) |
119 | 118 | oveq2d 7374 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = ๐ โ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐ฅ}))) = (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))) |
120 | 119 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ โ (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐ฅ})))) = (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) |
121 | 115, 120 | breq12d 5119 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ โ (๐ฅ โฅ (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐ฅ})))) โ ๐ โฅ (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))))) |
122 | 121 | notbid 318 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ โ (ยฌ ๐ฅ โฅ (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐ฅ})))) โ ยฌ ๐ โฅ (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))))) |
123 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ท โฆ {๐ฆ โ ๐ต โฃ (๐โ๐ฆ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) = (๐ โ ๐ท โฆ {๐ฆ โ ๐ต โฃ (๐โ๐ฆ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) |
124 | 9 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ โ) โ ๐บ โ Abel) |
125 | 10 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ โ) โ ๐ต โ Fin) |
126 | | ablfac1c.d |
. . . . . . . . . . . . . . . . . 18
โข ๐ท = {๐ค โ โ โฃ ๐ค โฅ (โฏโ๐ต)} |
127 | 126 | ssrab3 4041 |
. . . . . . . . . . . . . . . . 17
โข ๐ท โ
โ |
128 | 127 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ โ) โ ๐ท โ โ) |
129 | | ssidd 3968 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ โ) โ ๐ท โ ๐ท) |
130 | 2, 3, 90 | dprdres 19808 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐บdom DProd (๐ โพ ๐ท) โง (๐บ DProd (๐ โพ ๐ท)) โ (๐บ DProd ๐))) |
131 | 130 | simpld 496 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐บdom DProd (๐ โพ ๐ท)) |
132 | | dprdsubg 19804 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐บdom DProd (๐ โพ ๐ท) โ (๐บ DProd (๐ โพ ๐ท)) โ (SubGrpโ๐บ)) |
133 | 131, 132 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐บ DProd (๐ โพ ๐ท)) โ (SubGrpโ๐บ)) |
134 | | difssd 4093 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (๐ด โ ๐ท) โ ๐ด) |
135 | 2, 3, 134 | dprdres 19808 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐บdom DProd (๐ โพ (๐ด โ ๐ท)) โง (๐บ DProd (๐ โพ (๐ด โ ๐ท))) โ (๐บ DProd ๐))) |
136 | 135 | simpld 496 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ๐บdom DProd (๐ โพ (๐ด โ ๐ท))) |
137 | | dprdsubg 19804 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐บdom DProd (๐ โพ (๐ด โ ๐ท)) โ (๐บ DProd (๐ โพ (๐ด โ ๐ท))) โ (SubGrpโ๐บ)) |
138 | 136, 137 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐บ DProd (๐ โพ (๐ด โ ๐ท))) โ (SubGrpโ๐บ)) |
139 | | difss 4092 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ด โ ๐ท) โ ๐ด |
140 | | fssres 6709 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐:๐ดโถ(SubGrpโ๐บ) โง (๐ด โ ๐ท) โ ๐ด) โ (๐ โพ (๐ด โ ๐ท)):(๐ด โ ๐ท)โถ(SubGrpโ๐บ)) |
141 | 4, 139, 140 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐ โพ (๐ด โ ๐ท)):(๐ด โ ๐ท)โถ(SubGrpโ๐บ)) |
142 | 141 | fdmd 6680 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ dom (๐ โพ (๐ด โ ๐ท)) = (๐ด โ ๐ท)) |
143 | | fvres 6862 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (๐ด โ ๐ท) โ ((๐ โพ (๐ด โ ๐ท))โ๐) = (๐โ๐)) |
144 | 143 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ โ (๐ด โ ๐ท)) โ ((๐ โพ (๐ด โ ๐ท))โ๐) = (๐โ๐)) |
145 | | eldif 3921 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (๐ด โ ๐ท) โ (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) |
146 | 31 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ (๐โ๐) โ Fin) |
147 | 104 | subg0cl 18937 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐โ๐) โ (SubGrpโ๐บ) โ (0gโ๐บ) โ (๐โ๐)) |
148 | 24, 147 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ โง ๐ โ ๐ด) โ (0gโ๐บ) โ (๐โ๐)) |
149 | 148 | snssd 4770 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ โง ๐ โ ๐ด) โ {(0gโ๐บ)} โ (๐โ๐)) |
150 | 149 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ {(0gโ๐บ)} โ (๐โ๐)) |
151 | | fvex 6856 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
(0gโ๐บ) โ V |
152 | | hashsng 14270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
((0gโ๐บ) โ V โ
(โฏโ{(0gโ๐บ)}) = 1) |
153 | 151, 152 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
(โฏโ{(0gโ๐บ)}) = 1 |
154 | 56 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ (โฏโ(๐โ๐)) = (๐โ๐ถ)) |
155 | 36 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข (((๐ โง ๐ โ ๐ด) โง ๐ถ โ โ) โ ๐ โ โ) |
156 | | iddvdsexp 16163 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข ((๐ โ โค โง ๐ถ โ โ) โ ๐ โฅ (๐โ๐ถ)) |
157 | 58, 156 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข (((๐ โง ๐ โ ๐ด) โง ๐ถ โ โ) โ ๐ โฅ (๐โ๐ถ)) |
158 | 64 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข (((๐ โง ๐ โ ๐ด) โง ๐ถ โ โ) โ (๐โ๐ถ) โฅ (โฏโ๐ต)) |
159 | 56, 34 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข ((๐ โง ๐ โ ๐ด) โ (๐โ๐ถ) โ โค) |
160 | | dvdstr 16177 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข ((๐ โ โค โง (๐โ๐ถ) โ โค โง (โฏโ๐ต) โ โค) โ ((๐ โฅ (๐โ๐ถ) โง (๐โ๐ถ) โฅ (โฏโ๐ต)) โ ๐ โฅ (โฏโ๐ต))) |
161 | 58, 159, 65, 160 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข ((๐ โง ๐ โ ๐ด) โ ((๐ โฅ (๐โ๐ถ) โง (๐โ๐ถ) โฅ (โฏโ๐ต)) โ ๐ โฅ (โฏโ๐ต))) |
162 | 161 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข (((๐ โง ๐ โ ๐ด) โง ๐ถ โ โ) โ ((๐ โฅ (๐โ๐ถ) โง (๐โ๐ถ) โฅ (โฏโ๐ต)) โ ๐ โฅ (โฏโ๐ต))) |
163 | 157, 158,
162 | mp2and 698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข (((๐ โง ๐ โ ๐ด) โง ๐ถ โ โ) โ ๐ โฅ (โฏโ๐ต)) |
164 | | breq1 5109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข (๐ค = ๐ โ (๐ค โฅ (โฏโ๐ต) โ ๐ โฅ (โฏโ๐ต))) |
165 | 164, 126 | elrab2 3649 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข (๐ โ ๐ท โ (๐ โ โ โง ๐ โฅ (โฏโ๐ต))) |
166 | 155, 163,
165 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข (((๐ โง ๐ โ ๐ด) โง ๐ถ โ โ) โ ๐ โ ๐ท) |
167 | 166 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ โง ๐ โ ๐ด) โ (๐ถ โ โ โ ๐ โ ๐ท)) |
168 | 167 | con3d 152 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ โง ๐ โ ๐ด) โ (ยฌ ๐ โ ๐ท โ ยฌ ๐ถ โ โ)) |
169 | 168 | impr 456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ ยฌ ๐ถ โ โ) |
170 | 59 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ ๐ถ โ
โ0) |
171 | | elnn0 12416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (๐ถ โ โ0
โ (๐ถ โ โ
โจ ๐ถ =
0)) |
172 | 170, 171 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ (๐ถ โ โ โจ ๐ถ = 0)) |
173 | 172 | ord 863 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ (ยฌ ๐ถ โ โ โ ๐ถ = 0)) |
174 | 169, 173 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ ๐ถ = 0) |
175 | 174 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ (๐โ๐ถ) = (๐โ0)) |
176 | 38 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ ๐ โ โ) |
177 | 176 | nncnd 12170 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ ๐ โ โ) |
178 | 177 | exp0d 14046 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ (๐โ0) = 1) |
179 | 154, 175,
178 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ (โฏโ(๐โ๐)) = 1) |
180 | 153, 179 | eqtr4id 2796 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ
(โฏโ{(0gโ๐บ)}) = (โฏโ(๐โ๐))) |
181 | | snfi 8989 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
{(0gโ๐บ)} โ Fin |
182 | | hashen 14248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
(({(0gโ๐บ)} โ Fin โง (๐โ๐) โ Fin) โ
((โฏโ{(0gโ๐บ)}) = (โฏโ(๐โ๐)) โ {(0gโ๐บ)} โ (๐โ๐))) |
183 | 181, 146,
182 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ
((โฏโ{(0gโ๐บ)}) = (โฏโ(๐โ๐)) โ {(0gโ๐บ)} โ (๐โ๐))) |
184 | 180, 183 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ {(0gโ๐บ)} โ (๐โ๐)) |
185 | | fisseneq 9202 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐โ๐) โ Fin โง
{(0gโ๐บ)}
โ (๐โ๐) โง
{(0gโ๐บ)}
โ (๐โ๐)) โ
{(0gโ๐บ)} =
(๐โ๐)) |
186 | 146, 150,
184, 185 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ {(0gโ๐บ)} = (๐โ๐)) |
187 | 104 | subg0cl 18937 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐บ DProd (๐ โพ ๐ท)) โ (SubGrpโ๐บ) โ (0gโ๐บ) โ (๐บ DProd (๐ โพ ๐ท))) |
188 | 133, 187 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ (0gโ๐บ) โ (๐บ DProd (๐ โพ ๐ท))) |
189 | 188 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ (0gโ๐บ) โ (๐บ DProd (๐ โพ ๐ท))) |
190 | 189 | snssd 4770 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ {(0gโ๐บ)} โ (๐บ DProd (๐ โพ ๐ท))) |
191 | 186, 190 | eqsstrrd 3984 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ (๐โ๐) โ (๐บ DProd (๐ โพ ๐ท))) |
192 | 145, 191 | sylan2b 595 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ โ (๐ด โ ๐ท)) โ (๐โ๐) โ (๐บ DProd (๐ โพ ๐ท))) |
193 | 144, 192 | eqsstrd 3983 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ โ (๐ด โ ๐ท)) โ ((๐ โพ (๐ด โ ๐ท))โ๐) โ (๐บ DProd (๐ โพ ๐ท))) |
194 | 136, 142,
133, 193 | dprdlub 19806 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐บ DProd (๐ โพ (๐ด โ ๐ท))) โ (๐บ DProd (๐ โพ ๐ท))) |
195 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(LSSumโ๐บ) =
(LSSumโ๐บ) |
196 | 195 | lsmss2 19450 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐บ DProd (๐ โพ ๐ท)) โ (SubGrpโ๐บ) โง (๐บ DProd (๐ โพ (๐ด โ ๐ท))) โ (SubGrpโ๐บ) โง (๐บ DProd (๐ โพ (๐ด โ ๐ท))) โ (๐บ DProd (๐ โพ ๐ท))) โ ((๐บ DProd (๐ โพ ๐ท))(LSSumโ๐บ)(๐บ DProd (๐ โพ (๐ด โ ๐ท)))) = (๐บ DProd (๐ โพ ๐ท))) |
197 | 133, 138,
194, 196 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((๐บ DProd (๐ โพ ๐ท))(LSSumโ๐บ)(๐บ DProd (๐ โพ (๐ด โ ๐ท)))) = (๐บ DProd (๐ โพ ๐ท))) |
198 | | disjdif 4432 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ท โฉ (๐ด โ ๐ท)) = โ
|
199 | 198 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (๐ท โฉ (๐ด โ ๐ท)) = โ
) |
200 | | undif2 4437 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ท โช (๐ด โ ๐ท)) = (๐ท โช ๐ด) |
201 | | ssequn1 4141 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ท โ ๐ด โ (๐ท โช ๐ด) = ๐ด) |
202 | 90, 201 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐ท โช ๐ด) = ๐ด) |
203 | 200, 202 | eqtr2id 2790 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ๐ด = (๐ท โช (๐ด โ ๐ท))) |
204 | 4, 199, 203, 195, 2 | dprdsplit 19828 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐บ DProd ๐) = ((๐บ DProd (๐ โพ ๐ท))(LSSumโ๐บ)(๐บ DProd (๐ โพ (๐ด โ ๐ท))))) |
205 | 1 | simprd 497 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐บ DProd ๐) = ๐ต) |
206 | 204, 205 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((๐บ DProd (๐ โพ ๐ท))(LSSumโ๐บ)(๐บ DProd (๐ โพ (๐ด โ ๐ท)))) = ๐ต) |
207 | 197, 206 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐บ DProd (๐ โพ ๐ท)) = ๐ต) |
208 | 131, 207 | jca 513 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐บdom DProd (๐ โพ ๐ท) โง (๐บ DProd (๐ โพ ๐ท)) = ๐ต)) |
209 | 208 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ โ) โ (๐บdom DProd (๐ โพ ๐ท) โง (๐บ DProd (๐ โพ ๐ท)) = ๐ต)) |
210 | 4, 90 | fssresd 6710 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐ โพ ๐ท):๐ทโถ(SubGrpโ๐บ)) |
211 | 210 | fdmd 6680 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ dom (๐ โพ ๐ท) = ๐ท) |
212 | 211 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ โ) โ dom (๐ โพ ๐ท) = ๐ท) |
213 | 90 | sselda 3945 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ ๐ท) โ ๐ โ ๐ด) |
214 | 213, 59 | syldan 592 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ ๐ท) โ ๐ถ โ
โ0) |
215 | 214 | adantlr 714 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ท) โ ๐ถ โ
โ0) |
216 | | fvres 6862 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐ท โ ((๐ โพ ๐ท)โ๐) = (๐โ๐)) |
217 | 216 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ ๐ท) โ ((๐ โพ ๐ท)โ๐) = (๐โ๐)) |
218 | 217 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ ๐ท) โ (โฏโ((๐ โพ ๐ท)โ๐)) = (โฏโ(๐โ๐))) |
219 | 213, 56 | syldan 592 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ ๐ท) โ (โฏโ(๐โ๐)) = (๐โ๐ถ)) |
220 | 218, 219 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ ๐ท) โ (โฏโ((๐ โพ ๐ท)โ๐)) = (๐โ๐ถ)) |
221 | 220 | adantlr 714 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ท) โ (โฏโ((๐ โพ ๐ท)โ๐)) = (๐โ๐ถ)) |
222 | | simpr 486 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ โ) โ ๐ฅ โ โ) |
223 | | fzfid 13879 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (1...(โฏโ๐ต)) โ Fin) |
224 | | prmnn 16551 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ค โ โ โ ๐ค โ
โ) |
225 | 224 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ค โ โ โง ๐ค โฅ (โฏโ๐ต)) โ ๐ค โ โ) |
226 | | prmz 16552 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ค โ โ โ ๐ค โ
โค) |
227 | | dvdsle 16193 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ค โ โค โง
(โฏโ๐ต) โ
โ) โ (๐ค โฅ
(โฏโ๐ต) โ
๐ค โค (โฏโ๐ต))) |
228 | 226, 45, 227 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ค โ โ) โ (๐ค โฅ (โฏโ๐ต) โ ๐ค โค (โฏโ๐ต))) |
229 | 228 | 3impia 1118 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ค โ โ โง ๐ค โฅ (โฏโ๐ต)) โ ๐ค โค (โฏโ๐ต)) |
230 | 45 | nnzd 12527 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (โฏโ๐ต) โ
โค) |
231 | 230 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ค โ โ โง ๐ค โฅ (โฏโ๐ต)) โ (โฏโ๐ต) โ โค) |
232 | | fznn 13510 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
((โฏโ๐ต)
โ โค โ (๐ค
โ (1...(โฏโ๐ต)) โ (๐ค โ โ โง ๐ค โค (โฏโ๐ต)))) |
233 | 231, 232 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ค โ โ โง ๐ค โฅ (โฏโ๐ต)) โ (๐ค โ (1...(โฏโ๐ต)) โ (๐ค โ โ โง ๐ค โค (โฏโ๐ต)))) |
234 | 225, 229,
233 | mpbir2and 712 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ค โ โ โง ๐ค โฅ (โฏโ๐ต)) โ ๐ค โ (1...(โฏโ๐ต))) |
235 | 234 | rabssdv 4033 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ {๐ค โ โ โฃ ๐ค โฅ (โฏโ๐ต)} โ (1...(โฏโ๐ต))) |
236 | 126, 235 | eqsstrid 3993 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐ท โ (1...(โฏโ๐ต))) |
237 | 223, 236 | ssfid 9212 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ท โ Fin) |
238 | 237 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ โ) โ ๐ท โ Fin) |
239 | 6, 7, 123, 124, 125, 128, 126, 129, 209, 212, 215, 221, 222, 238 | ablfac1eulem 19852 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ โ) โ ยฌ ๐ฅ โฅ (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐ฅ}))))) |
240 | 239 | ralrimiva 3144 |
. . . . . . . . . . . . . 14
โข (๐ โ โ๐ฅ โ โ ยฌ ๐ฅ โฅ (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐ฅ}))))) |
241 | 240 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐ด) โ โ๐ฅ โ โ ยฌ ๐ฅ โฅ (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐ฅ}))))) |
242 | 122, 241,
36 | rspcdva 3583 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ด) โ ยฌ ๐ โฅ (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) |
243 | | coprm 16588 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง
(โฏโ(๐บ DProd
((๐ โพ ๐ท) โพ (๐ท โ {๐})))) โ โค) โ (ยฌ ๐ โฅ (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))) โ (๐ gcd (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) = 1)) |
244 | 36, 114, 243 | syl2anc 585 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ด) โ (ยฌ ๐ โฅ (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))) โ (๐ gcd (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) = 1)) |
245 | 242, 244 | mpbid 231 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ด) โ (๐ gcd (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) = 1) |
246 | | rpexp1i 16600 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง
(โฏโ(๐บ DProd
((๐ โพ ๐ท) โพ (๐ท โ {๐})))) โ โค โง (๐ pCnt (โฏโ๐ต)) โ โ0)
โ ((๐ gcd
(โฏโ(๐บ DProd
((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) = 1 โ ((๐โ(๐ pCnt (โฏโ๐ต))) gcd (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) = 1)) |
247 | 58, 114, 47, 246 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ด) โ ((๐ gcd (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) = 1 โ ((๐โ(๐ pCnt (โฏโ๐ต))) gcd (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) = 1)) |
248 | 245, 247 | mpd 15 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ ((๐โ(๐ pCnt (โฏโ๐ต))) gcd (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) = 1) |
249 | | coprmdvds2 16531 |
. . . . . . . . . 10
โข ((((๐โ(๐ pCnt (โฏโ๐ต))) โ โค โง
(โฏโ(๐บ DProd
((๐ โพ ๐ท) โพ (๐ท โ {๐})))) โ โค โง
(โฏโ๐ต) โ
โค) โง ((๐โ(๐ pCnt (โฏโ๐ต))) gcd (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) = 1) โ (((๐โ(๐ pCnt (โฏโ๐ต))) โฅ (โฏโ๐ต) โง (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))) โฅ (โฏโ๐ต)) โ ((๐โ(๐ pCnt (โฏโ๐ต))) ยท (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) โฅ (โฏโ๐ต))) |
250 | 49, 114, 65, 248, 249 | syl31anc 1374 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด) โ (((๐โ(๐ pCnt (โฏโ๐ต))) โฅ (โฏโ๐ต) โง (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))) โฅ (โฏโ๐ต)) โ ((๐โ(๐ pCnt (โฏโ๐ต))) ยท (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) โฅ (โฏโ๐ต))) |
251 | 87, 103, 250 | mp2and 698 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ ((๐โ(๐ pCnt (โฏโ๐ต))) ยท (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) โฅ (โฏโ๐ต)) |
252 | | eqid 2737 |
. . . . . . . . . 10
โข
(Cntzโ๐บ) =
(Cntzโ๐บ) |
253 | | inss1 4189 |
. . . . . . . . . . . . . 14
โข (๐ท โฉ {๐}) โ ๐ท |
254 | 253 | a1i 11 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐ด) โ (๐ท โฉ {๐}) โ ๐ท) |
255 | 93, 96, 254 | dprdres 19808 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ด) โ (๐บdom DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐})) โง (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐}))) โ (๐บ DProd (๐ โพ ๐ท)))) |
256 | 255 | simpld 496 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ด) โ ๐บdom DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐}))) |
257 | | dprdsubg 19804 |
. . . . . . . . . . 11
โข (๐บdom DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐})) โ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐}))) โ (SubGrpโ๐บ)) |
258 | 256, 257 | syl 17 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐}))) โ (SubGrpโ๐บ)) |
259 | | inass 4180 |
. . . . . . . . . . . . 13
โข ((๐ท โฉ {๐}) โฉ (๐ท โ {๐})) = (๐ท โฉ ({๐} โฉ (๐ท โ {๐}))) |
260 | | disjdif 4432 |
. . . . . . . . . . . . . 14
โข ({๐} โฉ (๐ท โ {๐})) = โ
|
261 | 260 | ineq2i 4170 |
. . . . . . . . . . . . 13
โข (๐ท โฉ ({๐} โฉ (๐ท โ {๐}))) = (๐ท โฉ โ
) |
262 | | in0 4352 |
. . . . . . . . . . . . 13
โข (๐ท โฉ โ
) =
โ
|
263 | 259, 261,
262 | 3eqtri 2769 |
. . . . . . . . . . . 12
โข ((๐ท โฉ {๐}) โฉ (๐ท โ {๐})) = โ
|
264 | 263 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ด) โ ((๐ท โฉ {๐}) โฉ (๐ท โ {๐})) = โ
) |
265 | 93, 96, 254, 97, 264, 104 | dprddisj2 19819 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ ((๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐}))) โฉ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))) = {(0gโ๐บ)}) |
266 | 93, 96, 254, 97, 264, 252 | dprdcntz2 19818 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐}))) โ ((Cntzโ๐บ)โ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) |
267 | 6 | dprdssv 19796 |
. . . . . . . . . . 11
โข (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐}))) โ ๐ต |
268 | | ssfi 9118 |
. . . . . . . . . . 11
โข ((๐ต โ Fin โง (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐}))) โ ๐ต) โ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐}))) โ Fin) |
269 | 19, 267, 268 | sylancl 587 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐}))) โ Fin) |
270 | 195, 104,
252, 258, 101, 265, 266, 269, 110 | lsmhash 19488 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ((๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐})))(LSSumโ๐บ)(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) = ((โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐})))) ยท (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))))) |
271 | | inundif 4439 |
. . . . . . . . . . . . . 14
โข ((๐ท โฉ {๐}) โช (๐ท โ {๐})) = ๐ท |
272 | 271 | eqcomi 2746 |
. . . . . . . . . . . . 13
โข ๐ท = ((๐ท โฉ {๐}) โช (๐ท โ {๐})) |
273 | 272 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ด) โ ๐ท = ((๐ท โฉ {๐}) โช (๐ท โ {๐}))) |
274 | 95, 264, 273, 195, 93 | dprdsplit 19828 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ด) โ (๐บ DProd (๐ โพ ๐ท)) = ((๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐})))(LSSumโ๐บ)(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) |
275 | 207 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ด) โ (๐บ DProd (๐ โพ ๐ท)) = ๐ต) |
276 | 274, 275 | eqtr3d 2779 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ ((๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐})))(LSSumโ๐บ)(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))) = ๐ต) |
277 | 276 | fveq2d 6847 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ((๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐})))(LSSumโ๐บ)(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) = (โฏโ๐ต)) |
278 | | snssi 4769 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ท โ {๐} โ ๐ท) |
279 | 278 | adantl 483 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ ๐ด) โง ๐ โ ๐ท) โ {๐} โ ๐ท) |
280 | | sseqin2 4176 |
. . . . . . . . . . . . . . . 16
โข ({๐} โ ๐ท โ (๐ท โฉ {๐}) = {๐}) |
281 | 279, 280 | sylib 217 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ ๐ด) โง ๐ โ ๐ท) โ (๐ท โฉ {๐}) = {๐}) |
282 | 281 | reseq2d 5938 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ ๐ด) โง ๐ โ ๐ท) โ ((๐ โพ ๐ท) โพ (๐ท โฉ {๐})) = ((๐ โพ ๐ท) โพ {๐})) |
283 | 282 | oveq2d 7374 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ ๐ด) โง ๐ โ ๐ท) โ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐}))) = (๐บ DProd ((๐ โพ ๐ท) โพ {๐}))) |
284 | 93 | adantr 482 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ ๐ด) โง ๐ โ ๐ท) โ ๐บdom DProd (๐ โพ ๐ท)) |
285 | 211 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ ๐ด) โง ๐ โ ๐ท) โ dom (๐ โพ ๐ท) = ๐ท) |
286 | | simpr 486 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ ๐ด) โง ๐ โ ๐ท) โ ๐ โ ๐ท) |
287 | 284, 285,
286 | dpjlem 19831 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ ๐ด) โง ๐ โ ๐ท) โ (๐บ DProd ((๐ โพ ๐ท) โพ {๐})) = ((๐ โพ ๐ท)โ๐)) |
288 | 216 | adantl 483 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ ๐ด) โง ๐ โ ๐ท) โ ((๐ โพ ๐ท)โ๐) = (๐โ๐)) |
289 | 283, 287,
288 | 3eqtrd 2781 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ ๐ด) โง ๐ โ ๐ท) โ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐}))) = (๐โ๐)) |
290 | | simprr 772 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ ยฌ ๐ โ ๐ท) |
291 | | disjsn 4673 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ท โฉ {๐}) = โ
โ ยฌ ๐ โ ๐ท) |
292 | 290, 291 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ (๐ท โฉ {๐}) = โ
) |
293 | 292 | reseq2d 5938 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ ((๐ โพ ๐ท) โพ (๐ท โฉ {๐})) = ((๐ โพ ๐ท) โพ โ
)) |
294 | | res0 5942 |
. . . . . . . . . . . . . . . 16
โข ((๐ โพ ๐ท) โพ โ
) =
โ
|
295 | 293, 294 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ ((๐ โพ ๐ท) โพ (๐ท โฉ {๐})) = โ
) |
296 | 295 | oveq2d 7374 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐}))) = (๐บ DProd โ
)) |
297 | 104 | dprd0 19811 |
. . . . . . . . . . . . . . . . 17
โข (๐บ โ Grp โ (๐บdom DProd โ
โง (๐บ DProd โ
) =
{(0gโ๐บ)})) |
298 | 40, 297 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐บdom DProd โ
โง (๐บ DProd โ
) =
{(0gโ๐บ)})) |
299 | 298 | simprd 497 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐บ DProd โ
) =
{(0gโ๐บ)}) |
300 | 299 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ (๐บ DProd โ
) =
{(0gโ๐บ)}) |
301 | 296, 300,
186 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ๐ด โง ยฌ ๐ โ ๐ท)) โ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐}))) = (๐โ๐)) |
302 | 301 | anassrs 469 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ ๐ด) โง ยฌ ๐ โ ๐ท) โ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐}))) = (๐โ๐)) |
303 | 289, 302 | pm2.61dan 812 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ด) โ (๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐}))) = (๐โ๐)) |
304 | 303 | fveq2d 6847 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐})))) = (โฏโ(๐โ๐))) |
305 | 304 | oveq1d 7373 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด) โ ((โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โฉ {๐})))) ยท (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) = ((โฏโ(๐โ๐)) ยท (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))))) |
306 | 270, 277,
305 | 3eqtr3d 2785 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ๐ต) = ((โฏโ(๐โ๐)) ยท (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))))) |
307 | 251, 306 | breqtrd 5132 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด) โ ((๐โ(๐ pCnt (โฏโ๐ต))) ยท (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) โฅ ((โฏโ(๐โ๐)) ยท (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))))) |
308 | 113 | nnne0d 12204 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐})))) โ 0) |
309 | | dvdsmulcr 16169 |
. . . . . . . 8
โข (((๐โ(๐ pCnt (โฏโ๐ต))) โ โค โง
(โฏโ(๐โ๐)) โ โค โง
((โฏโ(๐บ DProd
((๐ โพ ๐ท) โพ (๐ท โ {๐})))) โ โค โง
(โฏโ(๐บ DProd
((๐ โพ ๐ท) โพ (๐ท โ {๐})))) โ 0)) โ (((๐โ(๐ pCnt (โฏโ๐ต))) ยท (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) โฅ ((โฏโ(๐โ๐)) ยท (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) โ (๐โ(๐ pCnt (โฏโ๐ต))) โฅ (โฏโ(๐โ๐)))) |
310 | 49, 34, 114, 308, 309 | syl112anc 1375 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด) โ (((๐โ(๐ pCnt (โฏโ๐ต))) ยท (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) โฅ ((โฏโ(๐โ๐)) ยท (โฏโ(๐บ DProd ((๐ โพ ๐ท) โพ (๐ท โ {๐}))))) โ (๐โ(๐ pCnt (โฏโ๐ต))) โฅ (โฏโ(๐โ๐)))) |
311 | 307, 310 | mpbid 231 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ (๐โ(๐ pCnt (โฏโ๐ต))) โฅ (โฏโ(๐โ๐))) |
312 | | dvdseq 16197 |
. . . . . 6
โข
((((โฏโ(๐โ๐)) โ โ0 โง (๐โ(๐ pCnt (โฏโ๐ต))) โ โ0) โง
((โฏโ(๐โ๐)) โฅ (๐โ(๐ pCnt (โฏโ๐ต))) โง (๐โ(๐ pCnt (โฏโ๐ต))) โฅ (โฏโ(๐โ๐)))) โ (โฏโ(๐โ๐)) = (๐โ(๐ pCnt (โฏโ๐ต)))) |
313 | 33, 85, 73, 311, 312 | syl22anc 838 |
. . . . 5
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ(๐โ๐)) = (๐โ(๐ pCnt (โฏโ๐ต)))) |
314 | 6, 7, 8, 9, 10, 11 | ablfac1a 19849 |
. . . . 5
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ(๐โ๐)) = (๐โ(๐ pCnt (โฏโ๐ต)))) |
315 | 313, 314 | eqtr4d 2780 |
. . . 4
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ(๐โ๐)) = (โฏโ(๐โ๐))) |
316 | | hashen 14248 |
. . . . 5
โข (((๐โ๐) โ Fin โง (๐โ๐) โ Fin) โ ((โฏโ(๐โ๐)) = (โฏโ(๐โ๐)) โ (๐โ๐) โ (๐โ๐))) |
317 | 31, 23, 316 | syl2anc 585 |
. . . 4
โข ((๐ โง ๐ โ ๐ด) โ ((โฏโ(๐โ๐)) = (โฏโ(๐โ๐)) โ (๐โ๐) โ (๐โ๐))) |
318 | 315, 317 | mpbid 231 |
. . 3
โข ((๐ โง ๐ โ ๐ด) โ (๐โ๐) โ (๐โ๐)) |
319 | | fisseneq 9202 |
. . 3
โข (((๐โ๐) โ Fin โง (๐โ๐) โ (๐โ๐) โง (๐โ๐) โ (๐โ๐)) โ (๐โ๐) = (๐โ๐)) |
320 | 23, 84, 318, 319 | syl3anc 1372 |
. 2
โข ((๐ โง ๐ โ ๐ด) โ (๐โ๐) = (๐โ๐)) |
321 | 5, 18, 320 | eqfnfvd 6986 |
1
โข (๐ โ ๐ = ๐) |