Step | Hyp | Ref
| Expression |
1 | | cntzsubr.m |
. . . . . 6
β’ π = (mulGrpβπ
) |
2 | | cntzsubr.b |
. . . . . 6
β’ π΅ = (Baseβπ
) |
3 | 1, 2 | mgpbas 20045 |
. . . . 5
β’ π΅ = (Baseβπ) |
4 | | cntzsubr.z |
. . . . 5
β’ π = (Cntzβπ) |
5 | 3, 4 | cntzssv 19244 |
. . . 4
β’ (πβπ) β π΅ |
6 | 5 | a1i 11 |
. . 3
β’ ((π
β Ring β§ π β π΅) β (πβπ) β π΅) |
7 | | simpll 764 |
. . . . . . . 8
β’ (((π
β Ring β§ π β π΅) β§ π§ β π) β π
β Ring) |
8 | | ssel2 3972 |
. . . . . . . . 9
β’ ((π β π΅ β§ π§ β π) β π§ β π΅) |
9 | 8 | adantll 711 |
. . . . . . . 8
β’ (((π
β Ring β§ π β π΅) β§ π§ β π) β π§ β π΅) |
10 | | eqid 2726 |
. . . . . . . . 9
β’
(.rβπ
) = (.rβπ
) |
11 | | eqid 2726 |
. . . . . . . . 9
β’
(0gβπ
) = (0gβπ
) |
12 | 2, 10, 11 | ringlz 20192 |
. . . . . . . 8
β’ ((π
β Ring β§ π§ β π΅) β ((0gβπ
)(.rβπ
)π§) = (0gβπ
)) |
13 | 7, 9, 12 | syl2anc 583 |
. . . . . . 7
β’ (((π
β Ring β§ π β π΅) β§ π§ β π) β ((0gβπ
)(.rβπ
)π§) = (0gβπ
)) |
14 | 2, 10, 11 | ringrz 20193 |
. . . . . . . 8
β’ ((π
β Ring β§ π§ β π΅) β (π§(.rβπ
)(0gβπ
)) = (0gβπ
)) |
15 | 7, 9, 14 | syl2anc 583 |
. . . . . . 7
β’ (((π
β Ring β§ π β π΅) β§ π§ β π) β (π§(.rβπ
)(0gβπ
)) = (0gβπ
)) |
16 | 13, 15 | eqtr4d 2769 |
. . . . . 6
β’ (((π
β Ring β§ π β π΅) β§ π§ β π) β ((0gβπ
)(.rβπ
)π§) = (π§(.rβπ
)(0gβπ
))) |
17 | 16 | ralrimiva 3140 |
. . . . 5
β’ ((π
β Ring β§ π β π΅) β βπ§ β π ((0gβπ
)(.rβπ
)π§) = (π§(.rβπ
)(0gβπ
))) |
18 | | simpr 484 |
. . . . . 6
β’ ((π
β Ring β§ π β π΅) β π β π΅) |
19 | 2, 11 | ring0cl 20166 |
. . . . . . 7
β’ (π
β Ring β
(0gβπ
)
β π΅) |
20 | 19 | adantr 480 |
. . . . . 6
β’ ((π
β Ring β§ π β π΅) β (0gβπ
) β π΅) |
21 | 1, 10 | mgpplusg 20043 |
. . . . . . 7
β’
(.rβπ
) = (+gβπ) |
22 | 3, 21, 4 | cntzel 19239 |
. . . . . 6
β’ ((π β π΅ β§ (0gβπ
) β π΅) β ((0gβπ
) β (πβπ) β βπ§ β π ((0gβπ
)(.rβπ
)π§) = (π§(.rβπ
)(0gβπ
)))) |
23 | 18, 20, 22 | syl2anc 583 |
. . . . 5
β’ ((π
β Ring β§ π β π΅) β ((0gβπ
) β (πβπ) β βπ§ β π ((0gβπ
)(.rβπ
)π§) = (π§(.rβπ
)(0gβπ
)))) |
24 | 17, 23 | mpbird 257 |
. . . 4
β’ ((π
β Ring β§ π β π΅) β (0gβπ
) β (πβπ)) |
25 | 24 | ne0d 4330 |
. . 3
β’ ((π
β Ring β§ π β π΅) β (πβπ) β β
) |
26 | | simpl2 1189 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β§ π§ β π) β π₯ β (πβπ)) |
27 | | simpr 484 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β§ π§ β π) β π§ β π) |
28 | 21, 4 | cntzi 19245 |
. . . . . . . . . . . 12
β’ ((π₯ β (πβπ) β§ π§ β π) β (π₯(.rβπ
)π§) = (π§(.rβπ
)π₯)) |
29 | 26, 27, 28 | syl2anc 583 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β§ π§ β π) β (π₯(.rβπ
)π§) = (π§(.rβπ
)π₯)) |
30 | | simpl3 1190 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β§ π§ β π) β π¦ β (πβπ)) |
31 | 21, 4 | cntzi 19245 |
. . . . . . . . . . . 12
β’ ((π¦ β (πβπ) β§ π§ β π) β (π¦(.rβπ
)π§) = (π§(.rβπ
)π¦)) |
32 | 30, 27, 31 | syl2anc 583 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β§ π§ β π) β (π¦(.rβπ
)π§) = (π§(.rβπ
)π¦)) |
33 | 29, 32 | oveq12d 7423 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β§ π§ β π) β ((π₯(.rβπ
)π§)(+gβπ
)(π¦(.rβπ
)π§)) = ((π§(.rβπ
)π₯)(+gβπ
)(π§(.rβπ
)π¦))) |
34 | | simpl1l 1221 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β§ π§ β π) β π
β Ring) |
35 | 5, 26 | sselid 3975 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β§ π§ β π) β π₯ β π΅) |
36 | 5, 30 | sselid 3975 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β§ π§ β π) β π¦ β π΅) |
37 | | simp1r 1195 |
. . . . . . . . . . . 12
β’ (((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β π β π΅) |
38 | 37 | sselda 3977 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β§ π§ β π) β π§ β π΅) |
39 | | eqid 2726 |
. . . . . . . . . . . 12
β’
(+gβπ
) = (+gβπ
) |
40 | 2, 39, 10 | ringdir 20164 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯(+gβπ
)π¦)(.rβπ
)π§) = ((π₯(.rβπ
)π§)(+gβπ
)(π¦(.rβπ
)π§))) |
41 | 34, 35, 36, 38, 40 | syl13anc 1369 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β§ π§ β π) β ((π₯(+gβπ
)π¦)(.rβπ
)π§) = ((π₯(.rβπ
)π§)(+gβπ
)(π¦(.rβπ
)π§))) |
42 | 2, 39, 10 | ringdi 20163 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ (π§ β π΅ β§ π₯ β π΅ β§ π¦ β π΅)) β (π§(.rβπ
)(π₯(+gβπ
)π¦)) = ((π§(.rβπ
)π₯)(+gβπ
)(π§(.rβπ
)π¦))) |
43 | 34, 38, 35, 36, 42 | syl13anc 1369 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β§ π§ β π) β (π§(.rβπ
)(π₯(+gβπ
)π¦)) = ((π§(.rβπ
)π₯)(+gβπ
)(π§(.rβπ
)π¦))) |
44 | 33, 41, 43 | 3eqtr4d 2776 |
. . . . . . . . 9
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β§ π§ β π) β ((π₯(+gβπ
)π¦)(.rβπ
)π§) = (π§(.rβπ
)(π₯(+gβπ
)π¦))) |
45 | 44 | ralrimiva 3140 |
. . . . . . . 8
β’ (((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β βπ§ β π ((π₯(+gβπ
)π¦)(.rβπ
)π§) = (π§(.rβπ
)(π₯(+gβπ
)π¦))) |
46 | | simp1l 1194 |
. . . . . . . . . 10
β’ (((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β π
β Ring) |
47 | | simp2 1134 |
. . . . . . . . . . 11
β’ (((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β π₯ β (πβπ)) |
48 | 5, 47 | sselid 3975 |
. . . . . . . . . 10
β’ (((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β π₯ β π΅) |
49 | | simp3 1135 |
. . . . . . . . . . 11
β’ (((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β π¦ β (πβπ)) |
50 | 5, 49 | sselid 3975 |
. . . . . . . . . 10
β’ (((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β π¦ β π΅) |
51 | 2, 39 | ringacl 20177 |
. . . . . . . . . 10
β’ ((π
β Ring β§ π₯ β π΅ β§ π¦ β π΅) β (π₯(+gβπ
)π¦) β π΅) |
52 | 46, 48, 50, 51 | syl3anc 1368 |
. . . . . . . . 9
β’ (((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β (π₯(+gβπ
)π¦) β π΅) |
53 | 3, 21, 4 | cntzel 19239 |
. . . . . . . . 9
β’ ((π β π΅ β§ (π₯(+gβπ
)π¦) β π΅) β ((π₯(+gβπ
)π¦) β (πβπ) β βπ§ β π ((π₯(+gβπ
)π¦)(.rβπ
)π§) = (π§(.rβπ
)(π₯(+gβπ
)π¦)))) |
54 | 37, 52, 53 | syl2anc 583 |
. . . . . . . 8
β’ (((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β ((π₯(+gβπ
)π¦) β (πβπ) β βπ§ β π ((π₯(+gβπ
)π¦)(.rβπ
)π§) = (π§(.rβπ
)(π₯(+gβπ
)π¦)))) |
55 | 45, 54 | mpbird 257 |
. . . . . . 7
β’ (((π
β Ring β§ π β π΅) β§ π₯ β (πβπ) β§ π¦ β (πβπ)) β (π₯(+gβπ
)π¦) β (πβπ)) |
56 | 55 | 3expa 1115 |
. . . . . 6
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ)) β§ π¦ β (πβπ)) β (π₯(+gβπ
)π¦) β (πβπ)) |
57 | 56 | ralrimiva 3140 |
. . . . 5
β’ (((π
β Ring β§ π β π΅) β§ π₯ β (πβπ)) β βπ¦ β (πβπ)(π₯(+gβπ
)π¦) β (πβπ)) |
58 | 28 | adantll 711 |
. . . . . . . . 9
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ)) β§ π§ β π) β (π₯(.rβπ
)π§) = (π§(.rβπ
)π₯)) |
59 | 58 | fveq2d 6889 |
. . . . . . . 8
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ)) β§ π§ β π) β ((invgβπ
)β(π₯(.rβπ
)π§)) = ((invgβπ
)β(π§(.rβπ
)π₯))) |
60 | | eqid 2726 |
. . . . . . . . 9
β’
(invgβπ
) = (invgβπ
) |
61 | | simplll 772 |
. . . . . . . . 9
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ)) β§ π§ β π) β π
β Ring) |
62 | | simplr 766 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ)) β§ π§ β π) β π₯ β (πβπ)) |
63 | 5, 62 | sselid 3975 |
. . . . . . . . 9
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ)) β§ π§ β π) β π₯ β π΅) |
64 | | simplr 766 |
. . . . . . . . . 10
β’ (((π
β Ring β§ π β π΅) β§ π₯ β (πβπ)) β π β π΅) |
65 | 64 | sselda 3977 |
. . . . . . . . 9
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ)) β§ π§ β π) β π§ β π΅) |
66 | 2, 10, 60, 61, 63, 65 | ringmneg1 20203 |
. . . . . . . 8
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ)) β§ π§ β π) β (((invgβπ
)βπ₯)(.rβπ
)π§) = ((invgβπ
)β(π₯(.rβπ
)π§))) |
67 | 2, 10, 60, 61, 65, 63 | ringmneg2 20204 |
. . . . . . . 8
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ)) β§ π§ β π) β (π§(.rβπ
)((invgβπ
)βπ₯)) = ((invgβπ
)β(π§(.rβπ
)π₯))) |
68 | 59, 66, 67 | 3eqtr4d 2776 |
. . . . . . 7
β’ ((((π
β Ring β§ π β π΅) β§ π₯ β (πβπ)) β§ π§ β π) β (((invgβπ
)βπ₯)(.rβπ
)π§) = (π§(.rβπ
)((invgβπ
)βπ₯))) |
69 | 68 | ralrimiva 3140 |
. . . . . 6
β’ (((π
β Ring β§ π β π΅) β§ π₯ β (πβπ)) β βπ§ β π (((invgβπ
)βπ₯)(.rβπ
)π§) = (π§(.rβπ
)((invgβπ
)βπ₯))) |
70 | | ringgrp 20143 |
. . . . . . . . 9
β’ (π
β Ring β π
β Grp) |
71 | 70 | ad2antrr 723 |
. . . . . . . 8
β’ (((π
β Ring β§ π β π΅) β§ π₯ β (πβπ)) β π
β Grp) |
72 | | simpr 484 |
. . . . . . . . 9
β’ (((π
β Ring β§ π β π΅) β§ π₯ β (πβπ)) β π₯ β (πβπ)) |
73 | 5, 72 | sselid 3975 |
. . . . . . . 8
β’ (((π
β Ring β§ π β π΅) β§ π₯ β (πβπ)) β π₯ β π΅) |
74 | 2, 60 | grpinvcl 18917 |
. . . . . . . 8
β’ ((π
β Grp β§ π₯ β π΅) β ((invgβπ
)βπ₯) β π΅) |
75 | 71, 73, 74 | syl2anc 583 |
. . . . . . 7
β’ (((π
β Ring β§ π β π΅) β§ π₯ β (πβπ)) β ((invgβπ
)βπ₯) β π΅) |
76 | 3, 21, 4 | cntzel 19239 |
. . . . . . 7
β’ ((π β π΅ β§ ((invgβπ
)βπ₯) β π΅) β (((invgβπ
)βπ₯) β (πβπ) β βπ§ β π (((invgβπ
)βπ₯)(.rβπ
)π§) = (π§(.rβπ
)((invgβπ
)βπ₯)))) |
77 | 64, 75, 76 | syl2anc 583 |
. . . . . 6
β’ (((π
β Ring β§ π β π΅) β§ π₯ β (πβπ)) β (((invgβπ
)βπ₯) β (πβπ) β βπ§ β π (((invgβπ
)βπ₯)(.rβπ
)π§) = (π§(.rβπ
)((invgβπ
)βπ₯)))) |
78 | 69, 77 | mpbird 257 |
. . . . 5
β’ (((π
β Ring β§ π β π΅) β§ π₯ β (πβπ)) β ((invgβπ
)βπ₯) β (πβπ)) |
79 | 57, 78 | jca 511 |
. . . 4
β’ (((π
β Ring β§ π β π΅) β§ π₯ β (πβπ)) β (βπ¦ β (πβπ)(π₯(+gβπ
)π¦) β (πβπ) β§ ((invgβπ
)βπ₯) β (πβπ))) |
80 | 79 | ralrimiva 3140 |
. . 3
β’ ((π
β Ring β§ π β π΅) β βπ₯ β (πβπ)(βπ¦ β (πβπ)(π₯(+gβπ
)π¦) β (πβπ) β§ ((invgβπ
)βπ₯) β (πβπ))) |
81 | 70 | adantr 480 |
. . . 4
β’ ((π
β Ring β§ π β π΅) β π
β Grp) |
82 | 2, 39, 60 | issubg2 19068 |
. . . 4
β’ (π
β Grp β ((πβπ) β (SubGrpβπ
) β ((πβπ) β π΅ β§ (πβπ) β β
β§ βπ₯ β (πβπ)(βπ¦ β (πβπ)(π₯(+gβπ
)π¦) β (πβπ) β§ ((invgβπ
)βπ₯) β (πβπ))))) |
83 | 81, 82 | syl 17 |
. . 3
β’ ((π
β Ring β§ π β π΅) β ((πβπ) β (SubGrpβπ
) β ((πβπ) β π΅ β§ (πβπ) β β
β§ βπ₯ β (πβπ)(βπ¦ β (πβπ)(π₯(+gβπ
)π¦) β (πβπ) β§ ((invgβπ
)βπ₯) β (πβπ))))) |
84 | 6, 25, 80, 83 | mpbir3and 1339 |
. 2
β’ ((π
β Ring β§ π β π΅) β (πβπ) β (SubGrpβπ
)) |
85 | 1 | ringmgp 20144 |
. . 3
β’ (π
β Ring β π β Mnd) |
86 | 3, 4 | cntzsubm 19254 |
. . 3
β’ ((π β Mnd β§ π β π΅) β (πβπ) β (SubMndβπ)) |
87 | 85, 86 | sylan 579 |
. 2
β’ ((π
β Ring β§ π β π΅) β (πβπ) β (SubMndβπ)) |
88 | 1 | issubrg3 20502 |
. . 3
β’ (π
β Ring β ((πβπ) β (SubRingβπ
) β ((πβπ) β (SubGrpβπ
) β§ (πβπ) β (SubMndβπ)))) |
89 | 88 | adantr 480 |
. 2
β’ ((π
β Ring β§ π β π΅) β ((πβπ) β (SubRingβπ
) β ((πβπ) β (SubGrpβπ
) β§ (πβπ) β (SubMndβπ)))) |
90 | 84, 87, 89 | mpbir2and 710 |
1
β’ ((π
β Ring β§ π β π΅) β (πβπ) β (SubRingβπ
)) |