Step | Hyp | Ref
| Expression |
1 | | grpmnd 18862 |
. . 3
β’ (π β Grp β π β Mnd) |
2 | | cntzrec.b |
. . . 4
β’ π΅ = (Baseβπ) |
3 | | cntzrec.z |
. . . 4
β’ π = (Cntzβπ) |
4 | 2, 3 | cntzsubm 19243 |
. . 3
β’ ((π β Mnd β§ π β π΅) β (πβπ) β (SubMndβπ)) |
5 | 1, 4 | sylan 578 |
. 2
β’ ((π β Grp β§ π β π΅) β (πβπ) β (SubMndβπ)) |
6 | | simpll 763 |
. . . . . . . . . . 11
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β π β Grp) |
7 | 2, 3 | cntzssv 19233 |
. . . . . . . . . . . . 13
β’ (πβπ) β π΅ |
8 | | simprl 767 |
. . . . . . . . . . . . 13
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β π₯ β (πβπ)) |
9 | 7, 8 | sselid 3979 |
. . . . . . . . . . . 12
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β π₯ β π΅) |
10 | | eqid 2730 |
. . . . . . . . . . . . 13
β’
(invgβπ) = (invgβπ) |
11 | 2, 10 | grpinvcl 18908 |
. . . . . . . . . . . 12
β’ ((π β Grp β§ π₯ β π΅) β ((invgβπ)βπ₯) β π΅) |
12 | 6, 9, 11 | syl2anc 582 |
. . . . . . . . . . 11
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((invgβπ)βπ₯) β π΅) |
13 | | ssel2 3976 |
. . . . . . . . . . . 12
β’ ((π β π΅ β§ π¦ β π) β π¦ β π΅) |
14 | 13 | ad2ant2l 742 |
. . . . . . . . . . 11
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β π¦ β π΅) |
15 | | eqid 2730 |
. . . . . . . . . . . . 13
β’
(+gβπ) = (+gβπ) |
16 | 2, 15 | grpcl 18863 |
. . . . . . . . . . . 12
β’ ((π β Grp β§ π₯ β π΅ β§ ((invgβπ)βπ₯) β π΅) β (π₯(+gβπ)((invgβπ)βπ₯)) β π΅) |
17 | 6, 9, 12, 16 | syl3anc 1369 |
. . . . . . . . . . 11
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β (π₯(+gβπ)((invgβπ)βπ₯)) β π΅) |
18 | 2, 15 | grpass 18864 |
. . . . . . . . . . 11
β’ ((π β Grp β§
(((invgβπ)βπ₯) β π΅ β§ π¦ β π΅ β§ (π₯(+gβπ)((invgβπ)βπ₯)) β π΅)) β ((((invgβπ)βπ₯)(+gβπ)π¦)(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)(π¦(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯))))) |
19 | 6, 12, 14, 17, 18 | syl13anc 1370 |
. . . . . . . . . 10
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π¦)(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)(π¦(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯))))) |
20 | 2, 15 | grpass 18864 |
. . . . . . . . . . . 12
β’ ((π β Grp β§ (π¦ β π΅ β§ π₯ β π΅ β§ ((invgβπ)βπ₯) β π΅)) β ((π¦(+gβπ)π₯)(+gβπ)((invgβπ)βπ₯)) = (π¦(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯)))) |
21 | 6, 14, 9, 12, 20 | syl13anc 1370 |
. . . . . . . . . . 11
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((π¦(+gβπ)π₯)(+gβπ)((invgβπ)βπ₯)) = (π¦(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯)))) |
22 | 21 | oveq2d 7427 |
. . . . . . . . . 10
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β (((invgβπ)βπ₯)(+gβπ)((π¦(+gβπ)π₯)(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)(π¦(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯))))) |
23 | 19, 22 | eqtr4d 2773 |
. . . . . . . . 9
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π¦)(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)((π¦(+gβπ)π₯)(+gβπ)((invgβπ)βπ₯)))) |
24 | 15, 3 | cntzi 19234 |
. . . . . . . . . . . 12
β’ ((π₯ β (πβπ) β§ π¦ β π) β (π₯(+gβπ)π¦) = (π¦(+gβπ)π₯)) |
25 | 24 | adantl 480 |
. . . . . . . . . . 11
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β (π₯(+gβπ)π¦) = (π¦(+gβπ)π₯)) |
26 | 25 | oveq1d 7426 |
. . . . . . . . . 10
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((π₯(+gβπ)π¦)(+gβπ)((invgβπ)βπ₯)) = ((π¦(+gβπ)π₯)(+gβπ)((invgβπ)βπ₯))) |
27 | 26 | oveq2d 7427 |
. . . . . . . . 9
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β (((invgβπ)βπ₯)(+gβπ)((π₯(+gβπ)π¦)(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)((π¦(+gβπ)π₯)(+gβπ)((invgβπ)βπ₯)))) |
28 | 23, 27 | eqtr4d 2773 |
. . . . . . . 8
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π¦)(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)((π₯(+gβπ)π¦)(+gβπ)((invgβπ)βπ₯)))) |
29 | 2, 15 | grpcl 18863 |
. . . . . . . . . . 11
β’ ((π β Grp β§ π¦ β π΅ β§ ((invgβπ)βπ₯) β π΅) β (π¦(+gβπ)((invgβπ)βπ₯)) β π΅) |
30 | 6, 14, 12, 29 | syl3anc 1369 |
. . . . . . . . . 10
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β (π¦(+gβπ)((invgβπ)βπ₯)) β π΅) |
31 | 2, 15 | grpass 18864 |
. . . . . . . . . 10
β’ ((π β Grp β§
(((invgβπ)βπ₯) β π΅ β§ π₯ β π΅ β§ (π¦(+gβπ)((invgβπ)βπ₯)) β π΅)) β ((((invgβπ)βπ₯)(+gβπ)π₯)(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)(π₯(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯))))) |
32 | 6, 12, 9, 30, 31 | syl13anc 1370 |
. . . . . . . . 9
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π₯)(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)(π₯(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯))))) |
33 | 2, 15 | grpass 18864 |
. . . . . . . . . . 11
β’ ((π β Grp β§ (π₯ β π΅ β§ π¦ β π΅ β§ ((invgβπ)βπ₯) β π΅)) β ((π₯(+gβπ)π¦)(+gβπ)((invgβπ)βπ₯)) = (π₯(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯)))) |
34 | 6, 9, 14, 12, 33 | syl13anc 1370 |
. . . . . . . . . 10
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((π₯(+gβπ)π¦)(+gβπ)((invgβπ)βπ₯)) = (π₯(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯)))) |
35 | 34 | oveq2d 7427 |
. . . . . . . . 9
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β (((invgβπ)βπ₯)(+gβπ)((π₯(+gβπ)π¦)(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)(π₯(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯))))) |
36 | 32, 35 | eqtr4d 2773 |
. . . . . . . 8
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π₯)(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)((π₯(+gβπ)π¦)(+gβπ)((invgβπ)βπ₯)))) |
37 | 28, 36 | eqtr4d 2773 |
. . . . . . 7
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π¦)(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯))) = ((((invgβπ)βπ₯)(+gβπ)π₯)(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯)))) |
38 | | eqid 2730 |
. . . . . . . . . . 11
β’
(0gβπ) = (0gβπ) |
39 | 2, 15, 38, 10 | grprinv 18911 |
. . . . . . . . . 10
β’ ((π β Grp β§ π₯ β π΅) β (π₯(+gβπ)((invgβπ)βπ₯)) = (0gβπ)) |
40 | 6, 9, 39 | syl2anc 582 |
. . . . . . . . 9
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β (π₯(+gβπ)((invgβπ)βπ₯)) = (0gβπ)) |
41 | 40 | oveq2d 7427 |
. . . . . . . 8
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π¦)(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯))) = ((((invgβπ)βπ₯)(+gβπ)π¦)(+gβπ)(0gβπ))) |
42 | 2, 15 | grpcl 18863 |
. . . . . . . . . 10
β’ ((π β Grp β§
((invgβπ)βπ₯) β π΅ β§ π¦ β π΅) β (((invgβπ)βπ₯)(+gβπ)π¦) β π΅) |
43 | 6, 12, 14, 42 | syl3anc 1369 |
. . . . . . . . 9
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β (((invgβπ)βπ₯)(+gβπ)π¦) β π΅) |
44 | 2, 15, 38 | grprid 18889 |
. . . . . . . . 9
β’ ((π β Grp β§
(((invgβπ)βπ₯)(+gβπ)π¦) β π΅) β ((((invgβπ)βπ₯)(+gβπ)π¦)(+gβπ)(0gβπ)) = (((invgβπ)βπ₯)(+gβπ)π¦)) |
45 | 6, 43, 44 | syl2anc 582 |
. . . . . . . 8
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π¦)(+gβπ)(0gβπ)) = (((invgβπ)βπ₯)(+gβπ)π¦)) |
46 | 41, 45 | eqtrd 2770 |
. . . . . . 7
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π¦)(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)π¦)) |
47 | 2, 15, 38, 10 | grplinv 18910 |
. . . . . . . . . 10
β’ ((π β Grp β§ π₯ β π΅) β (((invgβπ)βπ₯)(+gβπ)π₯) = (0gβπ)) |
48 | 6, 9, 47 | syl2anc 582 |
. . . . . . . . 9
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β (((invgβπ)βπ₯)(+gβπ)π₯) = (0gβπ)) |
49 | 48 | oveq1d 7426 |
. . . . . . . 8
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π₯)(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯))) = ((0gβπ)(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯)))) |
50 | 2, 15, 38 | grplid 18888 |
. . . . . . . . 9
β’ ((π β Grp β§ (π¦(+gβπ)((invgβπ)βπ₯)) β π΅) β ((0gβπ)(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯))) = (π¦(+gβπ)((invgβπ)βπ₯))) |
51 | 6, 30, 50 | syl2anc 582 |
. . . . . . . 8
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((0gβπ)(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯))) = (π¦(+gβπ)((invgβπ)βπ₯))) |
52 | 49, 51 | eqtrd 2770 |
. . . . . . 7
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π₯)(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯))) = (π¦(+gβπ)((invgβπ)βπ₯))) |
53 | 37, 46, 52 | 3eqtr3d 2778 |
. . . . . 6
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β (((invgβπ)βπ₯)(+gβπ)π¦) = (π¦(+gβπ)((invgβπ)βπ₯))) |
54 | 53 | anassrs 466 |
. . . . 5
β’ ((((π β Grp β§ π β π΅) β§ π₯ β (πβπ)) β§ π¦ β π) β (((invgβπ)βπ₯)(+gβπ)π¦) = (π¦(+gβπ)((invgβπ)βπ₯))) |
55 | 54 | ralrimiva 3144 |
. . . 4
β’ (((π β Grp β§ π β π΅) β§ π₯ β (πβπ)) β βπ¦ β π (((invgβπ)βπ₯)(+gβπ)π¦) = (π¦(+gβπ)((invgβπ)βπ₯))) |
56 | | simplr 765 |
. . . . 5
β’ (((π β Grp β§ π β π΅) β§ π₯ β (πβπ)) β π β π΅) |
57 | | simpll 763 |
. . . . . 6
β’ (((π β Grp β§ π β π΅) β§ π₯ β (πβπ)) β π β Grp) |
58 | | simpr 483 |
. . . . . . 7
β’ (((π β Grp β§ π β π΅) β§ π₯ β (πβπ)) β π₯ β (πβπ)) |
59 | 7, 58 | sselid 3979 |
. . . . . 6
β’ (((π β Grp β§ π β π΅) β§ π₯ β (πβπ)) β π₯ β π΅) |
60 | 57, 59, 11 | syl2anc 582 |
. . . . 5
β’ (((π β Grp β§ π β π΅) β§ π₯ β (πβπ)) β ((invgβπ)βπ₯) β π΅) |
61 | 2, 15, 3 | cntzel 19228 |
. . . . 5
β’ ((π β π΅ β§ ((invgβπ)βπ₯) β π΅) β (((invgβπ)βπ₯) β (πβπ) β βπ¦ β π (((invgβπ)βπ₯)(+gβπ)π¦) = (π¦(+gβπ)((invgβπ)βπ₯)))) |
62 | 56, 60, 61 | syl2anc 582 |
. . . 4
β’ (((π β Grp β§ π β π΅) β§ π₯ β (πβπ)) β (((invgβπ)βπ₯) β (πβπ) β βπ¦ β π (((invgβπ)βπ₯)(+gβπ)π¦) = (π¦(+gβπ)((invgβπ)βπ₯)))) |
63 | 55, 62 | mpbird 256 |
. . 3
β’ (((π β Grp β§ π β π΅) β§ π₯ β (πβπ)) β ((invgβπ)βπ₯) β (πβπ)) |
64 | 63 | ralrimiva 3144 |
. 2
β’ ((π β Grp β§ π β π΅) β βπ₯ β (πβπ)((invgβπ)βπ₯) β (πβπ)) |
65 | 10 | issubg3 19060 |
. . 3
β’ (π β Grp β ((πβπ) β (SubGrpβπ) β ((πβπ) β (SubMndβπ) β§ βπ₯ β (πβπ)((invgβπ)βπ₯) β (πβπ)))) |
66 | 65 | adantr 479 |
. 2
β’ ((π β Grp β§ π β π΅) β ((πβπ) β (SubGrpβπ) β ((πβπ) β (SubMndβπ) β§ βπ₯ β (πβπ)((invgβπ)βπ₯) β (πβπ)))) |
67 | 5, 64, 66 | mpbir2and 709 |
1
β’ ((π β Grp β§ π β π΅) β (πβπ) β (SubGrpβπ)) |