Step | Hyp | Ref
| Expression |
1 | | sylow2a.y |
. . . . 5
โข (๐ โ ๐ โ Fin) |
2 | | pwfi 8999 |
. . . . 5
โข (๐ โ Fin โ ๐ซ
๐ โ
Fin) |
3 | 1, 2 | sylib 217 |
. . . 4
โข (๐ โ ๐ซ ๐ โ Fin) |
4 | | sylow2a.m |
. . . . . 6
โข (๐ โ โ โ (๐บ GrpAct ๐)) |
5 | | sylow2a.r |
. . . . . . 7
โข โผ =
{โจ๐ฅ, ๐ฆโฉ โฃ ({๐ฅ, ๐ฆ} โ ๐ โง โ๐ โ ๐ (๐ โ ๐ฅ) = ๐ฆ)} |
6 | | sylow2a.x |
. . . . . . 7
โข ๐ = (Baseโ๐บ) |
7 | 5, 6 | gaorber 18963 |
. . . . . 6
โข ( โ โ
(๐บ GrpAct ๐) โ โผ Er ๐) |
8 | 4, 7 | syl 17 |
. . . . 5
โข (๐ โ โผ Er ๐) |
9 | 8 | qsss 8598 |
. . . 4
โข (๐ โ (๐ / โผ ) โ ๐ซ
๐) |
10 | 3, 9 | ssfid 9088 |
. . 3
โข (๐ โ (๐ / โผ ) โ
Fin) |
11 | | diffi 9000 |
. . 3
โข ((๐ / โผ ) โ Fin โ
((๐ / โผ )
โ ๐ซ ๐) โ
Fin) |
12 | 10, 11 | syl 17 |
. 2
โข (๐ โ ((๐ / โผ ) โ ๐ซ
๐) โ
Fin) |
13 | | sylow2a.p |
. . . . 5
โข (๐ โ ๐ pGrp ๐บ) |
14 | | gagrp 18947 |
. . . . . . 7
โข ( โ โ
(๐บ GrpAct ๐) โ ๐บ โ Grp) |
15 | 4, 14 | syl 17 |
. . . . . 6
โข (๐ โ ๐บ โ Grp) |
16 | | sylow2a.f |
. . . . . 6
โข (๐ โ ๐ โ Fin) |
17 | 6 | pgpfi 19259 |
. . . . . 6
โข ((๐บ โ Grp โง ๐ โ Fin) โ (๐ pGrp ๐บ โ (๐ โ โ โง โ๐ โ โ0
(โฏโ๐) = (๐โ๐)))) |
18 | 15, 16, 17 | syl2anc 585 |
. . . . 5
โข (๐ โ (๐ pGrp ๐บ โ (๐ โ โ โง โ๐ โ โ0
(โฏโ๐) = (๐โ๐)))) |
19 | 13, 18 | mpbid 231 |
. . . 4
โข (๐ โ (๐ โ โ โง โ๐ โ โ0
(โฏโ๐) = (๐โ๐))) |
20 | 19 | simpld 496 |
. . 3
โข (๐ โ ๐ โ โ) |
21 | | prmz 16429 |
. . 3
โข (๐ โ โ โ ๐ โ
โค) |
22 | 20, 21 | syl 17 |
. 2
โข (๐ โ ๐ โ โค) |
23 | | eldifi 4067 |
. . . . 5
โข (๐ง โ ((๐ / โผ ) โ ๐ซ
๐) โ ๐ง โ (๐ / โผ )) |
24 | 1 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ง โ (๐ / โผ )) โ ๐ โ Fin) |
25 | 9 | sselda 3926 |
. . . . . . 7
โข ((๐ โง ๐ง โ (๐ / โผ )) โ ๐ง โ ๐ซ ๐) |
26 | 25 | elpwid 4548 |
. . . . . 6
โข ((๐ โง ๐ง โ (๐ / โผ )) โ ๐ง โ ๐) |
27 | 24, 26 | ssfid 9088 |
. . . . 5
โข ((๐ โง ๐ง โ (๐ / โผ )) โ ๐ง โ Fin) |
28 | 23, 27 | sylan2 594 |
. . . 4
โข ((๐ โง ๐ง โ ((๐ / โผ ) โ ๐ซ
๐)) โ ๐ง โ Fin) |
29 | | hashcl 14120 |
. . . 4
โข (๐ง โ Fin โ
(โฏโ๐ง) โ
โ0) |
30 | 28, 29 | syl 17 |
. . 3
โข ((๐ โง ๐ง โ ((๐ / โผ ) โ ๐ซ
๐)) โ
(โฏโ๐ง) โ
โ0) |
31 | 30 | nn0zd 12474 |
. 2
โข ((๐ โง ๐ง โ ((๐ / โผ ) โ ๐ซ
๐)) โ
(โฏโ๐ง) โ
โค) |
32 | | eldif 3902 |
. . 3
โข (๐ง โ ((๐ / โผ ) โ ๐ซ
๐) โ (๐ง โ (๐ / โผ ) โง ยฌ ๐ง โ ๐ซ ๐)) |
33 | | eqid 2736 |
. . . . 5
โข (๐ / โผ ) = (๐ / โผ ) |
34 | | sseq1 3951 |
. . . . . . . 8
โข ([๐ค] โผ = ๐ง โ ([๐ค] โผ โ ๐ โ ๐ง โ ๐)) |
35 | | velpw 4544 |
. . . . . . . 8
โข (๐ง โ ๐ซ ๐ โ ๐ง โ ๐) |
36 | 34, 35 | bitr4di 289 |
. . . . . . 7
โข ([๐ค] โผ = ๐ง โ ([๐ค] โผ โ ๐ โ ๐ง โ ๐ซ ๐)) |
37 | 36 | notbid 318 |
. . . . . 6
โข ([๐ค] โผ = ๐ง โ (ยฌ [๐ค] โผ โ ๐ โ ยฌ ๐ง โ ๐ซ ๐)) |
38 | | fveq2 6804 |
. . . . . . 7
โข ([๐ค] โผ = ๐ง โ (โฏโ[๐ค] โผ ) =
(โฏโ๐ง)) |
39 | 38 | breq2d 5093 |
. . . . . 6
โข ([๐ค] โผ = ๐ง โ (๐ โฅ (โฏโ[๐ค] โผ ) โ ๐ โฅ (โฏโ๐ง))) |
40 | 37, 39 | imbi12d 345 |
. . . . 5
โข ([๐ค] โผ = ๐ง โ ((ยฌ [๐ค] โผ โ ๐ โ ๐ โฅ (โฏโ[๐ค] โผ )) โ (ยฌ
๐ง โ ๐ซ ๐ โ ๐ โฅ (โฏโ๐ง)))) |
41 | 20 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ค โ ๐) โ ๐ โ โ) |
42 | 8 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ค โ ๐) โ โผ Er ๐) |
43 | | simpr 486 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ค โ ๐) โ ๐ค โ ๐) |
44 | 42, 43 | erref 8549 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ค โ ๐) โ ๐ค โผ ๐ค) |
45 | | vex 3441 |
. . . . . . . . . . . . . 14
โข ๐ค โ V |
46 | 45, 45 | elec 8573 |
. . . . . . . . . . . . 13
โข (๐ค โ [๐ค] โผ โ ๐ค โผ ๐ค) |
47 | 44, 46 | sylibr 233 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ค โ ๐) โ ๐ค โ [๐ค] โผ ) |
48 | 47 | ne0d 4275 |
. . . . . . . . . . 11
โข ((๐ โง ๐ค โ ๐) โ [๐ค] โผ โ
โ
) |
49 | 8 | ecss 8575 |
. . . . . . . . . . . . . 14
โข (๐ โ [๐ค] โผ โ ๐) |
50 | 1, 49 | ssfid 9088 |
. . . . . . . . . . . . 13
โข (๐ โ [๐ค] โผ โ
Fin) |
51 | 50 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ค โ ๐) โ [๐ค] โผ โ
Fin) |
52 | | hashnncl 14130 |
. . . . . . . . . . . 12
โข ([๐ค] โผ โ Fin โ
((โฏโ[๐ค] โผ )
โ โ โ [๐ค]
โผ
โ โ
)) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โง ๐ค โ ๐) โ ((โฏโ[๐ค] โผ ) โ โ
โ [๐ค] โผ โ
โ
)) |
54 | 48, 53 | mpbird 257 |
. . . . . . . . . 10
โข ((๐ โง ๐ค โ ๐) โ (โฏโ[๐ค] โผ ) โ
โ) |
55 | | pceq0 16621 |
. . . . . . . . . 10
โข ((๐ โ โ โง
(โฏโ[๐ค] โผ )
โ โ) โ ((๐
pCnt (โฏโ[๐ค]
โผ
)) = 0 โ ยฌ ๐
โฅ (โฏโ[๐ค]
โผ
))) |
56 | 41, 54, 55 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ โง ๐ค โ ๐) โ ((๐ pCnt (โฏโ[๐ค] โผ )) = 0 โ ยฌ
๐ โฅ
(โฏโ[๐ค] โผ
))) |
57 | | oveq2 7315 |
. . . . . . . . . 10
โข ((๐ pCnt (โฏโ[๐ค] โผ )) = 0 โ
(๐โ(๐ pCnt (โฏโ[๐ค] โผ ))) = (๐โ0)) |
58 | | hashcl 14120 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ([๐ค] โผ โ Fin โ
(โฏโ[๐ค] โผ )
โ โ0) |
59 | 50, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (โฏโ[๐ค] โผ ) โ
โ0) |
60 | 59 | nn0zd 12474 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (โฏโ[๐ค] โผ ) โ
โค) |
61 | | ssrab2 4019 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข {๐ฃ โ ๐ โฃ (๐ฃ โ ๐ค) = ๐ค} โ ๐ |
62 | | ssfi 8994 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ Fin โง {๐ฃ โ ๐ โฃ (๐ฃ โ ๐ค) = ๐ค} โ ๐) โ {๐ฃ โ ๐ โฃ (๐ฃ โ ๐ค) = ๐ค} โ Fin) |
63 | 16, 61, 62 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ {๐ฃ โ ๐ โฃ (๐ฃ โ ๐ค) = ๐ค} โ Fin) |
64 | | hashcl 14120 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ({๐ฃ โ ๐ โฃ (๐ฃ โ ๐ค) = ๐ค} โ Fin โ (โฏโ{๐ฃ โ ๐ โฃ (๐ฃ โ ๐ค) = ๐ค}) โ
โ0) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (โฏโ{๐ฃ โ ๐ โฃ (๐ฃ โ ๐ค) = ๐ค}) โ
โ0) |
66 | 65 | nn0zd 12474 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (โฏโ{๐ฃ โ ๐ โฃ (๐ฃ โ ๐ค) = ๐ค}) โ โค) |
67 | | dvdsmul1 16036 |
. . . . . . . . . . . . . . . . . . . 20
โข
(((โฏโ[๐ค]
โผ
) โ โค โง (โฏโ{๐ฃ โ ๐ โฃ (๐ฃ โ ๐ค) = ๐ค}) โ โค) โ
(โฏโ[๐ค] โผ )
โฅ ((โฏโ[๐ค]
โผ
) ยท (โฏโ{๐ฃ โ ๐ โฃ (๐ฃ โ ๐ค) = ๐ค}))) |
68 | 60, 66, 67 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (โฏโ[๐ค] โผ ) โฅ
((โฏโ[๐ค] โผ )
ยท (โฏโ{๐ฃ
โ ๐ โฃ (๐ฃ โ ๐ค) = ๐ค}))) |
69 | 68 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ค โ ๐) โ (โฏโ[๐ค] โผ ) โฅ
((โฏโ[๐ค] โผ )
ยท (โฏโ{๐ฃ
โ ๐ โฃ (๐ฃ โ ๐ค) = ๐ค}))) |
70 | 4 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ค โ ๐) โ โ โ (๐บ GrpAct ๐)) |
71 | 16 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ค โ ๐) โ ๐ โ Fin) |
72 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . . 20
โข {๐ฃ โ ๐ โฃ (๐ฃ โ ๐ค) = ๐ค} = {๐ฃ โ ๐ โฃ (๐ฃ โ ๐ค) = ๐ค} |
73 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐บ ~QG {๐ฃ โ ๐ โฃ (๐ฃ โ ๐ค) = ๐ค}) = (๐บ ~QG {๐ฃ โ ๐ โฃ (๐ฃ โ ๐ค) = ๐ค}) |
74 | 6, 72, 73, 5 | orbsta2 18969 |
. . . . . . . . . . . . . . . . . . 19
โข ((( โ โ
(๐บ GrpAct ๐) โง ๐ค โ ๐) โง ๐ โ Fin) โ (โฏโ๐) = ((โฏโ[๐ค] โผ ) ยท
(โฏโ{๐ฃ โ
๐ โฃ (๐ฃ โ ๐ค) = ๐ค}))) |
75 | 70, 43, 71, 74 | syl21anc 836 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ค โ ๐) โ (โฏโ๐) = ((โฏโ[๐ค] โผ ) ยท
(โฏโ{๐ฃ โ
๐ โฃ (๐ฃ โ ๐ค) = ๐ค}))) |
76 | 69, 75 | breqtrrd 5109 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ค โ ๐) โ (โฏโ[๐ค] โผ ) โฅ
(โฏโ๐)) |
77 | 19 | simprd 497 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ๐ โ โ0
(โฏโ๐) = (๐โ๐)) |
78 | 77 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ค โ ๐) โ โ๐ โ โ0
(โฏโ๐) = (๐โ๐)) |
79 | | breq2 5085 |
. . . . . . . . . . . . . . . . . . 19
โข
((โฏโ๐) =
(๐โ๐) โ ((โฏโ[๐ค] โผ ) โฅ
(โฏโ๐) โ
(โฏโ[๐ค] โผ )
โฅ (๐โ๐))) |
80 | 79 | biimpcd 249 |
. . . . . . . . . . . . . . . . . 18
โข
((โฏโ[๐ค]
โผ
) โฅ (โฏโ๐)
โ ((โฏโ๐) =
(๐โ๐) โ (โฏโ[๐ค] โผ ) โฅ (๐โ๐))) |
81 | 80 | reximdv 3164 |
. . . . . . . . . . . . . . . . 17
โข
((โฏโ[๐ค]
โผ
) โฅ (โฏโ๐)
โ (โ๐ โ
โ0 (โฏโ๐) = (๐โ๐) โ โ๐ โ โ0
(โฏโ[๐ค] โผ )
โฅ (๐โ๐))) |
82 | 76, 78, 81 | sylc 65 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐) โ โ๐ โ โ0
(โฏโ[๐ค] โผ )
โฅ (๐โ๐)) |
83 | | pcprmpw2 16632 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง
(โฏโ[๐ค] โผ )
โ โ) โ (โ๐ โ โ0
(โฏโ[๐ค] โผ )
โฅ (๐โ๐) โ (โฏโ[๐ค] โผ ) = (๐โ(๐ pCnt (โฏโ[๐ค] โผ
))))) |
84 | 41, 54, 83 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐) โ (โ๐ โ โ0
(โฏโ[๐ค] โผ )
โฅ (๐โ๐) โ (โฏโ[๐ค] โผ ) = (๐โ(๐ pCnt (โฏโ[๐ค] โผ
))))) |
85 | 82, 84 | mpbid 231 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ค โ ๐) โ (โฏโ[๐ค] โผ ) = (๐โ(๐ pCnt (โฏโ[๐ค] โผ
)))) |
86 | 85 | eqcomd 2742 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ค โ ๐) โ (๐โ(๐ pCnt (โฏโ[๐ค] โผ ))) =
(โฏโ[๐ค] โผ
)) |
87 | 22 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ค โ ๐) โ ๐ โ โค) |
88 | 87 | zcnd 12477 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐) โ ๐ โ โ) |
89 | 88 | exp0d 13908 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ค โ ๐) โ (๐โ0) = 1) |
90 | | hash1 14168 |
. . . . . . . . . . . . . . 15
โข
(โฏโ1o) = 1 |
91 | 89, 90 | eqtr4di 2794 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ค โ ๐) โ (๐โ0) =
(โฏโ1o)) |
92 | 86, 91 | eqeq12d 2752 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ค โ ๐) โ ((๐โ(๐ pCnt (โฏโ[๐ค] โผ ))) = (๐โ0) โ
(โฏโ[๐ค] โผ ) =
(โฏโ1o))) |
93 | | df1o2 8335 |
. . . . . . . . . . . . . . 15
โข
1o = {โ
} |
94 | | snfi 8869 |
. . . . . . . . . . . . . . 15
โข {โ
}
โ Fin |
95 | 93, 94 | eqeltri 2833 |
. . . . . . . . . . . . . 14
โข
1o โ Fin |
96 | | hashen 14111 |
. . . . . . . . . . . . . 14
โข (([๐ค] โผ โ Fin โง
1o โ Fin) โ ((โฏโ[๐ค] โผ ) =
(โฏโ1o) โ [๐ค] โผ โ
1o)) |
97 | 51, 95, 96 | sylancl 587 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ค โ ๐) โ ((โฏโ[๐ค] โผ ) =
(โฏโ1o) โ [๐ค] โผ โ
1o)) |
98 | 92, 97 | bitrd 279 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ค โ ๐) โ ((๐โ(๐ pCnt (โฏโ[๐ค] โผ ))) = (๐โ0) โ [๐ค] โผ โ
1o)) |
99 | | en1b 8848 |
. . . . . . . . . . . 12
โข ([๐ค] โผ โ
1o โ [๐ค]
โผ
= {โช [๐ค] โผ }) |
100 | 98, 99 | bitrdi 287 |
. . . . . . . . . . 11
โข ((๐ โง ๐ค โ ๐) โ ((๐โ(๐ pCnt (โฏโ[๐ค] โผ ))) = (๐โ0) โ [๐ค] โผ = {โช [๐ค]
โผ
})) |
101 | 43 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ค โ ๐) โง (โ โ ๐ โง [๐ค] โผ = {โช [๐ค]
โผ
})) โ ๐ค โ ๐) |
102 | 4 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ค โ ๐) โง (โ โ ๐ โง [๐ค] โผ = {โช [๐ค]
โผ
})) โ โ โ (๐บ GrpAct ๐)) |
103 | 6 | gaf 18950 |
. . . . . . . . . . . . . . . . . . . 20
โข ( โ โ
(๐บ GrpAct ๐) โ โ :(๐ ร ๐)โถ๐) |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ค โ ๐) โง (โ โ ๐ โง [๐ค] โผ = {โช [๐ค]
โผ
})) โ โ :(๐ ร ๐)โถ๐) |
105 | | simprl 769 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ค โ ๐) โง (โ โ ๐ โง [๐ค] โผ = {โช [๐ค]
โผ
})) โ โ โ ๐) |
106 | 104, 105,
101 | fovcdmd 7476 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ค โ ๐) โง (โ โ ๐ โง [๐ค] โผ = {โช [๐ค]
โผ
})) โ (โ โ ๐ค) โ ๐) |
107 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . 19
โข (โ โ ๐ค) = (โ โ ๐ค) |
108 | | oveq1 7314 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = โ โ (๐ โ ๐ค) = (โ โ ๐ค)) |
109 | 108 | eqeq1d 2738 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = โ โ ((๐ โ ๐ค) = (โ โ ๐ค) โ (โ โ ๐ค) = (โ โ ๐ค))) |
110 | 109 | rspcev 3566 |
. . . . . . . . . . . . . . . . . . 19
โข ((โ โ ๐ โง (โ โ ๐ค) = (โ โ ๐ค)) โ โ๐ โ ๐ (๐ โ ๐ค) = (โ โ ๐ค)) |
111 | 105, 107,
110 | sylancl 587 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ค โ ๐) โง (โ โ ๐ โง [๐ค] โผ = {โช [๐ค]
โผ
})) โ โ๐ โ
๐ (๐ โ ๐ค) = (โ โ ๐ค)) |
112 | 5 | gaorb 18962 |
. . . . . . . . . . . . . . . . . 18
โข (๐ค โผ (โ โ ๐ค) โ (๐ค โ ๐ โง (โ โ ๐ค) โ ๐ โง โ๐ โ ๐ (๐ โ ๐ค) = (โ โ ๐ค))) |
113 | 101, 106,
111, 112 | syl3anbrc 1343 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ค โ ๐) โง (โ โ ๐ โง [๐ค] โผ = {โช [๐ค]
โผ
})) โ ๐ค โผ (โ โ ๐ค)) |
114 | | ovex 7340 |
. . . . . . . . . . . . . . . . . 18
โข (โ โ ๐ค) โ V |
115 | 114, 45 | elec 8573 |
. . . . . . . . . . . . . . . . 17
โข ((โ โ ๐ค) โ [๐ค] โผ โ ๐ค โผ (โ โ ๐ค)) |
116 | 113, 115 | sylibr 233 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ค โ ๐) โง (โ โ ๐ โง [๐ค] โผ = {โช [๐ค]
โผ
})) โ (โ โ ๐ค) โ [๐ค] โผ ) |
117 | | simprr 771 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ค โ ๐) โง (โ โ ๐ โง [๐ค] โผ = {โช [๐ค]
โผ
})) โ [๐ค] โผ =
{โช [๐ค] โผ }) |
118 | 116, 117 | eleqtrd 2839 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ค โ ๐) โง (โ โ ๐ โง [๐ค] โผ = {โช [๐ค]
โผ
})) โ (โ โ ๐ค) โ {โช [๐ค]
โผ
}) |
119 | 114 | elsn 4580 |
. . . . . . . . . . . . . . 15
โข ((โ โ ๐ค) โ {โช [๐ค] โผ } โ (โ โ ๐ค) = โช [๐ค] โผ ) |
120 | 118, 119 | sylib 217 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ค โ ๐) โง (โ โ ๐ โง [๐ค] โผ = {โช [๐ค]
โผ
})) โ (โ โ ๐ค) = โช
[๐ค] โผ ) |
121 | 47 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ค โ ๐) โง (โ โ ๐ โง [๐ค] โผ = {โช [๐ค]
โผ
})) โ ๐ค โ [๐ค] โผ ) |
122 | 121, 117 | eleqtrd 2839 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ค โ ๐) โง (โ โ ๐ โง [๐ค] โผ = {โช [๐ค]
โผ
})) โ ๐ค โ {โช [๐ค]
โผ
}) |
123 | 45 | elsn 4580 |
. . . . . . . . . . . . . . 15
โข (๐ค โ {โช [๐ค]
โผ
} โ ๐ค = โช [๐ค]
โผ
) |
124 | 122, 123 | sylib 217 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ค โ ๐) โง (โ โ ๐ โง [๐ค] โผ = {โช [๐ค]
โผ
})) โ ๐ค = โช [๐ค]
โผ
) |
125 | 120, 124 | eqtr4d 2779 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ค โ ๐) โง (โ โ ๐ โง [๐ค] โผ = {โช [๐ค]
โผ
})) โ (โ โ ๐ค) = ๐ค) |
126 | 125 | expr 458 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ค โ ๐) โง โ โ ๐) โ ([๐ค] โผ = {โช [๐ค]
โผ
} โ (โ โ ๐ค) = ๐ค)) |
127 | 126 | ralrimdva 3148 |
. . . . . . . . . . 11
โข ((๐ โง ๐ค โ ๐) โ ([๐ค] โผ = {โช [๐ค]
โผ
} โ โโ โ
๐ (โ โ ๐ค) = ๐ค)) |
128 | 100, 127 | sylbid 239 |
. . . . . . . . . 10
โข ((๐ โง ๐ค โ ๐) โ ((๐โ(๐ pCnt (โฏโ[๐ค] โผ ))) = (๐โ0) โ โโ โ ๐ (โ โ ๐ค) = ๐ค)) |
129 | 57, 128 | syl5 34 |
. . . . . . . . 9
โข ((๐ โง ๐ค โ ๐) โ ((๐ pCnt (โฏโ[๐ค] โผ )) = 0 โ
โโ โ ๐ (โ โ ๐ค) = ๐ค)) |
130 | 56, 129 | sylbird 260 |
. . . . . . . 8
โข ((๐ โง ๐ค โ ๐) โ (ยฌ ๐ โฅ (โฏโ[๐ค] โผ ) โ
โโ โ ๐ (โ โ ๐ค) = ๐ค)) |
131 | | oveq2 7315 |
. . . . . . . . . . . . 13
โข (๐ข = ๐ค โ (โ โ ๐ข) = (โ โ ๐ค)) |
132 | | id 22 |
. . . . . . . . . . . . 13
โข (๐ข = ๐ค โ ๐ข = ๐ค) |
133 | 131, 132 | eqeq12d 2752 |
. . . . . . . . . . . 12
โข (๐ข = ๐ค โ ((โ โ ๐ข) = ๐ข โ (โ โ ๐ค) = ๐ค)) |
134 | 133 | ralbidv 3171 |
. . . . . . . . . . 11
โข (๐ข = ๐ค โ (โโ โ ๐ (โ โ ๐ข) = ๐ข โ โโ โ ๐ (โ โ ๐ค) = ๐ค)) |
135 | | sylow2a.z |
. . . . . . . . . . 11
โข ๐ = {๐ข โ ๐ โฃ โโ โ ๐ (โ โ ๐ข) = ๐ข} |
136 | 134, 135 | elrab2 3632 |
. . . . . . . . . 10
โข (๐ค โ ๐ โ (๐ค โ ๐ โง โโ โ ๐ (โ โ ๐ค) = ๐ค)) |
137 | 136 | baib 537 |
. . . . . . . . 9
โข (๐ค โ ๐ โ (๐ค โ ๐ โ โโ โ ๐ (โ โ ๐ค) = ๐ค)) |
138 | 137 | adantl 483 |
. . . . . . . 8
โข ((๐ โง ๐ค โ ๐) โ (๐ค โ ๐ โ โโ โ ๐ (โ โ ๐ค) = ๐ค)) |
139 | 130, 138 | sylibrd 259 |
. . . . . . 7
โข ((๐ โง ๐ค โ ๐) โ (ยฌ ๐ โฅ (โฏโ[๐ค] โผ ) โ ๐ค โ ๐)) |
140 | 6, 4, 13, 16, 1, 135, 5 | sylow2alem1 19271 |
. . . . . . . . . 10
โข ((๐ โง ๐ค โ ๐) โ [๐ค] โผ = {๐ค}) |
141 | | simpr 486 |
. . . . . . . . . . 11
โข ((๐ โง ๐ค โ ๐) โ ๐ค โ ๐) |
142 | 141 | snssd 4748 |
. . . . . . . . . 10
โข ((๐ โง ๐ค โ ๐) โ {๐ค} โ ๐) |
143 | 140, 142 | eqsstrd 3964 |
. . . . . . . . 9
โข ((๐ โง ๐ค โ ๐) โ [๐ค] โผ โ ๐) |
144 | 143 | ex 414 |
. . . . . . . 8
โข (๐ โ (๐ค โ ๐ โ [๐ค] โผ โ ๐)) |
145 | 144 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ค โ ๐) โ (๐ค โ ๐ โ [๐ค] โผ โ ๐)) |
146 | 139, 145 | syld 47 |
. . . . . 6
โข ((๐ โง ๐ค โ ๐) โ (ยฌ ๐ โฅ (โฏโ[๐ค] โผ ) โ [๐ค] โผ โ ๐)) |
147 | 146 | con1d 145 |
. . . . 5
โข ((๐ โง ๐ค โ ๐) โ (ยฌ [๐ค] โผ โ ๐ โ ๐ โฅ (โฏโ[๐ค] โผ
))) |
148 | 33, 40, 147 | ectocld 8604 |
. . . 4
โข ((๐ โง ๐ง โ (๐ / โผ )) โ (ยฌ
๐ง โ ๐ซ ๐ โ ๐ โฅ (โฏโ๐ง))) |
149 | 148 | impr 456 |
. . 3
โข ((๐ โง (๐ง โ (๐ / โผ ) โง ยฌ ๐ง โ ๐ซ ๐)) โ ๐ โฅ (โฏโ๐ง)) |
150 | 32, 149 | sylan2b 595 |
. 2
โข ((๐ โง ๐ง โ ((๐ / โผ ) โ ๐ซ
๐)) โ ๐ โฅ (โฏโ๐ง)) |
151 | 12, 22, 31, 150 | fsumdvds 16066 |
1
โข (๐ โ ๐ โฅ ฮฃ๐ง โ ((๐ / โผ ) โ ๐ซ
๐)(โฏโ๐ง)) |