Step | Hyp | Ref
| Expression |
1 | | dmdprdd.1 |
. 2
β’ (π β πΊ β Grp) |
2 | | dmdprdd.3 |
. 2
β’ (π β π:πΌβΆ(SubGrpβπΊ)) |
3 | | eldifsn 4790 |
. . . . . . 7
β’ (π¦ β (πΌ β {π₯}) β (π¦ β πΌ β§ π¦ β π₯)) |
4 | | necom 2994 |
. . . . . . . 8
β’ (π¦ β π₯ β π₯ β π¦) |
5 | 4 | anbi2i 623 |
. . . . . . 7
β’ ((π¦ β πΌ β§ π¦ β π₯) β (π¦ β πΌ β§ π₯ β π¦)) |
6 | 3, 5 | bitri 274 |
. . . . . 6
β’ (π¦ β (πΌ β {π₯}) β (π¦ β πΌ β§ π₯ β π¦)) |
7 | | dmdprdd.4 |
. . . . . . . 8
β’ ((π β§ (π₯ β πΌ β§ π¦ β πΌ β§ π₯ β π¦)) β (πβπ₯) β (πβ(πβπ¦))) |
8 | 7 | 3exp2 1354 |
. . . . . . 7
β’ (π β (π₯ β πΌ β (π¦ β πΌ β (π₯ β π¦ β (πβπ₯) β (πβ(πβπ¦)))))) |
9 | 8 | imp4b 422 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β ((π¦ β πΌ β§ π₯ β π¦) β (πβπ₯) β (πβ(πβπ¦)))) |
10 | 6, 9 | biimtrid 241 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β (π¦ β (πΌ β {π₯}) β (πβπ₯) β (πβ(πβπ¦)))) |
11 | 10 | ralrimiv 3145 |
. . . 4
β’ ((π β§ π₯ β πΌ) β βπ¦ β (πΌ β {π₯})(πβπ₯) β (πβ(πβπ¦))) |
12 | | dmdprdd.5 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β ((πβπ₯) β© (πΎββͺ (π β (πΌ β {π₯})))) β { 0 }) |
13 | 2 | ffvelcdmda 7086 |
. . . . . . . 8
β’ ((π β§ π₯ β πΌ) β (πβπ₯) β (SubGrpβπΊ)) |
14 | | dmdprd.0 |
. . . . . . . . 9
β’ 0 =
(0gβπΊ) |
15 | 14 | subg0cl 19050 |
. . . . . . . 8
β’ ((πβπ₯) β (SubGrpβπΊ) β 0 β (πβπ₯)) |
16 | 13, 15 | syl 17 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β 0 β (πβπ₯)) |
17 | 1 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π₯ β πΌ) β πΊ β Grp) |
18 | | eqid 2732 |
. . . . . . . . . . 11
β’
(BaseβπΊ) =
(BaseβπΊ) |
19 | 18 | subgacs 19077 |
. . . . . . . . . 10
β’ (πΊ β Grp β
(SubGrpβπΊ) β
(ACSβ(BaseβπΊ))) |
20 | | acsmre 17600 |
. . . . . . . . . 10
β’
((SubGrpβπΊ)
β (ACSβ(BaseβπΊ)) β (SubGrpβπΊ) β (Mooreβ(BaseβπΊ))) |
21 | 17, 19, 20 | 3syl 18 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΌ) β (SubGrpβπΊ) β (Mooreβ(BaseβπΊ))) |
22 | | imassrn 6070 |
. . . . . . . . . . . 12
β’ (π β (πΌ β {π₯})) β ran π |
23 | 2 | frnd 6725 |
. . . . . . . . . . . . 13
β’ (π β ran π β (SubGrpβπΊ)) |
24 | 23 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β πΌ) β ran π β (SubGrpβπΊ)) |
25 | 22, 24 | sstrid 3993 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β πΌ) β (π β (πΌ β {π₯})) β (SubGrpβπΊ)) |
26 | | mresspw 17540 |
. . . . . . . . . . . 12
β’
((SubGrpβπΊ)
β (Mooreβ(BaseβπΊ)) β (SubGrpβπΊ) β π« (BaseβπΊ)) |
27 | 21, 26 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β πΌ) β (SubGrpβπΊ) β π« (BaseβπΊ)) |
28 | 25, 27 | sstrd 3992 |
. . . . . . . . . 10
β’ ((π β§ π₯ β πΌ) β (π β (πΌ β {π₯})) β π« (BaseβπΊ)) |
29 | | sspwuni 5103 |
. . . . . . . . . 10
β’ ((π β (πΌ β {π₯})) β π« (BaseβπΊ) β βͺ (π
β (πΌ β {π₯})) β (BaseβπΊ)) |
30 | 28, 29 | sylib 217 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΌ) β βͺ (π β (πΌ β {π₯})) β (BaseβπΊ)) |
31 | | dmdprd.k |
. . . . . . . . . 10
β’ πΎ =
(mrClsβ(SubGrpβπΊ)) |
32 | 31 | mrccl 17559 |
. . . . . . . . 9
β’
(((SubGrpβπΊ)
β (Mooreβ(BaseβπΊ)) β§ βͺ (π β (πΌ β {π₯})) β (BaseβπΊ)) β (πΎββͺ (π β (πΌ β {π₯}))) β (SubGrpβπΊ)) |
33 | 21, 30, 32 | syl2anc 584 |
. . . . . . . 8
β’ ((π β§ π₯ β πΌ) β (πΎββͺ (π β (πΌ β {π₯}))) β (SubGrpβπΊ)) |
34 | 14 | subg0cl 19050 |
. . . . . . . 8
β’ ((πΎββͺ (π
β (πΌ β {π₯}))) β (SubGrpβπΊ) β 0 β (πΎββͺ (π β (πΌ β {π₯})))) |
35 | 33, 34 | syl 17 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β 0 β (πΎββͺ (π β (πΌ β {π₯})))) |
36 | 16, 35 | elind 4194 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β 0 β ((πβπ₯) β© (πΎββͺ (π β (πΌ β {π₯}))))) |
37 | 36 | snssd 4812 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β { 0 } β ((πβπ₯) β© (πΎββͺ (π β (πΌ β {π₯}))))) |
38 | 12, 37 | eqssd 3999 |
. . . 4
β’ ((π β§ π₯ β πΌ) β ((πβπ₯) β© (πΎββͺ (π β (πΌ β {π₯})))) = { 0 }) |
39 | 11, 38 | jca 512 |
. . 3
β’ ((π β§ π₯ β πΌ) β (βπ¦ β (πΌ β {π₯})(πβπ₯) β (πβ(πβπ¦)) β§ ((πβπ₯) β© (πΎββͺ (π β (πΌ β {π₯})))) = { 0 })) |
40 | 39 | ralrimiva 3146 |
. 2
β’ (π β βπ₯ β πΌ (βπ¦ β (πΌ β {π₯})(πβπ₯) β (πβ(πβπ¦)) β§ ((πβπ₯) β© (πΎββͺ (π β (πΌ β {π₯})))) = { 0 })) |
41 | | dmdprdd.2 |
. . 3
β’ (π β πΌ β π) |
42 | 2 | fdmd 6728 |
. . 3
β’ (π β dom π = πΌ) |
43 | | dmdprd.z |
. . . 4
β’ π = (CntzβπΊ) |
44 | 43, 14, 31 | dmdprd 19909 |
. . 3
β’ ((πΌ β π β§ dom π = πΌ) β (πΊdom DProd π β (πΊ β Grp β§ π:πΌβΆ(SubGrpβπΊ) β§ βπ₯ β πΌ (βπ¦ β (πΌ β {π₯})(πβπ₯) β (πβ(πβπ¦)) β§ ((πβπ₯) β© (πΎββͺ (π β (πΌ β {π₯})))) = { 0 })))) |
45 | 41, 42, 44 | syl2anc 584 |
. 2
β’ (π β (πΊdom DProd π β (πΊ β Grp β§ π:πΌβΆ(SubGrpβπΊ) β§ βπ₯ β πΌ (βπ¦ β (πΌ β {π₯})(πβπ₯) β (πβ(πβπ¦)) β§ ((πβπ₯) β© (πΎββͺ (π β (πΌ β {π₯})))) = { 0 })))) |
46 | 1, 2, 40, 45 | mpbir3and 1342 |
1
β’ (π β πΊdom DProd π) |