Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . . . . 6
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β π
β IDomn) |
2 | | isidom 20790 |
. . . . . . 7
β’ (π
β IDomn β (π
β CRing β§ π
β Domn)) |
3 | 2 | simprbi 498 |
. . . . . 6
β’ (π
β IDomn β π
β Domn) |
4 | | domnring 20782 |
. . . . . 6
β’ (π
β Domn β π
β Ring) |
5 | | eqid 2733 |
. . . . . . 7
β’
(Unitβπ
) =
(Unitβπ
) |
6 | | idomsubgmo.g |
. . . . . . 7
β’ πΊ = ((mulGrpβπ
) βΎs
(Unitβπ
)) |
7 | 5, 6 | unitgrp 20101 |
. . . . . 6
β’ (π
β Ring β πΊ β Grp) |
8 | 1, 3, 4, 7 | 4syl 19 |
. . . . 5
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β πΊ β Grp) |
9 | | eqid 2733 |
. . . . . 6
β’
(BaseβπΊ) =
(BaseβπΊ) |
10 | 9 | subgacs 18968 |
. . . . 5
β’ (πΊ β Grp β
(SubGrpβπΊ) β
(ACSβ(BaseβπΊ))) |
11 | | acsmre 17537 |
. . . . 5
β’
((SubGrpβπΊ)
β (ACSβ(BaseβπΊ)) β (SubGrpβπΊ) β (Mooreβ(BaseβπΊ))) |
12 | 8, 10, 11 | 3syl 18 |
. . . 4
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (SubGrpβπΊ) β (Mooreβ(BaseβπΊ))) |
13 | | proot1mul.k |
. . . 4
β’ πΎ =
(mrClsβ(SubGrpβπΊ)) |
14 | | simprl 770 |
. . . . . . 7
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β π β (β‘π β {π})) |
15 | | proot1mul.o |
. . . . . . . . 9
β’ π = (odβπΊ) |
16 | 9, 15 | odf 19324 |
. . . . . . . 8
β’ π:(BaseβπΊ)βΆβ0 |
17 | | ffn 6669 |
. . . . . . . 8
β’ (π:(BaseβπΊ)βΆβ0 β π Fn (BaseβπΊ)) |
18 | | fniniseg 7011 |
. . . . . . . 8
β’ (π Fn (BaseβπΊ) β (π β (β‘π β {π}) β (π β (BaseβπΊ) β§ (πβπ) = π))) |
19 | 16, 17, 18 | mp2b 10 |
. . . . . . 7
β’ (π β (β‘π β {π}) β (π β (BaseβπΊ) β§ (πβπ) = π)) |
20 | 14, 19 | sylib 217 |
. . . . . 6
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (π β (BaseβπΊ) β§ (πβπ) = π)) |
21 | 20 | simpld 496 |
. . . . 5
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β π β (BaseβπΊ)) |
22 | 21 | snssd 4770 |
. . . 4
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β {π} β (BaseβπΊ)) |
23 | 12, 13, 22 | mrcssidd 17510 |
. . 3
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β {π} β (πΎβ{π})) |
24 | | snssg 4745 |
. . . 4
β’ (π β (β‘π β {π}) β (π β (πΎβ{π}) β {π} β (πΎβ{π}))) |
25 | 14, 24 | syl 17 |
. . 3
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (π β (πΎβ{π}) β {π} β (πΎβ{π}))) |
26 | 23, 25 | mpbird 257 |
. 2
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β π β (πΎβ{π})) |
27 | 6 | idomsubgmo 41568 |
. . . 4
β’ ((π
β IDomn β§ π β β) β
β*π₯ β
(SubGrpβπΊ)(β―βπ₯) = π) |
28 | 27 | adantr 482 |
. . 3
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β β*π₯ β (SubGrpβπΊ)(β―βπ₯) = π) |
29 | 13 | mrccl 17496 |
. . . 4
β’
(((SubGrpβπΊ)
β (Mooreβ(BaseβπΊ)) β§ {π} β (BaseβπΊ)) β (πΎβ{π}) β (SubGrpβπΊ)) |
30 | 12, 22, 29 | syl2anc 585 |
. . 3
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (πΎβ{π}) β (SubGrpβπΊ)) |
31 | 20 | simprd 497 |
. . . . . 6
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (πβπ) = π) |
32 | | simplr 768 |
. . . . . 6
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β π β β) |
33 | 31, 32 | eqeltrd 2834 |
. . . . 5
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (πβπ) β β) |
34 | 9, 15, 13 | odhash2 19362 |
. . . . 5
β’ ((πΊ β Grp β§ π β (BaseβπΊ) β§ (πβπ) β β) β
(β―β(πΎβ{π})) = (πβπ)) |
35 | 8, 21, 33, 34 | syl3anc 1372 |
. . . 4
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (β―β(πΎβ{π})) = (πβπ)) |
36 | 35, 31 | eqtrd 2773 |
. . 3
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (β―β(πΎβ{π})) = π) |
37 | | simprr 772 |
. . . . . . 7
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β π β (β‘π β {π})) |
38 | | fniniseg 7011 |
. . . . . . . 8
β’ (π Fn (BaseβπΊ) β (π β (β‘π β {π}) β (π β (BaseβπΊ) β§ (πβπ) = π))) |
39 | 16, 17, 38 | mp2b 10 |
. . . . . . 7
β’ (π β (β‘π β {π}) β (π β (BaseβπΊ) β§ (πβπ) = π)) |
40 | 37, 39 | sylib 217 |
. . . . . 6
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (π β (BaseβπΊ) β§ (πβπ) = π)) |
41 | 40 | simpld 496 |
. . . . 5
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β π β (BaseβπΊ)) |
42 | 41 | snssd 4770 |
. . . 4
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β {π} β (BaseβπΊ)) |
43 | 13 | mrccl 17496 |
. . . 4
β’
(((SubGrpβπΊ)
β (Mooreβ(BaseβπΊ)) β§ {π} β (BaseβπΊ)) β (πΎβ{π}) β (SubGrpβπΊ)) |
44 | 12, 42, 43 | syl2anc 585 |
. . 3
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (πΎβ{π}) β (SubGrpβπΊ)) |
45 | 40 | simprd 497 |
. . . . . 6
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (πβπ) = π) |
46 | 45, 32 | eqeltrd 2834 |
. . . . 5
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (πβπ) β β) |
47 | 9, 15, 13 | odhash2 19362 |
. . . . 5
β’ ((πΊ β Grp β§ π β (BaseβπΊ) β§ (πβπ) β β) β
(β―β(πΎβ{π})) = (πβπ)) |
48 | 8, 41, 46, 47 | syl3anc 1372 |
. . . 4
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (β―β(πΎβ{π})) = (πβπ)) |
49 | 48, 45 | eqtrd 2773 |
. . 3
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (β―β(πΎβ{π})) = π) |
50 | | fveqeq2 6852 |
. . . 4
β’ (π₯ = (πΎβ{π}) β ((β―βπ₯) = π β (β―β(πΎβ{π})) = π)) |
51 | | fveqeq2 6852 |
. . . 4
β’ (π₯ = (πΎβ{π}) β ((β―βπ₯) = π β (β―β(πΎβ{π})) = π)) |
52 | 50, 51 | rmoi 3848 |
. . 3
β’
((β*π₯ β
(SubGrpβπΊ)(β―βπ₯) = π β§ ((πΎβ{π}) β (SubGrpβπΊ) β§ (β―β(πΎβ{π})) = π) β§ ((πΎβ{π}) β (SubGrpβπΊ) β§ (β―β(πΎβ{π})) = π)) β (πΎβ{π}) = (πΎβ{π})) |
53 | 28, 30, 36, 44, 49, 52 | syl122anc 1380 |
. 2
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (πΎβ{π}) = (πΎβ{π})) |
54 | 26, 53 | eleqtrd 2836 |
1
β’ (((π
β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β π β (πΎβ{π})) |