Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’
(CntzβπΊ) =
(CntzβπΊ) |
2 | | eqid 2733 |
. . 3
β’
(0gβπΊ) = (0gβπΊ) |
3 | | eqid 2733 |
. . 3
β’
(mrClsβ(SubGrpβπΊ)) = (mrClsβ(SubGrpβπΊ)) |
4 | | dprdss.1 |
. . . 4
β’ (π β πΊdom DProd π) |
5 | | dprdgrp 19870 |
. . . 4
β’ (πΊdom DProd π β πΊ β Grp) |
6 | 4, 5 | syl 17 |
. . 3
β’ (π β πΊ β Grp) |
7 | | dprdss.2 |
. . . 4
β’ (π β dom π = πΌ) |
8 | 4, 7 | dprddomcld 19866 |
. . 3
β’ (π β πΌ β V) |
9 | | dprdss.3 |
. . 3
β’ (π β π:πΌβΆ(SubGrpβπΊ)) |
10 | | dprdss.4 |
. . . . . . 7
β’ ((π β§ π β πΌ) β (πβπ) β (πβπ)) |
11 | 10 | ralrimiva 3147 |
. . . . . 6
β’ (π β βπ β πΌ (πβπ) β (πβπ)) |
12 | | fveq2 6889 |
. . . . . . . 8
β’ (π = π₯ β (πβπ) = (πβπ₯)) |
13 | | fveq2 6889 |
. . . . . . . 8
β’ (π = π₯ β (πβπ) = (πβπ₯)) |
14 | 12, 13 | sseq12d 4015 |
. . . . . . 7
β’ (π = π₯ β ((πβπ) β (πβπ) β (πβπ₯) β (πβπ₯))) |
15 | 14 | rspcv 3609 |
. . . . . 6
β’ (π₯ β πΌ β (βπ β πΌ (πβπ) β (πβπ) β (πβπ₯) β (πβπ₯))) |
16 | 11, 15 | mpan9 508 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β (πβπ₯) β (πβπ₯)) |
17 | 16 | 3ad2antr1 1189 |
. . . 4
β’ ((π β§ (π₯ β πΌ β§ π¦ β πΌ β§ π₯ β π¦)) β (πβπ₯) β (πβπ₯)) |
18 | 4 | adantr 482 |
. . . . . 6
β’ ((π β§ (π₯ β πΌ β§ π¦ β πΌ β§ π₯ β π¦)) β πΊdom DProd π) |
19 | 7 | adantr 482 |
. . . . . 6
β’ ((π β§ (π₯ β πΌ β§ π¦ β πΌ β§ π₯ β π¦)) β dom π = πΌ) |
20 | | simpr1 1195 |
. . . . . 6
β’ ((π β§ (π₯ β πΌ β§ π¦ β πΌ β§ π₯ β π¦)) β π₯ β πΌ) |
21 | | simpr2 1196 |
. . . . . 6
β’ ((π β§ (π₯ β πΌ β§ π¦ β πΌ β§ π₯ β π¦)) β π¦ β πΌ) |
22 | | simpr3 1197 |
. . . . . 6
β’ ((π β§ (π₯ β πΌ β§ π¦ β πΌ β§ π₯ β π¦)) β π₯ β π¦) |
23 | 18, 19, 20, 21, 22, 1 | dprdcntz 19873 |
. . . . 5
β’ ((π β§ (π₯ β πΌ β§ π¦ β πΌ β§ π₯ β π¦)) β (πβπ₯) β ((CntzβπΊ)β(πβπ¦))) |
24 | 4, 7 | dprdf2 19872 |
. . . . . . . . 9
β’ (π β π:πΌβΆ(SubGrpβπΊ)) |
25 | 24 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π₯ β πΌ β§ π¦ β πΌ β§ π₯ β π¦)) β π:πΌβΆ(SubGrpβπΊ)) |
26 | 25, 21 | ffvelcdmd 7085 |
. . . . . . 7
β’ ((π β§ (π₯ β πΌ β§ π¦ β πΌ β§ π₯ β π¦)) β (πβπ¦) β (SubGrpβπΊ)) |
27 | | eqid 2733 |
. . . . . . . 8
β’
(BaseβπΊ) =
(BaseβπΊ) |
28 | 27 | subgss 19002 |
. . . . . . 7
β’ ((πβπ¦) β (SubGrpβπΊ) β (πβπ¦) β (BaseβπΊ)) |
29 | 26, 28 | syl 17 |
. . . . . 6
β’ ((π β§ (π₯ β πΌ β§ π¦ β πΌ β§ π₯ β π¦)) β (πβπ¦) β (BaseβπΊ)) |
30 | | fveq2 6889 |
. . . . . . . 8
β’ (π = π¦ β (πβπ) = (πβπ¦)) |
31 | | fveq2 6889 |
. . . . . . . 8
β’ (π = π¦ β (πβπ) = (πβπ¦)) |
32 | 30, 31 | sseq12d 4015 |
. . . . . . 7
β’ (π = π¦ β ((πβπ) β (πβπ) β (πβπ¦) β (πβπ¦))) |
33 | 11 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β πΌ β§ π¦ β πΌ β§ π₯ β π¦)) β βπ β πΌ (πβπ) β (πβπ)) |
34 | 32, 33, 21 | rspcdva 3614 |
. . . . . 6
β’ ((π β§ (π₯ β πΌ β§ π¦ β πΌ β§ π₯ β π¦)) β (πβπ¦) β (πβπ¦)) |
35 | 27, 1 | cntz2ss 19194 |
. . . . . 6
β’ (((πβπ¦) β (BaseβπΊ) β§ (πβπ¦) β (πβπ¦)) β ((CntzβπΊ)β(πβπ¦)) β ((CntzβπΊ)β(πβπ¦))) |
36 | 29, 34, 35 | syl2anc 585 |
. . . . 5
β’ ((π β§ (π₯ β πΌ β§ π¦ β πΌ β§ π₯ β π¦)) β ((CntzβπΊ)β(πβπ¦)) β ((CntzβπΊ)β(πβπ¦))) |
37 | 23, 36 | sstrd 3992 |
. . . 4
β’ ((π β§ (π₯ β πΌ β§ π¦ β πΌ β§ π₯ β π¦)) β (πβπ₯) β ((CntzβπΊ)β(πβπ¦))) |
38 | 17, 37 | sstrd 3992 |
. . 3
β’ ((π β§ (π₯ β πΌ β§ π¦ β πΌ β§ π₯ β π¦)) β (πβπ₯) β ((CntzβπΊ)β(πβπ¦))) |
39 | 6 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β πΊ β Grp) |
40 | 27 | subgacs 19036 |
. . . . . . 7
β’ (πΊ β Grp β
(SubGrpβπΊ) β
(ACSβ(BaseβπΊ))) |
41 | | acsmre 17593 |
. . . . . . 7
β’
((SubGrpβπΊ)
β (ACSβ(BaseβπΊ)) β (SubGrpβπΊ) β (Mooreβ(BaseβπΊ))) |
42 | 39, 40, 41 | 3syl 18 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β (SubGrpβπΊ) β (Mooreβ(BaseβπΊ))) |
43 | | difss 4131 |
. . . . . . . . 9
β’ (πΌ β {π₯}) β πΌ |
44 | 11 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΌ) β βπ β πΌ (πβπ) β (πβπ)) |
45 | | ssralv 4050 |
. . . . . . . . 9
β’ ((πΌ β {π₯}) β πΌ β (βπ β πΌ (πβπ) β (πβπ) β βπ β (πΌ β {π₯})(πβπ) β (πβπ))) |
46 | 43, 44, 45 | mpsyl 68 |
. . . . . . . 8
β’ ((π β§ π₯ β πΌ) β βπ β (πΌ β {π₯})(πβπ) β (πβπ)) |
47 | | ss2iun 5015 |
. . . . . . . 8
β’
(βπ β
(πΌ β {π₯})(πβπ) β (πβπ) β βͺ
π β (πΌ β {π₯})(πβπ) β βͺ
π β (πΌ β {π₯})(πβπ)) |
48 | 46, 47 | syl 17 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β βͺ
π β (πΌ β {π₯})(πβπ) β βͺ
π β (πΌ β {π₯})(πβπ)) |
49 | 9 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β πΌ) β π:πΌβΆ(SubGrpβπΊ)) |
50 | | ffun 6718 |
. . . . . . . 8
β’ (π:πΌβΆ(SubGrpβπΊ) β Fun π) |
51 | | funiunfv 7244 |
. . . . . . . 8
β’ (Fun
π β βͺ π β (πΌ β {π₯})(πβπ) = βͺ (π β (πΌ β {π₯}))) |
52 | 49, 50, 51 | 3syl 18 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β βͺ
π β (πΌ β {π₯})(πβπ) = βͺ (π β (πΌ β {π₯}))) |
53 | 24 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β πΌ) β π:πΌβΆ(SubGrpβπΊ)) |
54 | | ffun 6718 |
. . . . . . . 8
β’ (π:πΌβΆ(SubGrpβπΊ) β Fun π) |
55 | | funiunfv 7244 |
. . . . . . . 8
β’ (Fun
π β βͺ π β (πΌ β {π₯})(πβπ) = βͺ (π β (πΌ β {π₯}))) |
56 | 53, 54, 55 | 3syl 18 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β βͺ
π β (πΌ β {π₯})(πβπ) = βͺ (π β (πΌ β {π₯}))) |
57 | 48, 52, 56 | 3sstr3d 4028 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β βͺ (π β (πΌ β {π₯})) β βͺ
(π β (πΌ β {π₯}))) |
58 | | imassrn 6069 |
. . . . . . . 8
β’ (π β (πΌ β {π₯})) β ran π |
59 | 53 | frnd 6723 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΌ) β ran π β (SubGrpβπΊ)) |
60 | | mresspw 17533 |
. . . . . . . . . 10
β’
((SubGrpβπΊ)
β (Mooreβ(BaseβπΊ)) β (SubGrpβπΊ) β π« (BaseβπΊ)) |
61 | 42, 60 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΌ) β (SubGrpβπΊ) β π« (BaseβπΊ)) |
62 | 59, 61 | sstrd 3992 |
. . . . . . . 8
β’ ((π β§ π₯ β πΌ) β ran π β π« (BaseβπΊ)) |
63 | 58, 62 | sstrid 3993 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β (π β (πΌ β {π₯})) β π« (BaseβπΊ)) |
64 | | sspwuni 5103 |
. . . . . . 7
β’ ((π β (πΌ β {π₯})) β π« (BaseβπΊ) β βͺ (π
β (πΌ β {π₯})) β (BaseβπΊ)) |
65 | 63, 64 | sylib 217 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β βͺ (π β (πΌ β {π₯})) β (BaseβπΊ)) |
66 | 42, 3, 57, 65 | mrcssd 17565 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯}))) β
((mrClsβ(SubGrpβπΊ))ββͺ (π β (πΌ β {π₯})))) |
67 | | ss2in 4236 |
. . . . 5
β’ (((πβπ₯) β (πβπ₯) β§ ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯}))) β
((mrClsβ(SubGrpβπΊ))ββͺ (π β (πΌ β {π₯})))) β ((πβπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯})))) β ((πβπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯}))))) |
68 | 16, 66, 67 | syl2anc 585 |
. . . 4
β’ ((π β§ π₯ β πΌ) β ((πβπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯})))) β ((πβπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯}))))) |
69 | 4 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β πΊdom DProd π) |
70 | 7 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β dom π = πΌ) |
71 | | simpr 486 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β π₯ β πΌ) |
72 | 69, 70, 71, 2, 3 | dprddisj 19874 |
. . . 4
β’ ((π β§ π₯ β πΌ) β ((πβπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯})))) =
{(0gβπΊ)}) |
73 | 68, 72 | sseqtrd 4022 |
. . 3
β’ ((π β§ π₯ β πΌ) β ((πβπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯})))) β
{(0gβπΊ)}) |
74 | 1, 2, 3, 6, 8, 9, 38, 73 | dmdprdd 19864 |
. 2
β’ (π β πΊdom DProd π) |
75 | 4 | a1d 25 |
. . . . 5
β’ (π β (πΊdom DProd π β πΊdom DProd π)) |
76 | | ss2ixp 8901 |
. . . . . . 7
β’
(βπ β
πΌ (πβπ) β (πβπ) β Xπ β πΌ (πβπ) β Xπ β πΌ (πβπ)) |
77 | 11, 76 | syl 17 |
. . . . . 6
β’ (π β Xπ β
πΌ (πβπ) β Xπ β πΌ (πβπ)) |
78 | | rabss2 4075 |
. . . . . 6
β’ (Xπ β
πΌ (πβπ) β Xπ β πΌ (πβπ) β {β β Xπ β πΌ (πβπ) β£ β finSupp (0gβπΊ)} β {β β Xπ β πΌ (πβπ) β£ β finSupp (0gβπΊ)}) |
79 | | ssrexv 4051 |
. . . . . 6
β’ ({β β Xπ β
πΌ (πβπ) β£ β finSupp (0gβπΊ)} β {β β Xπ β πΌ (πβπ) β£ β finSupp (0gβπΊ)} β (βπ β {β β Xπ β πΌ (πβπ) β£ β finSupp (0gβπΊ)}π = (πΊ Ξ£g π) β βπ β {β β Xπ β πΌ (πβπ) β£ β finSupp (0gβπΊ)}π = (πΊ Ξ£g π))) |
80 | 77, 78, 79 | 3syl 18 |
. . . . 5
β’ (π β (βπ β {β β Xπ β πΌ (πβπ) β£ β finSupp (0gβπΊ)}π = (πΊ Ξ£g π) β βπ β {β β Xπ β πΌ (πβπ) β£ β finSupp (0gβπΊ)}π = (πΊ Ξ£g π))) |
81 | 75, 80 | anim12d 610 |
. . . 4
β’ (π β ((πΊdom DProd π β§ βπ β {β β Xπ β πΌ (πβπ) β£ β finSupp (0gβπΊ)}π = (πΊ Ξ£g π)) β (πΊdom DProd π β§ βπ β {β β Xπ β πΌ (πβπ) β£ β finSupp (0gβπΊ)}π = (πΊ Ξ£g π)))) |
82 | | fdm 6724 |
. . . . 5
β’ (π:πΌβΆ(SubGrpβπΊ) β dom π = πΌ) |
83 | | eqid 2733 |
. . . . . 6
β’ {β β Xπ β
πΌ (πβπ) β£ β finSupp (0gβπΊ)} = {β β Xπ β πΌ (πβπ) β£ β finSupp (0gβπΊ)} |
84 | 2, 83 | eldprd 19869 |
. . . . 5
β’ (dom
π = πΌ β (π β (πΊ DProd π) β (πΊdom DProd π β§ βπ β {β β Xπ β πΌ (πβπ) β£ β finSupp (0gβπΊ)}π = (πΊ Ξ£g π)))) |
85 | 9, 82, 84 | 3syl 18 |
. . . 4
β’ (π β (π β (πΊ DProd π) β (πΊdom DProd π β§ βπ β {β β Xπ β πΌ (πβπ) β£ β finSupp (0gβπΊ)}π = (πΊ Ξ£g π)))) |
86 | | eqid 2733 |
. . . . . 6
β’ {β β Xπ β
πΌ (πβπ) β£ β finSupp (0gβπΊ)} = {β β Xπ β πΌ (πβπ) β£ β finSupp (0gβπΊ)} |
87 | 2, 86 | eldprd 19869 |
. . . . 5
β’ (dom
π = πΌ β (π β (πΊ DProd π) β (πΊdom DProd π β§ βπ β {β β Xπ β πΌ (πβπ) β£ β finSupp (0gβπΊ)}π = (πΊ Ξ£g π)))) |
88 | 7, 87 | syl 17 |
. . . 4
β’ (π β (π β (πΊ DProd π) β (πΊdom DProd π β§ βπ β {β β Xπ β πΌ (πβπ) β£ β finSupp (0gβπΊ)}π = (πΊ Ξ£g π)))) |
89 | 81, 85, 88 | 3imtr4d 294 |
. . 3
β’ (π β (π β (πΊ DProd π) β π β (πΊ DProd π))) |
90 | 89 | ssrdv 3988 |
. 2
β’ (π β (πΊ DProd π) β (πΊ DProd π)) |
91 | 74, 90 | jca 513 |
1
β’ (π β (πΊdom DProd π β§ (πΊ DProd π) β (πΊ DProd π))) |