Step | Hyp | Ref
| Expression |
1 | | sylow2blem3.hp |
. . . . . . . . 9
โข (๐ โ ๐ pGrp (๐บ โพs ๐ป)) |
2 | | pgpprm 19380 |
. . . . . . . . 9
โข (๐ pGrp (๐บ โพs ๐ป) โ ๐ โ โ) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
4 | | sylow2b.h |
. . . . . . . . . . 11
โข (๐ โ ๐ป โ (SubGrpโ๐บ)) |
5 | | subgrcl 18938 |
. . . . . . . . . . 11
โข (๐ป โ (SubGrpโ๐บ) โ ๐บ โ Grp) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ๐บ โ Grp) |
7 | | sylow2b.x |
. . . . . . . . . . 11
โข ๐ = (Baseโ๐บ) |
8 | 7 | grpbn0 18784 |
. . . . . . . . . 10
โข (๐บ โ Grp โ ๐ โ โ
) |
9 | 6, 8 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ
) |
10 | | sylow2b.xf |
. . . . . . . . . 10
โข (๐ โ ๐ โ Fin) |
11 | | hashnncl 14272 |
. . . . . . . . . 10
โข (๐ โ Fin โ
((โฏโ๐) โ
โ โ ๐ โ
โ
)) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
โข (๐ โ ((โฏโ๐) โ โ โ ๐ โ โ
)) |
13 | 9, 12 | mpbird 257 |
. . . . . . . 8
โข (๐ โ (โฏโ๐) โ
โ) |
14 | | pcndvds2 16745 |
. . . . . . . 8
โข ((๐ โ โ โง
(โฏโ๐) โ
โ) โ ยฌ ๐
โฅ ((โฏโ๐)
/ (๐โ(๐ pCnt (โฏโ๐))))) |
15 | 3, 13, 14 | syl2anc 585 |
. . . . . . 7
โข (๐ โ ยฌ ๐ โฅ ((โฏโ๐) / (๐โ(๐ pCnt (โฏโ๐))))) |
16 | | sylow2b.r |
. . . . . . . . . . 11
โข โผ =
(๐บ ~QG
๐พ) |
17 | | sylow2b.k |
. . . . . . . . . . 11
โข (๐ โ ๐พ โ (SubGrpโ๐บ)) |
18 | 7, 16, 17, 10 | lagsubg2 18996 |
. . . . . . . . . 10
โข (๐ โ (โฏโ๐) = ((โฏโ(๐ / โผ )) ยท
(โฏโ๐พ))) |
19 | 18 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ โ ((โฏโ๐) / (โฏโ๐พ)) = (((โฏโ(๐ / โผ )) ยท
(โฏโ๐พ)) /
(โฏโ๐พ))) |
20 | | sylow2blem3.kn |
. . . . . . . . . 10
โข (๐ โ (โฏโ๐พ) = (๐โ(๐ pCnt (โฏโ๐)))) |
21 | 20 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ โ ((โฏโ๐) / (โฏโ๐พ)) = ((โฏโ๐) / (๐โ(๐ pCnt (โฏโ๐))))) |
22 | | pwfi 9125 |
. . . . . . . . . . . . . 14
โข (๐ โ Fin โ ๐ซ
๐ โ
Fin) |
23 | 10, 22 | sylib 217 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ซ ๐ โ Fin) |
24 | 7, 16 | eqger 18985 |
. . . . . . . . . . . . . . 15
โข (๐พ โ (SubGrpโ๐บ) โ โผ Er ๐) |
25 | 17, 24 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ โผ Er ๐) |
26 | 25 | qsss 8720 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ / โผ ) โ ๐ซ
๐) |
27 | 23, 26 | ssfid 9214 |
. . . . . . . . . . . 12
โข (๐ โ (๐ / โผ ) โ
Fin) |
28 | | hashcl 14262 |
. . . . . . . . . . . 12
โข ((๐ / โผ ) โ Fin โ
(โฏโ(๐ /
โผ
)) โ โ0) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (โฏโ(๐ / โผ )) โ
โ0) |
30 | 29 | nn0cnd 12480 |
. . . . . . . . . 10
โข (๐ โ (โฏโ(๐ / โผ )) โ
โ) |
31 | | eqid 2733 |
. . . . . . . . . . . . . . 15
โข
(0gโ๐บ) = (0gโ๐บ) |
32 | 31 | subg0cl 18941 |
. . . . . . . . . . . . . 14
โข (๐พ โ (SubGrpโ๐บ) โ
(0gโ๐บ)
โ ๐พ) |
33 | 17, 32 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (0gโ๐บ) โ ๐พ) |
34 | 33 | ne0d 4296 |
. . . . . . . . . . . 12
โข (๐ โ ๐พ โ โ
) |
35 | 7 | subgss 18934 |
. . . . . . . . . . . . . . 15
โข (๐พ โ (SubGrpโ๐บ) โ ๐พ โ ๐) |
36 | 17, 35 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐พ โ ๐) |
37 | 10, 36 | ssfid 9214 |
. . . . . . . . . . . . 13
โข (๐ โ ๐พ โ Fin) |
38 | | hashnncl 14272 |
. . . . . . . . . . . . 13
โข (๐พ โ Fin โ
((โฏโ๐พ) โ
โ โ ๐พ โ
โ
)) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ ((โฏโ๐พ) โ โ โ ๐พ โ โ
)) |
40 | 34, 39 | mpbird 257 |
. . . . . . . . . . 11
โข (๐ โ (โฏโ๐พ) โ
โ) |
41 | 40 | nncnd 12174 |
. . . . . . . . . 10
โข (๐ โ (โฏโ๐พ) โ
โ) |
42 | 40 | nnne0d 12208 |
. . . . . . . . . 10
โข (๐ โ (โฏโ๐พ) โ 0) |
43 | 30, 41, 42 | divcan4d 11942 |
. . . . . . . . 9
โข (๐ โ (((โฏโ(๐ / โผ )) ยท
(โฏโ๐พ)) /
(โฏโ๐พ)) =
(โฏโ(๐ /
โผ
))) |
44 | 19, 21, 43 | 3eqtr3d 2781 |
. . . . . . . 8
โข (๐ โ ((โฏโ๐) / (๐โ(๐ pCnt (โฏโ๐)))) = (โฏโ(๐ / โผ
))) |
45 | 44 | breq2d 5118 |
. . . . . . 7
โข (๐ โ (๐ โฅ ((โฏโ๐) / (๐โ(๐ pCnt (โฏโ๐)))) โ ๐ โฅ (โฏโ(๐ / โผ
)))) |
46 | 15, 45 | mtbid 324 |
. . . . . 6
โข (๐ โ ยฌ ๐ โฅ (โฏโ(๐ / โผ
))) |
47 | | prmz 16556 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โค) |
48 | 3, 47 | syl 17 |
. . . . . . 7
โข (๐ โ ๐ โ โค) |
49 | 29 | nn0zd 12530 |
. . . . . . 7
โข (๐ โ (โฏโ(๐ / โผ )) โ
โค) |
50 | | ssrab2 4038 |
. . . . . . . . . 10
โข {๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง} โ (๐ / โผ ) |
51 | | ssfi 9120 |
. . . . . . . . . 10
โข (((๐ / โผ ) โ Fin โง
{๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง} โ (๐ / โผ )) โ {๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง} โ Fin) |
52 | 27, 50, 51 | sylancl 587 |
. . . . . . . . 9
โข (๐ โ {๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง} โ Fin) |
53 | | hashcl 14262 |
. . . . . . . . 9
โข ({๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง} โ Fin โ (โฏโ{๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง}) โ
โ0) |
54 | 52, 53 | syl 17 |
. . . . . . . 8
โข (๐ โ (โฏโ{๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง}) โ
โ0) |
55 | 54 | nn0zd 12530 |
. . . . . . 7
โข (๐ โ (โฏโ{๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง}) โ โค) |
56 | | eqid 2733 |
. . . . . . . 8
โข
(Baseโ(๐บ
โพs ๐ป)) =
(Baseโ(๐บ
โพs ๐ป)) |
57 | | sylow2b.a |
. . . . . . . . 9
โข + =
(+gโ๐บ) |
58 | | sylow2b.m |
. . . . . . . . 9
โข ยท =
(๐ฅ โ ๐ป, ๐ฆ โ (๐ / โผ ) โฆ ran
(๐ง โ ๐ฆ โฆ (๐ฅ + ๐ง))) |
59 | 7, 10, 4, 17, 57, 16, 58 | sylow2blem2 19408 |
. . . . . . . 8
โข (๐ โ ยท โ ((๐บ โพs ๐ป) GrpAct (๐ / โผ
))) |
60 | | eqid 2733 |
. . . . . . . . . . 11
โข (๐บ โพs ๐ป) = (๐บ โพs ๐ป) |
61 | 60 | subgbas 18937 |
. . . . . . . . . 10
โข (๐ป โ (SubGrpโ๐บ) โ ๐ป = (Baseโ(๐บ โพs ๐ป))) |
62 | 4, 61 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐ป = (Baseโ(๐บ โพs ๐ป))) |
63 | 7 | subgss 18934 |
. . . . . . . . . . 11
โข (๐ป โ (SubGrpโ๐บ) โ ๐ป โ ๐) |
64 | 4, 63 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ๐ป โ ๐) |
65 | 10, 64 | ssfid 9214 |
. . . . . . . . 9
โข (๐ โ ๐ป โ Fin) |
66 | 62, 65 | eqeltrrd 2835 |
. . . . . . . 8
โข (๐ โ (Baseโ(๐บ โพs ๐ป)) โ Fin) |
67 | | eqid 2733 |
. . . . . . . 8
โข {๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง} = {๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง} |
68 | | eqid 2733 |
. . . . . . . 8
โข
{โจ๐ฅ, ๐ฆโฉ โฃ ({๐ฅ, ๐ฆ} โ (๐ / โผ ) โง
โ๐ โ
(Baseโ(๐บ
โพs ๐ป))(๐ ยท ๐ฅ) = ๐ฆ)} = {โจ๐ฅ, ๐ฆโฉ โฃ ({๐ฅ, ๐ฆ} โ (๐ / โผ ) โง
โ๐ โ
(Baseโ(๐บ
โพs ๐ป))(๐ ยท ๐ฅ) = ๐ฆ)} |
69 | 56, 59, 1, 66, 27, 67, 68 | sylow2a 19406 |
. . . . . . 7
โข (๐ โ ๐ โฅ ((โฏโ(๐ / โผ )) โ
(โฏโ{๐ง โ
(๐ / โผ )
โฃ โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง}))) |
70 | | dvdssub2 16188 |
. . . . . . 7
โข (((๐ โ โค โง
(โฏโ(๐ /
โผ
)) โ โค โง (โฏโ{๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง}) โ โค) โง ๐ โฅ ((โฏโ(๐ / โผ )) โ
(โฏโ{๐ง โ
(๐ / โผ )
โฃ โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง}))) โ (๐ โฅ (โฏโ(๐ / โผ )) โ ๐ โฅ (โฏโ{๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง}))) |
71 | 48, 49, 55, 69, 70 | syl31anc 1374 |
. . . . . 6
โข (๐ โ (๐ โฅ (โฏโ(๐ / โผ )) โ ๐ โฅ (โฏโ{๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง}))) |
72 | 46, 71 | mtbid 324 |
. . . . 5
โข (๐ โ ยฌ ๐ โฅ (โฏโ{๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง})) |
73 | | hasheq0 14269 |
. . . . . . . 8
โข ({๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง} โ Fin โ ((โฏโ{๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง}) = 0 โ {๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง} = โ
)) |
74 | 52, 73 | syl 17 |
. . . . . . 7
โข (๐ โ ((โฏโ{๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง}) = 0 โ {๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง} = โ
)) |
75 | | dvds0 16159 |
. . . . . . . . 9
โข (๐ โ โค โ ๐ โฅ 0) |
76 | 48, 75 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐ โฅ 0) |
77 | | breq2 5110 |
. . . . . . . 8
โข
((โฏโ{๐ง
โ (๐ / โผ )
โฃ โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง}) = 0 โ (๐ โฅ (โฏโ{๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง}) โ ๐ โฅ 0)) |
78 | 76, 77 | syl5ibrcom 247 |
. . . . . . 7
โข (๐ โ ((โฏโ{๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง}) = 0 โ ๐ โฅ (โฏโ{๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง}))) |
79 | 74, 78 | sylbird 260 |
. . . . . 6
โข (๐ โ ({๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง} = โ
โ ๐ โฅ (โฏโ{๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง}))) |
80 | 79 | necon3bd 2954 |
. . . . 5
โข (๐ โ (ยฌ ๐ โฅ (โฏโ{๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง}) โ {๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง} โ โ
)) |
81 | 72, 80 | mpd 15 |
. . . 4
โข (๐ โ {๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง} โ โ
) |
82 | | rabn0 4346 |
. . . 4
โข ({๐ง โ (๐ / โผ ) โฃ
โ๐ข โ
(Baseโ(๐บ
โพs ๐ป))(๐ข ยท ๐ง) = ๐ง} โ โ
โ โ๐ง โ (๐ / โผ )โ๐ข โ (Baseโ(๐บ โพs ๐ป))(๐ข ยท ๐ง) = ๐ง) |
83 | 81, 82 | sylib 217 |
. . 3
โข (๐ โ โ๐ง โ (๐ / โผ )โ๐ข โ (Baseโ(๐บ โพs ๐ป))(๐ข ยท ๐ง) = ๐ง) |
84 | 62 | raleqdv 3312 |
. . . 4
โข (๐ โ (โ๐ข โ ๐ป (๐ข ยท ๐ง) = ๐ง โ โ๐ข โ (Baseโ(๐บ โพs ๐ป))(๐ข ยท ๐ง) = ๐ง)) |
85 | 84 | rexbidv 3172 |
. . 3
โข (๐ โ (โ๐ง โ (๐ / โผ )โ๐ข โ ๐ป (๐ข ยท ๐ง) = ๐ง โ โ๐ง โ (๐ / โผ )โ๐ข โ (Baseโ(๐บ โพs ๐ป))(๐ข ยท ๐ง) = ๐ง)) |
86 | 83, 85 | mpbird 257 |
. 2
โข (๐ โ โ๐ง โ (๐ / โผ )โ๐ข โ ๐ป (๐ข ยท ๐ง) = ๐ง) |
87 | | vex 3448 |
. . . . 5
โข ๐ง โ V |
88 | 87 | elqs 8711 |
. . . 4
โข (๐ง โ (๐ / โผ ) โ
โ๐ โ ๐ ๐ง = [๐] โผ ) |
89 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ ๐ง = [๐] โผ ) |
90 | 89 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ (๐ข ยท ๐ง) = (๐ข ยท [๐] โผ )) |
91 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ (๐ข ยท ๐ง) = ๐ง) |
92 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ ๐) |
93 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ ๐ข โ ๐ป) |
94 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ ๐ โ ๐) |
95 | 7, 10, 4, 17, 57, 16, 58 | sylow2blem1 19407 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ข โ ๐ป โง ๐ โ ๐) โ (๐ข ยท [๐] โผ ) = [(๐ข + ๐)] โผ ) |
96 | 92, 93, 94, 95 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ (๐ข ยท [๐] โผ ) = [(๐ข + ๐)] โผ ) |
97 | 90, 91, 96 | 3eqtr3d 2781 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ ๐ง = [(๐ข + ๐)] โผ ) |
98 | 89, 97 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ [๐] โผ = [(๐ข + ๐)] โผ ) |
99 | 25 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ โผ Er ๐) |
100 | 99, 94 | erth 8700 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ (๐ โผ (๐ข + ๐) โ [๐] โผ = [(๐ข + ๐)] โผ )) |
101 | 98, 100 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ ๐ โผ (๐ข + ๐)) |
102 | 6 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ ๐บ โ Grp) |
103 | 36 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ ๐พ โ ๐) |
104 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . 20
โข
(invgโ๐บ) = (invgโ๐บ) |
105 | 7, 104, 57, 16 | eqgval 18984 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐บ โ Grp โง ๐พ โ ๐) โ (๐ โผ (๐ข + ๐) โ (๐ โ ๐ โง (๐ข + ๐) โ ๐ โง (((invgโ๐บ)โ๐) + (๐ข + ๐)) โ ๐พ))) |
106 | 102, 103,
105 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ (๐ โผ (๐ข + ๐) โ (๐ โ ๐ โง (๐ข + ๐) โ ๐ โง (((invgโ๐บ)โ๐) + (๐ข + ๐)) โ ๐พ))) |
107 | 101, 106 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ (๐ โ ๐ โง (๐ข + ๐) โ ๐ โง (((invgโ๐บ)โ๐) + (๐ข + ๐)) โ ๐พ)) |
108 | 107 | simp3d 1145 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ (((invgโ๐บ)โ๐) + (๐ข + ๐)) โ ๐พ) |
109 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ =
(((invgโ๐บ)โ๐) + (๐ข + ๐)) โ (๐ + ๐ฅ) = (๐ +
(((invgโ๐บ)โ๐) + (๐ข + ๐)))) |
110 | 109 | oveq1d 7373 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ =
(((invgโ๐บ)โ๐) + (๐ข + ๐)) โ ((๐ + ๐ฅ) โ ๐) = ((๐ +
(((invgโ๐บ)โ๐) + (๐ข + ๐))) โ ๐)) |
111 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐)) = (๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐)) |
112 | | ovex 7391 |
. . . . . . . . . . . . . . . . 17
โข ((๐ +
(((invgโ๐บ)โ๐) + (๐ข + ๐))) โ ๐) โ V |
113 | 110, 111,
112 | fvmpt 6949 |
. . . . . . . . . . . . . . . 16
โข
((((invgโ๐บ)โ๐) + (๐ข + ๐)) โ ๐พ โ ((๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐))โ(((invgโ๐บ)โ๐) + (๐ข + ๐))) = ((๐ +
(((invgโ๐บ)โ๐) + (๐ข + ๐))) โ ๐)) |
114 | 108, 113 | syl 17 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ ((๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐))โ(((invgโ๐บ)โ๐) + (๐ข + ๐))) = ((๐ +
(((invgโ๐บ)โ๐) + (๐ข + ๐))) โ ๐)) |
115 | 7, 57, 31, 104 | grprinv 18806 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐บ โ Grp โง ๐ โ ๐) โ (๐ +
((invgโ๐บ)โ๐)) = (0gโ๐บ)) |
116 | 102, 94, 115 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ (๐ +
((invgโ๐บ)โ๐)) = (0gโ๐บ)) |
117 | 116 | oveq1d 7373 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ ((๐ +
((invgโ๐บ)โ๐)) + (๐ข + ๐)) = ((0gโ๐บ) + (๐ข + ๐))) |
118 | 7, 104 | grpinvcl 18803 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐บ โ Grp โง ๐ โ ๐) โ ((invgโ๐บ)โ๐) โ ๐) |
119 | 102, 94, 118 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ ((invgโ๐บ)โ๐) โ ๐) |
120 | 64 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ ๐ป โ ๐) |
121 | 120, 93 | sseldd 3946 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ ๐ข โ ๐) |
122 | 7, 57 | grpcl 18761 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐บ โ Grp โง ๐ข โ ๐ โง ๐ โ ๐) โ (๐ข + ๐) โ ๐) |
123 | 102, 121,
94, 122 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ (๐ข + ๐) โ ๐) |
124 | 7, 57 | grpass 18762 |
. . . . . . . . . . . . . . . . . 18
โข ((๐บ โ Grp โง (๐ โ ๐ โง ((invgโ๐บ)โ๐) โ ๐ โง (๐ข + ๐) โ ๐)) โ ((๐ +
((invgโ๐บ)โ๐)) + (๐ข + ๐)) = (๐ +
(((invgโ๐บ)โ๐) + (๐ข + ๐)))) |
125 | 102, 94, 119, 123, 124 | syl13anc 1373 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ ((๐ +
((invgโ๐บ)โ๐)) + (๐ข + ๐)) = (๐ +
(((invgโ๐บ)โ๐) + (๐ข + ๐)))) |
126 | 7, 57, 31 | grplid 18785 |
. . . . . . . . . . . . . . . . . 18
โข ((๐บ โ Grp โง (๐ข + ๐) โ ๐) โ ((0gโ๐บ) + (๐ข + ๐)) = (๐ข + ๐)) |
127 | 102, 123,
126 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ ((0gโ๐บ) + (๐ข + ๐)) = (๐ข + ๐)) |
128 | 117, 125,
127 | 3eqtr3d 2781 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ (๐ +
(((invgโ๐บ)โ๐) + (๐ข + ๐))) = (๐ข + ๐)) |
129 | 128 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ ((๐ +
(((invgโ๐บ)โ๐) + (๐ข + ๐))) โ ๐) = ((๐ข + ๐) โ ๐)) |
130 | | sylow2blem3.d |
. . . . . . . . . . . . . . . . 17
โข โ =
(-gโ๐บ) |
131 | 7, 57, 130 | grppncan 18843 |
. . . . . . . . . . . . . . . 16
โข ((๐บ โ Grp โง ๐ข โ ๐ โง ๐ โ ๐) โ ((๐ข + ๐) โ ๐) = ๐ข) |
132 | 102, 121,
94, 131 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ ((๐ข + ๐) โ ๐) = ๐ข) |
133 | 114, 129,
132 | 3eqtrd 2777 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ ((๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐))โ(((invgโ๐บ)โ๐) + (๐ข + ๐))) = ๐ข) |
134 | | ovex 7391 |
. . . . . . . . . . . . . . . 16
โข ((๐ + ๐ฅ) โ ๐) โ V |
135 | 134, 111 | fnmpti 6645 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐)) Fn ๐พ |
136 | | fnfvelrn 7032 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐)) Fn ๐พ โง (((invgโ๐บ)โ๐) + (๐ข + ๐)) โ ๐พ) โ ((๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐))โ(((invgโ๐บ)โ๐) + (๐ข + ๐))) โ ran (๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐))) |
137 | 135, 108,
136 | sylancr 588 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ ((๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐))โ(((invgโ๐บ)โ๐) + (๐ข + ๐))) โ ran (๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐))) |
138 | 133, 137 | eqeltrrd 2835 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง (๐ข โ ๐ป โง (๐ข ยท ๐ง) = ๐ง)) โ ๐ข โ ran (๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐))) |
139 | 138 | expr 458 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง ๐ข โ ๐ป) โ ((๐ข ยท ๐ง) = ๐ง โ ๐ข โ ran (๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐)))) |
140 | 139 | ralimdva 3161 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โ
(โ๐ข โ ๐ป (๐ข ยท ๐ง) = ๐ง โ โ๐ข โ ๐ป ๐ข โ ran (๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐)))) |
141 | 140 | imp 408 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โง
โ๐ข โ ๐ป (๐ข ยท ๐ง) = ๐ง) โ โ๐ข โ ๐ป ๐ข โ ran (๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐))) |
142 | 141 | an32s 651 |
. . . . . . . . 9
โข (((๐ โง โ๐ข โ ๐ป (๐ข ยท ๐ง) = ๐ง) โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โ
โ๐ข โ ๐ป ๐ข โ ran (๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐))) |
143 | | dfss3 3933 |
. . . . . . . . 9
โข (๐ป โ ran (๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐)) โ โ๐ข โ ๐ป ๐ข โ ran (๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐))) |
144 | 142, 143 | sylibr 233 |
. . . . . . . 8
โข (((๐ โง โ๐ข โ ๐ป (๐ข ยท ๐ง) = ๐ง) โง (๐ โ ๐ โง ๐ง = [๐] โผ )) โ ๐ป โ ran (๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐))) |
145 | 144 | expr 458 |
. . . . . . 7
โข (((๐ โง โ๐ข โ ๐ป (๐ข ยท ๐ง) = ๐ง) โง ๐ โ ๐) โ (๐ง = [๐] โผ โ ๐ป โ ran (๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐)))) |
146 | 145 | reximdva 3162 |
. . . . . 6
โข ((๐ โง โ๐ข โ ๐ป (๐ข ยท ๐ง) = ๐ง) โ (โ๐ โ ๐ ๐ง = [๐] โผ โ โ๐ โ ๐ ๐ป โ ran (๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐)))) |
147 | 146 | ex 414 |
. . . . 5
โข (๐ โ (โ๐ข โ ๐ป (๐ข ยท ๐ง) = ๐ง โ (โ๐ โ ๐ ๐ง = [๐] โผ โ โ๐ โ ๐ ๐ป โ ran (๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐))))) |
148 | 147 | com23 86 |
. . . 4
โข (๐ โ (โ๐ โ ๐ ๐ง = [๐] โผ โ
(โ๐ข โ ๐ป (๐ข ยท ๐ง) = ๐ง โ โ๐ โ ๐ ๐ป โ ran (๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐))))) |
149 | 88, 148 | biimtrid 241 |
. . 3
โข (๐ โ (๐ง โ (๐ / โผ ) โ
(โ๐ข โ ๐ป (๐ข ยท ๐ง) = ๐ง โ โ๐ โ ๐ ๐ป โ ran (๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐))))) |
150 | 149 | rexlimdv 3147 |
. 2
โข (๐ โ (โ๐ง โ (๐ / โผ )โ๐ข โ ๐ป (๐ข ยท ๐ง) = ๐ง โ โ๐ โ ๐ ๐ป โ ran (๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐)))) |
151 | 86, 150 | mpd 15 |
1
โข (๐ โ โ๐ โ ๐ ๐ป โ ran (๐ฅ โ ๐พ โฆ ((๐ + ๐ฅ) โ ๐))) |