Step | Hyp | Ref
| Expression |
1 | | grpmnd 18826 |
. . 3
β’ (π β Grp β π β Mnd) |
2 | | cntzrec.b |
. . . 4
β’ π΅ = (Baseβπ) |
3 | | cntzrec.z |
. . . 4
β’ π = (Cntzβπ) |
4 | 2, 3 | cntzsubm 19202 |
. . 3
β’ ((π β Mnd β§ π β π΅) β (πβπ) β (SubMndβπ)) |
5 | 1, 4 | sylan 581 |
. 2
β’ ((π β Grp β§ π β π΅) β (πβπ) β (SubMndβπ)) |
6 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β π β Grp) |
7 | 2, 3 | cntzssv 19192 |
. . . . . . . . . . . . 13
β’ (πβπ) β π΅ |
8 | | simprl 770 |
. . . . . . . . . . . . 13
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β π₯ β (πβπ)) |
9 | 7, 8 | sselid 3981 |
. . . . . . . . . . . 12
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β π₯ β π΅) |
10 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(invgβπ) = (invgβπ) |
11 | 2, 10 | grpinvcl 18872 |
. . . . . . . . . . . 12
β’ ((π β Grp β§ π₯ β π΅) β ((invgβπ)βπ₯) β π΅) |
12 | 6, 9, 11 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((invgβπ)βπ₯) β π΅) |
13 | | ssel2 3978 |
. . . . . . . . . . . 12
β’ ((π β π΅ β§ π¦ β π) β π¦ β π΅) |
14 | 13 | ad2ant2l 745 |
. . . . . . . . . . 11
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β π¦ β π΅) |
15 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(+gβπ) = (+gβπ) |
16 | 2, 15 | grpcl 18827 |
. . . . . . . . . . . 12
β’ ((π β Grp β§ π₯ β π΅ β§ ((invgβπ)βπ₯) β π΅) β (π₯(+gβπ)((invgβπ)βπ₯)) β π΅) |
17 | 6, 9, 12, 16 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β (π₯(+gβπ)((invgβπ)βπ₯)) β π΅) |
18 | 2, 15 | grpass 18828 |
. . . . . . . . . . 11
β’ ((π β Grp β§
(((invgβπ)βπ₯) β π΅ β§ π¦ β π΅ β§ (π₯(+gβπ)((invgβπ)βπ₯)) β π΅)) β ((((invgβπ)βπ₯)(+gβπ)π¦)(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)(π¦(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯))))) |
19 | 6, 12, 14, 17, 18 | syl13anc 1373 |
. . . . . . . . . 10
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π¦)(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)(π¦(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯))))) |
20 | 2, 15 | grpass 18828 |
. . . . . . . . . . . 12
β’ ((π β Grp β§ (π¦ β π΅ β§ π₯ β π΅ β§ ((invgβπ)βπ₯) β π΅)) β ((π¦(+gβπ)π₯)(+gβπ)((invgβπ)βπ₯)) = (π¦(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯)))) |
21 | 6, 14, 9, 12, 20 | syl13anc 1373 |
. . . . . . . . . . 11
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((π¦(+gβπ)π₯)(+gβπ)((invgβπ)βπ₯)) = (π¦(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯)))) |
22 | 21 | oveq2d 7425 |
. . . . . . . . . 10
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β (((invgβπ)βπ₯)(+gβπ)((π¦(+gβπ)π₯)(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)(π¦(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯))))) |
23 | 19, 22 | eqtr4d 2776 |
. . . . . . . . 9
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π¦)(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)((π¦(+gβπ)π₯)(+gβπ)((invgβπ)βπ₯)))) |
24 | 15, 3 | cntzi 19193 |
. . . . . . . . . . . 12
β’ ((π₯ β (πβπ) β§ π¦ β π) β (π₯(+gβπ)π¦) = (π¦(+gβπ)π₯)) |
25 | 24 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β (π₯(+gβπ)π¦) = (π¦(+gβπ)π₯)) |
26 | 25 | oveq1d 7424 |
. . . . . . . . . 10
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((π₯(+gβπ)π¦)(+gβπ)((invgβπ)βπ₯)) = ((π¦(+gβπ)π₯)(+gβπ)((invgβπ)βπ₯))) |
27 | 26 | oveq2d 7425 |
. . . . . . . . 9
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β (((invgβπ)βπ₯)(+gβπ)((π₯(+gβπ)π¦)(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)((π¦(+gβπ)π₯)(+gβπ)((invgβπ)βπ₯)))) |
28 | 23, 27 | eqtr4d 2776 |
. . . . . . . 8
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π¦)(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)((π₯(+gβπ)π¦)(+gβπ)((invgβπ)βπ₯)))) |
29 | 2, 15 | grpcl 18827 |
. . . . . . . . . . 11
β’ ((π β Grp β§ π¦ β π΅ β§ ((invgβπ)βπ₯) β π΅) β (π¦(+gβπ)((invgβπ)βπ₯)) β π΅) |
30 | 6, 14, 12, 29 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β (π¦(+gβπ)((invgβπ)βπ₯)) β π΅) |
31 | 2, 15 | grpass 18828 |
. . . . . . . . . 10
β’ ((π β Grp β§
(((invgβπ)βπ₯) β π΅ β§ π₯ β π΅ β§ (π¦(+gβπ)((invgβπ)βπ₯)) β π΅)) β ((((invgβπ)βπ₯)(+gβπ)π₯)(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)(π₯(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯))))) |
32 | 6, 12, 9, 30, 31 | syl13anc 1373 |
. . . . . . . . 9
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π₯)(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)(π₯(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯))))) |
33 | 2, 15 | grpass 18828 |
. . . . . . . . . . 11
β’ ((π β Grp β§ (π₯ β π΅ β§ π¦ β π΅ β§ ((invgβπ)βπ₯) β π΅)) β ((π₯(+gβπ)π¦)(+gβπ)((invgβπ)βπ₯)) = (π₯(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯)))) |
34 | 6, 9, 14, 12, 33 | syl13anc 1373 |
. . . . . . . . . 10
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((π₯(+gβπ)π¦)(+gβπ)((invgβπ)βπ₯)) = (π₯(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯)))) |
35 | 34 | oveq2d 7425 |
. . . . . . . . 9
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β (((invgβπ)βπ₯)(+gβπ)((π₯(+gβπ)π¦)(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)(π₯(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯))))) |
36 | 32, 35 | eqtr4d 2776 |
. . . . . . . 8
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π₯)(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)((π₯(+gβπ)π¦)(+gβπ)((invgβπ)βπ₯)))) |
37 | 28, 36 | eqtr4d 2776 |
. . . . . . 7
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π¦)(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯))) = ((((invgβπ)βπ₯)(+gβπ)π₯)(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯)))) |
38 | | eqid 2733 |
. . . . . . . . . . 11
β’
(0gβπ) = (0gβπ) |
39 | 2, 15, 38, 10 | grprinv 18875 |
. . . . . . . . . 10
β’ ((π β Grp β§ π₯ β π΅) β (π₯(+gβπ)((invgβπ)βπ₯)) = (0gβπ)) |
40 | 6, 9, 39 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β (π₯(+gβπ)((invgβπ)βπ₯)) = (0gβπ)) |
41 | 40 | oveq2d 7425 |
. . . . . . . 8
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π¦)(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯))) = ((((invgβπ)βπ₯)(+gβπ)π¦)(+gβπ)(0gβπ))) |
42 | 2, 15 | grpcl 18827 |
. . . . . . . . . 10
β’ ((π β Grp β§
((invgβπ)βπ₯) β π΅ β§ π¦ β π΅) β (((invgβπ)βπ₯)(+gβπ)π¦) β π΅) |
43 | 6, 12, 14, 42 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β (((invgβπ)βπ₯)(+gβπ)π¦) β π΅) |
44 | 2, 15, 38 | grprid 18853 |
. . . . . . . . 9
β’ ((π β Grp β§
(((invgβπ)βπ₯)(+gβπ)π¦) β π΅) β ((((invgβπ)βπ₯)(+gβπ)π¦)(+gβπ)(0gβπ)) = (((invgβπ)βπ₯)(+gβπ)π¦)) |
45 | 6, 43, 44 | syl2anc 585 |
. . . . . . . 8
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π¦)(+gβπ)(0gβπ)) = (((invgβπ)βπ₯)(+gβπ)π¦)) |
46 | 41, 45 | eqtrd 2773 |
. . . . . . 7
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π¦)(+gβπ)(π₯(+gβπ)((invgβπ)βπ₯))) = (((invgβπ)βπ₯)(+gβπ)π¦)) |
47 | 2, 15, 38, 10 | grplinv 18874 |
. . . . . . . . . 10
β’ ((π β Grp β§ π₯ β π΅) β (((invgβπ)βπ₯)(+gβπ)π₯) = (0gβπ)) |
48 | 6, 9, 47 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β (((invgβπ)βπ₯)(+gβπ)π₯) = (0gβπ)) |
49 | 48 | oveq1d 7424 |
. . . . . . . 8
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π₯)(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯))) = ((0gβπ)(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯)))) |
50 | 2, 15, 38 | grplid 18852 |
. . . . . . . . 9
β’ ((π β Grp β§ (π¦(+gβπ)((invgβπ)βπ₯)) β π΅) β ((0gβπ)(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯))) = (π¦(+gβπ)((invgβπ)βπ₯))) |
51 | 6, 30, 50 | syl2anc 585 |
. . . . . . . 8
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((0gβπ)(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯))) = (π¦(+gβπ)((invgβπ)βπ₯))) |
52 | 49, 51 | eqtrd 2773 |
. . . . . . 7
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β ((((invgβπ)βπ₯)(+gβπ)π₯)(+gβπ)(π¦(+gβπ)((invgβπ)βπ₯))) = (π¦(+gβπ)((invgβπ)βπ₯))) |
53 | 37, 46, 52 | 3eqtr3d 2781 |
. . . . . 6
β’ (((π β Grp β§ π β π΅) β§ (π₯ β (πβπ) β§ π¦ β π)) β (((invgβπ)βπ₯)(+gβπ)π¦) = (π¦(+gβπ)((invgβπ)βπ₯))) |
54 | 53 | anassrs 469 |
. . . . 5
β’ ((((π β Grp β§ π β π΅) β§ π₯ β (πβπ)) β§ π¦ β π) β (((invgβπ)βπ₯)(+gβπ)π¦) = (π¦(+gβπ)((invgβπ)βπ₯))) |
55 | 54 | ralrimiva 3147 |
. . . 4
β’ (((π β Grp β§ π β π΅) β§ π₯ β (πβπ)) β βπ¦ β π (((invgβπ)βπ₯)(+gβπ)π¦) = (π¦(+gβπ)((invgβπ)βπ₯))) |
56 | | simplr 768 |
. . . . 5
β’ (((π β Grp β§ π β π΅) β§ π₯ β (πβπ)) β π β π΅) |
57 | | simpll 766 |
. . . . . 6
β’ (((π β Grp β§ π β π΅) β§ π₯ β (πβπ)) β π β Grp) |
58 | | simpr 486 |
. . . . . . 7
β’ (((π β Grp β§ π β π΅) β§ π₯ β (πβπ)) β π₯ β (πβπ)) |
59 | 7, 58 | sselid 3981 |
. . . . . 6
β’ (((π β Grp β§ π β π΅) β§ π₯ β (πβπ)) β π₯ β π΅) |
60 | 57, 59, 11 | syl2anc 585 |
. . . . 5
β’ (((π β Grp β§ π β π΅) β§ π₯ β (πβπ)) β ((invgβπ)βπ₯) β π΅) |
61 | 2, 15, 3 | cntzel 19187 |
. . . . 5
β’ ((π β π΅ β§ ((invgβπ)βπ₯) β π΅) β (((invgβπ)βπ₯) β (πβπ) β βπ¦ β π (((invgβπ)βπ₯)(+gβπ)π¦) = (π¦(+gβπ)((invgβπ)βπ₯)))) |
62 | 56, 60, 61 | syl2anc 585 |
. . . 4
β’ (((π β Grp β§ π β π΅) β§ π₯ β (πβπ)) β (((invgβπ)βπ₯) β (πβπ) β βπ¦ β π (((invgβπ)βπ₯)(+gβπ)π¦) = (π¦(+gβπ)((invgβπ)βπ₯)))) |
63 | 55, 62 | mpbird 257 |
. . 3
β’ (((π β Grp β§ π β π΅) β§ π₯ β (πβπ)) β ((invgβπ)βπ₯) β (πβπ)) |
64 | 63 | ralrimiva 3147 |
. 2
β’ ((π β Grp β§ π β π΅) β βπ₯ β (πβπ)((invgβπ)βπ₯) β (πβπ)) |
65 | 10 | issubg3 19024 |
. . 3
β’ (π β Grp β ((πβπ) β (SubGrpβπ) β ((πβπ) β (SubMndβπ) β§ βπ₯ β (πβπ)((invgβπ)βπ₯) β (πβπ)))) |
66 | 65 | adantr 482 |
. 2
β’ ((π β Grp β§ π β π΅) β ((πβπ) β (SubGrpβπ) β ((πβπ) β (SubMndβπ) β§ βπ₯ β (πβπ)((invgβπ)βπ₯) β (πβπ)))) |
67 | 5, 64, 66 | mpbir2and 712 |
1
β’ ((π β Grp β§ π β π΅) β (πβπ) β (SubGrpβπ)) |