Step | Hyp | Ref
| Expression |
1 | | pgpfac1.n |
. . . . . . . . . 10
β’ (π β π΅ β Fin) |
2 | | pwfi 9056 |
. . . . . . . . . 10
β’ (π΅ β Fin β π«
π΅ β
Fin) |
3 | 1, 2 | sylib 217 |
. . . . . . . . 9
β’ (π β π« π΅ β Fin) |
4 | 3 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π) β π« π΅ β Fin) |
5 | | pgpfac1.b |
. . . . . . . . . . . 12
β’ π΅ = (BaseβπΊ) |
6 | 5 | subgss 18862 |
. . . . . . . . . . 11
β’ (π£ β (SubGrpβπΊ) β π£ β π΅) |
7 | 6 | 3ad2ant2 1135 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π£ β (SubGrpβπΊ) β§ (π£ β π β§ π΄ β π£)) β π£ β π΅) |
8 | | velpw 4564 |
. . . . . . . . . 10
β’ (π£ β π« π΅ β π£ β π΅) |
9 | 7, 8 | sylibr 233 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π£ β (SubGrpβπΊ) β§ (π£ β π β§ π΄ β π£)) β π£ β π« π΅) |
10 | 9 | rabssdv 4031 |
. . . . . . . 8
β’ ((π β§ π β π) β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} β π« π΅) |
11 | 4, 10 | ssfid 9145 |
. . . . . . 7
β’ ((π β§ π β π) β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} β Fin) |
12 | | finnum 9818 |
. . . . . . 7
β’ ({π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} β Fin β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} β dom card) |
13 | 11, 12 | syl 17 |
. . . . . 6
β’ ((π β§ π β π) β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} β dom card) |
14 | | pgpfac1.s |
. . . . . . . . . 10
β’ π = (πΎβ{π΄}) |
15 | | pgpfac1.g |
. . . . . . . . . . . . 13
β’ (π β πΊ β Abel) |
16 | | ablgrp 19496 |
. . . . . . . . . . . . 13
β’ (πΊ β Abel β πΊ β Grp) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . 12
β’ (π β πΊ β Grp) |
18 | 5 | subgacs 18895 |
. . . . . . . . . . . 12
β’ (πΊ β Grp β
(SubGrpβπΊ) β
(ACSβπ΅)) |
19 | | acsmre 17467 |
. . . . . . . . . . . 12
β’
((SubGrpβπΊ)
β (ACSβπ΅) β
(SubGrpβπΊ) β
(Mooreβπ΅)) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β (SubGrpβπΊ) β (Mooreβπ΅)) |
21 | | pgpfac1.u |
. . . . . . . . . . . . 13
β’ (π β π β (SubGrpβπΊ)) |
22 | 5 | subgss 18862 |
. . . . . . . . . . . . 13
β’ (π β (SubGrpβπΊ) β π β π΅) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π β π΅) |
24 | | pgpfac1.au |
. . . . . . . . . . . 12
β’ (π β π΄ β π) |
25 | 23, 24 | sseldd 3944 |
. . . . . . . . . . 11
β’ (π β π΄ β π΅) |
26 | | pgpfac1.k |
. . . . . . . . . . . 12
β’ πΎ =
(mrClsβ(SubGrpβπΊ)) |
27 | 26 | mrcsncl 17427 |
. . . . . . . . . . 11
β’
(((SubGrpβπΊ)
β (Mooreβπ΅)
β§ π΄ β π΅) β (πΎβ{π΄}) β (SubGrpβπΊ)) |
28 | 20, 25, 27 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (πΎβ{π΄}) β (SubGrpβπΊ)) |
29 | 14, 28 | eqeltrid 2843 |
. . . . . . . . 9
β’ (π β π β (SubGrpβπΊ)) |
30 | 29 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π) β π β (SubGrpβπΊ)) |
31 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β π) β π β π) |
32 | 24 | snssd 4768 |
. . . . . . . . . . . . 13
β’ (π β {π΄} β π) |
33 | 32, 23 | sstrd 3953 |
. . . . . . . . . . . 12
β’ (π β {π΄} β π΅) |
34 | 20, 26, 33 | mrcssidd 17440 |
. . . . . . . . . . 11
β’ (π β {π΄} β (πΎβ{π΄})) |
35 | 34, 14 | sseqtrrdi 3994 |
. . . . . . . . . 10
β’ (π β {π΄} β π) |
36 | | snssg 4743 |
. . . . . . . . . . 11
β’ (π΄ β π΅ β (π΄ β π β {π΄} β π)) |
37 | 25, 36 | syl 17 |
. . . . . . . . . 10
β’ (π β (π΄ β π β {π΄} β π)) |
38 | 35, 37 | mpbird 257 |
. . . . . . . . 9
β’ (π β π΄ β π) |
39 | 38 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π) β π΄ β π) |
40 | | psseq1 4046 |
. . . . . . . . . 10
β’ (π£ = π β (π£ β π β π β π)) |
41 | | eleq2 2827 |
. . . . . . . . . 10
β’ (π£ = π β (π΄ β π£ β π΄ β π)) |
42 | 40, 41 | anbi12d 632 |
. . . . . . . . 9
β’ (π£ = π β ((π£ β π β§ π΄ β π£) β (π β π β§ π΄ β π))) |
43 | 42 | rspcev 3580 |
. . . . . . . 8
β’ ((π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π)) β βπ£ β (SubGrpβπΊ)(π£ β π β§ π΄ β π£)) |
44 | 30, 31, 39, 43 | syl12anc 836 |
. . . . . . 7
β’ ((π β§ π β π) β βπ£ β (SubGrpβπΊ)(π£ β π β§ π΄ β π£)) |
45 | | rabn0 4344 |
. . . . . . 7
β’ ({π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} β β
β βπ£ β (SubGrpβπΊ)(π£ β π β§ π΄ β π£)) |
46 | 44, 45 | sylibr 233 |
. . . . . 6
β’ ((π β§ π β π) β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} β β
) |
47 | | simpr1 1195 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π’ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} β§ π’ β β
β§ [β] Or
π’)) β π’ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)}) |
48 | | simpr2 1196 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ (π’ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} β§ π’ β β
β§ [β] Or
π’)) β π’ β β
) |
49 | 11 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ (π’ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} β§ π’ β β
β§ [β] Or
π’)) β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} β Fin) |
50 | 49, 47 | ssfid 9145 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ (π’ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} β§ π’ β β
β§ [β] Or
π’)) β π’ β Fin) |
51 | | simpr3 1197 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ (π’ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} β§ π’ β β
β§ [β] Or
π’)) β
[β] Or π’) |
52 | | fin1a2lem10 10279 |
. . . . . . . . . 10
β’ ((π’ β β
β§ π’ β Fin β§
[β] Or π’)
β βͺ π’ β π’) |
53 | 48, 50, 51, 52 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π’ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} β§ π’ β β
β§ [β] Or
π’)) β βͺ π’
β π’) |
54 | 47, 53 | sseldd 3944 |
. . . . . . . 8
β’ (((π β§ π β π) β§ (π’ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} β§ π’ β β
β§ [β] Or
π’)) β βͺ π’
β {π£ β
(SubGrpβπΊ) β£
(π£ β π β§ π΄ β π£)}) |
55 | 54 | ex 414 |
. . . . . . 7
β’ ((π β§ π β π) β ((π’ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} β§ π’ β β
β§ [β] Or
π’) β βͺ π’
β {π£ β
(SubGrpβπΊ) β£
(π£ β π β§ π΄ β π£)})) |
56 | 55 | alrimiv 1931 |
. . . . . 6
β’ ((π β§ π β π) β βπ’((π’ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} β§ π’ β β
β§ [β] Or
π’) β βͺ π’
β {π£ β
(SubGrpβπΊ) β£
(π£ β π β§ π΄ β π£)})) |
57 | | zornn0g 10375 |
. . . . . 6
β’ (({π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} β dom card β§ {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} β β
β§ βπ’((π’ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} β§ π’ β β
β§ [β] Or
π’) β βͺ π’
β {π£ β
(SubGrpβπΊ) β£
(π£ β π β§ π΄ β π£)})) β βπ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)}βπ€ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} Β¬ π β π€) |
58 | 13, 46, 56, 57 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π β π) β βπ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)}βπ€ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} Β¬ π β π€) |
59 | | psseq1 4046 |
. . . . . . . 8
β’ (π£ = π€ β (π£ β π β π€ β π)) |
60 | | eleq2 2827 |
. . . . . . . 8
β’ (π£ = π€ β (π΄ β π£ β π΄ β π€)) |
61 | 59, 60 | anbi12d 632 |
. . . . . . 7
β’ (π£ = π€ β ((π£ β π β§ π΄ β π£) β (π€ β π β§ π΄ β π€))) |
62 | 61 | ralrab 3650 |
. . . . . 6
β’
(βπ€ β
{π£ β
(SubGrpβπΊ) β£
(π£ β π β§ π΄ β π£)} Β¬ π β π€ β βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) |
63 | 62 | rexbii 3096 |
. . . . 5
β’
(βπ β
{π£ β
(SubGrpβπΊ) β£
(π£ β π β§ π΄ β π£)}βπ€ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} Β¬ π β π€ β βπ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)}βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) |
64 | 58, 63 | sylib 217 |
. . . 4
β’ ((π β§ π β π) β βπ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)}βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) |
65 | 64 | ex 414 |
. . 3
β’ (π β (π β π β βπ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)}βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€))) |
66 | | pgpfac1.3 |
. . . . 5
β’ (π β βπ β (SubGrpβπΊ)((π β π β§ π΄ β π ) β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π ))) |
67 | | psseq1 4046 |
. . . . . . 7
β’ (π£ = π β (π£ β π β π β π)) |
68 | | eleq2 2827 |
. . . . . . 7
β’ (π£ = π β (π΄ β π£ β π΄ β π )) |
69 | 67, 68 | anbi12d 632 |
. . . . . 6
β’ (π£ = π β ((π£ β π β§ π΄ β π£) β (π β π β§ π΄ β π ))) |
70 | 69 | ralrab 3650 |
. . . . 5
β’
(βπ β
{π£ β
(SubGrpβπΊ) β£
(π£ β π β§ π΄ β π£)}βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π ) β βπ β (SubGrpβπΊ)((π β π β§ π΄ β π ) β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π ))) |
71 | 66, 70 | sylibr 233 |
. . . 4
β’ (π β βπ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)}βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π )) |
72 | | r19.29 3116 |
. . . . 5
β’
((βπ β
{π£ β
(SubGrpβπΊ) β£
(π£ β π β§ π΄ β π£)}βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π ) β§ βπ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)}βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) β βπ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} (βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π ) β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€))) |
73 | 69 | elrab 3644 |
. . . . . . 7
β’ (π β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} β (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) |
74 | | ineq2 4165 |
. . . . . . . . . . . 12
β’ (π‘ = π£ β (π β© π‘) = (π β© π£)) |
75 | 74 | eqeq1d 2740 |
. . . . . . . . . . 11
β’ (π‘ = π£ β ((π β© π‘) = { 0 } β (π β© π£) = { 0 })) |
76 | | oveq2 7358 |
. . . . . . . . . . . 12
β’ (π‘ = π£ β (π β π‘) = (π β π£)) |
77 | 76 | eqeq1d 2740 |
. . . . . . . . . . 11
β’ (π‘ = π£ β ((π β π‘) = π β (π β π£) = π )) |
78 | 75, 77 | anbi12d 632 |
. . . . . . . . . 10
β’ (π‘ = π£ β (((π β© π‘) = { 0 } β§ (π β π‘) = π ) β ((π β© π£) = { 0 } β§ (π β π£) = π ))) |
79 | 78 | cbvrexvw 3225 |
. . . . . . . . 9
β’
(βπ‘ β
(SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π ) β βπ£ β (SubGrpβπΊ)((π β© π£) = { 0 } β§ (π β π£) = π )) |
80 | | simprrl 780 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β π β π) |
81 | 80 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ ((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€))) β π β π) |
82 | | simpr2 1196 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ ((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€))) β (π β π£) = π ) |
83 | 82 | psseq1d 4051 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ ((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€))) β ((π β π£) β π β π β π)) |
84 | 81, 83 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ ((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€))) β (π β π£) β π) |
85 | | pssdif 4325 |
. . . . . . . . . . . . . . 15
β’ ((π β π£) β π β (π β (π β π£)) β β
) |
86 | | n0 4305 |
. . . . . . . . . . . . . . 15
β’ ((π β (π β π£)) β β
β βπ π β (π β (π β π£))) |
87 | 85, 86 | sylib 217 |
. . . . . . . . . . . . . 14
β’ ((π β π£) β π β βπ π β (π β (π β π£))) |
88 | 84, 87 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ ((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€))) β βπ π β (π β (π β π£))) |
89 | | pgpfac1.o |
. . . . . . . . . . . . . . . 16
β’ π = (odβπΊ) |
90 | | pgpfac1.e |
. . . . . . . . . . . . . . . 16
β’ πΈ = (gExβπΊ) |
91 | | pgpfac1.z |
. . . . . . . . . . . . . . . 16
β’ 0 =
(0gβπΊ) |
92 | | pgpfac1.l |
. . . . . . . . . . . . . . . 16
β’ β =
(LSSumβπΊ) |
93 | | pgpfac1.p |
. . . . . . . . . . . . . . . . 17
β’ (π β π pGrp πΊ) |
94 | 93 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ (((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) β§ π β (π β (π β π£)))) β π pGrp πΊ) |
95 | 15 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ (((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) β§ π β (π β (π β π£)))) β πΊ β Abel) |
96 | 1 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ (((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) β§ π β (π β (π β π£)))) β π΅ β Fin) |
97 | | pgpfac1.oe |
. . . . . . . . . . . . . . . . 17
β’ (π β (πβπ΄) = πΈ) |
98 | 97 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ (((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) β§ π β (π β (π β π£)))) β (πβπ΄) = πΈ) |
99 | 21 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ (((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) β§ π β (π β (π β π£)))) β π β (SubGrpβπΊ)) |
100 | 24 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ (((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) β§ π β (π β (π β π£)))) β π΄ β π) |
101 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ (((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) β§ π β (π β (π β π£)))) β π£ β (SubGrpβπΊ)) |
102 | | simprl1 1219 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ (((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) β§ π β (π β (π β π£)))) β (π β© π£) = { 0 }) |
103 | 84 | adantrr 716 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ (((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) β§ π β (π β (π β π£)))) β (π β π£) β π) |
104 | 103 | pssssd 4056 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ (((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) β§ π β (π β (π β π£)))) β (π β π£) β π) |
105 | | simprl3 1221 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ (((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) β§ π β (π β (π β π£)))) β βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) |
106 | 82 | adantrr 716 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ (((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) β§ π β (π β (π β π£)))) β (π β π£) = π ) |
107 | | psseq1 4046 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β π£) = π β ((π β π£) β π¦ β π β π¦)) |
108 | 107 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β π£) = π β (Β¬ (π β π£) β π¦ β Β¬ π β π¦)) |
109 | 108 | imbi2d 341 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β π£) = π β (((π¦ β π β§ π΄ β π¦) β Β¬ (π β π£) β π¦) β ((π¦ β π β§ π΄ β π¦) β Β¬ π β π¦))) |
110 | 109 | ralbidv 3173 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β π£) = π β (βπ¦ β (SubGrpβπΊ)((π¦ β π β§ π΄ β π¦) β Β¬ (π β π£) β π¦) β βπ¦ β (SubGrpβπΊ)((π¦ β π β§ π΄ β π¦) β Β¬ π β π¦))) |
111 | | psseq1 4046 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ = π€ β (π¦ β π β π€ β π)) |
112 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ = π€ β (π΄ β π¦ β π΄ β π€)) |
113 | 111, 112 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ = π€ β ((π¦ β π β§ π΄ β π¦) β (π€ β π β§ π΄ β π€))) |
114 | | psseq2 4047 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ = π€ β (π β π¦ β π β π€)) |
115 | 114 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ = π€ β (Β¬ π β π¦ β Β¬ π β π€)) |
116 | 113, 115 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = π€ β (((π¦ β π β§ π΄ β π¦) β Β¬ π β π¦) β ((π€ β π β§ π΄ β π€) β Β¬ π β π€))) |
117 | 116 | cbvralvw 3224 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ¦ β
(SubGrpβπΊ)((π¦ β π β§ π΄ β π¦) β Β¬ π β π¦) β βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) |
118 | 110, 117 | bitrdi 287 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π£) = π β (βπ¦ β (SubGrpβπΊ)((π¦ β π β§ π΄ β π¦) β Β¬ (π β π£) β π¦) β βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€))) |
119 | 106, 118 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ (((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) β§ π β (π β (π β π£)))) β (βπ¦ β (SubGrpβπΊ)((π¦ β π β§ π΄ β π¦) β Β¬ (π β π£) β π¦) β βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€))) |
120 | 105, 119 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ (((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) β§ π β (π β (π β π£)))) β βπ¦ β (SubGrpβπΊ)((π¦ β π β§ π΄ β π¦) β Β¬ (π β π£) β π¦)) |
121 | | simprr 772 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ (((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) β§ π β (π β (π β π£)))) β π β (π β (π β π£))) |
122 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
β’
(.gβπΊ) = (.gβπΊ) |
123 | 26, 14, 5, 89, 90, 91, 92, 94, 95, 96, 98, 99, 100, 101, 102, 104, 120, 121, 122 | pgpfac1lem4 19786 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ (((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) β§ π β (π β (π β π£)))) β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π)) |
124 | 123 | expr 458 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ ((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€))) β (π β (π β (π β π£)) β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π))) |
125 | 124 | exlimdv 1937 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ ((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€))) β (βπ π β (π β (π β π£)) β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π))) |
126 | 88, 125 | mpd 15 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β§ ((π β© π£) = { 0 } β§ (π β π£) = π β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€))) β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π)) |
127 | 126 | 3exp2 1355 |
. . . . . . . . . . 11
β’ (((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β ((π β© π£) = { 0 } β ((π β π£) = π β (βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€) β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π))))) |
128 | 127 | impd 412 |
. . . . . . . . . 10
β’ (((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β§ π£ β (SubGrpβπΊ)) β (((π β© π£) = { 0 } β§ (π β π£) = π ) β (βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€) β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π)))) |
129 | 128 | rexlimdva 3151 |
. . . . . . . . 9
β’ ((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β (βπ£ β (SubGrpβπΊ)((π β© π£) = { 0 } β§ (π β π£) = π ) β (βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€) β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π)))) |
130 | 79, 129 | biimtrid 241 |
. . . . . . . 8
β’ ((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β (βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π ) β (βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€) β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π)))) |
131 | 130 | impd 412 |
. . . . . . 7
β’ ((π β§ (π β (SubGrpβπΊ) β§ (π β π β§ π΄ β π ))) β ((βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π ) β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π))) |
132 | 73, 131 | sylan2b 595 |
. . . . . 6
β’ ((π β§ π β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)}) β ((βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π ) β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π))) |
133 | 132 | rexlimdva 3151 |
. . . . 5
β’ (π β (βπ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)} (βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π ) β§ βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π))) |
134 | 72, 133 | syl5 34 |
. . . 4
β’ (π β ((βπ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)}βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π ) β§ βπ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)}βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€)) β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π))) |
135 | 71, 134 | mpand 694 |
. . 3
β’ (π β (βπ β {π£ β (SubGrpβπΊ) β£ (π£ β π β§ π΄ β π£)}βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ π β π€) β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π))) |
136 | 65, 135 | syld 47 |
. 2
β’ (π β (π β π β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π))) |
137 | 91 | 0subg 18886 |
. . . . . 6
β’ (πΊ β Grp β { 0 } β
(SubGrpβπΊ)) |
138 | 17, 137 | syl 17 |
. . . . 5
β’ (π β { 0 } β
(SubGrpβπΊ)) |
139 | 138 | adantr 482 |
. . . 4
β’ ((π β§ π = π) β { 0 } β
(SubGrpβπΊ)) |
140 | 91 | subg0cl 18869 |
. . . . . . . 8
β’ (π β (SubGrpβπΊ) β 0 β π) |
141 | 29, 140 | syl 17 |
. . . . . . 7
β’ (π β 0 β π) |
142 | 141 | snssd 4768 |
. . . . . 6
β’ (π β { 0 } β π) |
143 | 142 | adantr 482 |
. . . . 5
β’ ((π β§ π = π) β { 0 } β π) |
144 | | sseqin2 4174 |
. . . . 5
β’ ({ 0 } β
π β (π β© { 0 }) = { 0 }) |
145 | 143, 144 | sylib 217 |
. . . 4
β’ ((π β§ π = π) β (π β© { 0 }) = { 0 }) |
146 | 92 | lsmss2 19378 |
. . . . . . 7
β’ ((π β (SubGrpβπΊ) β§ { 0 } β
(SubGrpβπΊ) β§ {
0 }
β π) β (π β { 0 }) = π) |
147 | 29, 138, 142, 146 | syl3anc 1372 |
. . . . . 6
β’ (π β (π β { 0 }) = π) |
148 | 147 | eqeq1d 2740 |
. . . . 5
β’ (π β ((π β { 0 }) = π β π = π)) |
149 | 148 | biimpar 479 |
. . . 4
β’ ((π β§ π = π) β (π β { 0 }) = π) |
150 | | ineq2 4165 |
. . . . . . 7
β’ (π‘ = { 0 } β (π β© π‘) = (π β© { 0 })) |
151 | 150 | eqeq1d 2740 |
. . . . . 6
β’ (π‘ = { 0 } β ((π β© π‘) = { 0 } β (π β© { 0 }) = { 0 })) |
152 | | oveq2 7358 |
. . . . . . 7
β’ (π‘ = { 0 } β (π β π‘) = (π β { 0
})) |
153 | 152 | eqeq1d 2740 |
. . . . . 6
β’ (π‘ = { 0 } β ((π β π‘) = π β (π β { 0 }) = π)) |
154 | 151, 153 | anbi12d 632 |
. . . . 5
β’ (π‘ = { 0 } β (((π β© π‘) = { 0 } β§ (π β π‘) = π) β ((π β© { 0 }) = { 0 } β§ (π β { 0 }) = π))) |
155 | 154 | rspcev 3580 |
. . . 4
β’ (({ 0 } β
(SubGrpβπΊ) β§
((π β© { 0 }) = { 0 } β§
(π β { 0 }) = π)) β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π)) |
156 | 139, 145,
149, 155 | syl12anc 836 |
. . 3
β’ ((π β§ π = π) β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π)) |
157 | 156 | ex 414 |
. 2
β’ (π β (π = π β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π))) |
158 | 26 | mrcsscl 17435 |
. . . . 5
β’
(((SubGrpβπΊ)
β (Mooreβπ΅)
β§ {π΄} β π β§ π β (SubGrpβπΊ)) β (πΎβ{π΄}) β π) |
159 | 20, 32, 21, 158 | syl3anc 1372 |
. . . 4
β’ (π β (πΎβ{π΄}) β π) |
160 | 14, 159 | eqsstrid 3991 |
. . 3
β’ (π β π β π) |
161 | | sspss 4058 |
. . 3
β’ (π β π β (π β π β¨ π = π)) |
162 | 160, 161 | sylib 217 |
. 2
β’ (π β (π β π β¨ π = π)) |
163 | 136, 157,
162 | mpjaod 859 |
1
β’ (π β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π)) |