Step | Hyp | Ref
| Expression |
1 | | nnnn0 12428 |
. . . . . 6
β’ (π β β β π β
β0) |
2 | | cznrng.y |
. . . . . . 7
β’ π =
(β€/nβ€βπ) |
3 | 2 | zncrng 20974 |
. . . . . 6
β’ (π β β0
β π β
CRing) |
4 | 1, 3 | syl 17 |
. . . . 5
β’ (π β β β π β CRing) |
5 | | crngring 19984 |
. . . . . 6
β’ (π β CRing β π β Ring) |
6 | | cznrng.b |
. . . . . . . 8
β’ π΅ = (Baseβπ) |
7 | | cznrng.0 |
. . . . . . . 8
β’ 0 =
(0gβπ) |
8 | 6, 7 | ring0cl 19998 |
. . . . . . 7
β’ (π β Ring β 0 β π΅) |
9 | | eleq1a 2829 |
. . . . . . 7
β’ ( 0 β π΅ β (πΆ = 0 β πΆ β π΅)) |
10 | 8, 9 | syl 17 |
. . . . . 6
β’ (π β Ring β (πΆ = 0 β πΆ β π΅)) |
11 | 5, 10 | syl 17 |
. . . . 5
β’ (π β CRing β (πΆ = 0 β πΆ β π΅)) |
12 | 4, 11 | syl 17 |
. . . 4
β’ (π β β β (πΆ = 0 β πΆ β π΅)) |
13 | 12 | imp 408 |
. . 3
β’ ((π β β β§ πΆ = 0 ) β πΆ β π΅) |
14 | | cznrng.x |
. . . . . 6
β’ π = (π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©) |
15 | 2, 6, 14 | cznabel 46342 |
. . . . 5
β’ ((π β β β§ πΆ β π΅) β π β Abel) |
16 | 15 | adantlr 714 |
. . . 4
β’ (((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β π β Abel) |
17 | | eqid 2733 |
. . . . . 6
β’
(mulGrpβπ) =
(mulGrpβπ) |
18 | 2, 6, 14 | cznrnglem 46341 |
. . . . . 6
β’ π΅ = (Baseβπ) |
19 | 17, 18 | mgpbas 19910 |
. . . . 5
β’ π΅ =
(Baseβ(mulGrpβπ)) |
20 | 14 | fveq2i 6849 |
. . . . . . 7
β’
(mulGrpβπ) =
(mulGrpβ(π sSet
β¨(.rβndx), (π₯ β π΅, π¦ β π΅ β¦ πΆ)β©)) |
21 | 2 | fvexi 6860 |
. . . . . . . 8
β’ π β V |
22 | 6 | fvexi 6860 |
. . . . . . . . 9
β’ π΅ β V |
23 | 22, 22 | mpoex 8016 |
. . . . . . . 8
β’ (π₯ β π΅, π¦ β π΅ β¦ πΆ) β V |
24 | | mulrid 17183 |
. . . . . . . . 9
β’
.r = Slot (.rβndx) |
25 | 24 | setsid 17088 |
. . . . . . . 8
β’ ((π β V β§ (π₯ β π΅, π¦ β π΅ β¦ πΆ) β V) β (π₯ β π΅, π¦ β π΅ β¦ πΆ) = (.rβ(π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©))) |
26 | 21, 23, 25 | mp2an 691 |
. . . . . . 7
β’ (π₯ β π΅, π¦ β π΅ β¦ πΆ) = (.rβ(π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©)) |
27 | 20, 26 | mgpplusg 19908 |
. . . . . 6
β’ (π₯ β π΅, π¦ β π΅ β¦ πΆ) = (+gβ(mulGrpβπ)) |
28 | 27 | eqcomi 2742 |
. . . . 5
β’
(+gβ(mulGrpβπ)) = (π₯ β π΅, π¦ β π΅ β¦ πΆ) |
29 | | ne0i 4298 |
. . . . . 6
β’ (πΆ β π΅ β π΅ β β
) |
30 | 29 | adantl 483 |
. . . . 5
β’ (((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β π΅ β β
) |
31 | | simpr 486 |
. . . . 5
β’ (((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β πΆ β π΅) |
32 | 19, 28, 30, 31 | copissgrp 46192 |
. . . 4
β’ (((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β (mulGrpβπ) β Smgrp) |
33 | | oveq1 7368 |
. . . . . . . . 9
β’ (πΆ = 0 β (πΆ(+gβπ)πΆ) = ( 0 (+gβπ)πΆ)) |
34 | 33 | ad3antlr 730 |
. . . . . . . 8
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (πΆ(+gβπ)πΆ) = ( 0 (+gβπ)πΆ)) |
35 | 4, 5 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β β β π β Ring) |
36 | | ringmnd 19982 |
. . . . . . . . . . . . 13
β’ (π β Ring β π β Mnd) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . 12
β’ (π β β β π β Mnd) |
38 | 37 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β β β§ πΆ = 0 ) β π β Mnd) |
39 | 38 | anim1i 616 |
. . . . . . . . . 10
β’ (((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β (π β Mnd β§ πΆ β π΅)) |
40 | 39 | adantr 482 |
. . . . . . . . 9
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β Mnd β§ πΆ β π΅)) |
41 | | eqid 2733 |
. . . . . . . . . 10
β’
(+gβπ) = (+gβπ) |
42 | 6, 41, 7 | mndlid 18584 |
. . . . . . . . 9
β’ ((π β Mnd β§ πΆ β π΅) β ( 0 (+gβπ)πΆ) = πΆ) |
43 | 40, 42 | syl 17 |
. . . . . . . 8
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ( 0 (+gβπ)πΆ) = πΆ) |
44 | 34, 43 | eqtrd 2773 |
. . . . . . 7
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (πΆ(+gβπ)πΆ) = πΆ) |
45 | | eqidd 2734 |
. . . . . . . . 9
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π₯ β π΅, π¦ β π΅ β¦ πΆ) = (π₯ β π΅, π¦ β π΅ β¦ πΆ)) |
46 | | eqidd 2734 |
. . . . . . . . 9
β’
(((((π β
β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β§ (π₯ = π β§ π¦ = π)) β πΆ = πΆ) |
47 | | simpr1 1195 |
. . . . . . . . 9
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) |
48 | | simpr2 1196 |
. . . . . . . . 9
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) |
49 | 31 | adantr 482 |
. . . . . . . . 9
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β πΆ β π΅) |
50 | 45, 46, 47, 48, 49 | ovmpod 7511 |
. . . . . . . 8
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π) = πΆ) |
51 | | eqidd 2734 |
. . . . . . . . 9
β’
(((((π β
β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β§ (π₯ = π β§ π¦ = π)) β πΆ = πΆ) |
52 | | simpr3 1197 |
. . . . . . . . 9
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) |
53 | 45, 51, 47, 52, 49 | ovmpod 7511 |
. . . . . . . 8
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π) = πΆ) |
54 | 50, 53 | oveq12d 7379 |
. . . . . . 7
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)(+gβπ)(π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)) = (πΆ(+gβπ)πΆ)) |
55 | | eqidd 2734 |
. . . . . . . 8
β’
(((((π β
β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β§ (π₯ = π β§ π¦ = (π(+gβπ)π))) β πΆ = πΆ) |
56 | 35 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β Ring) |
57 | 6, 41 | ringacl 20007 |
. . . . . . . . 9
β’ ((π β Ring β§ π β π΅ β§ π β π΅) β (π(+gβπ)π) β π΅) |
58 | 56, 48, 52, 57 | syl3anc 1372 |
. . . . . . . 8
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π(+gβπ)π) β π΅) |
59 | 45, 55, 47, 58, 49 | ovmpod 7511 |
. . . . . . 7
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π(π₯ β π΅, π¦ β π΅ β¦ πΆ)(π(+gβπ)π)) = πΆ) |
60 | 44, 54, 59 | 3eqtr4rd 2784 |
. . . . . 6
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π(π₯ β π΅, π¦ β π΅ β¦ πΆ)(π(+gβπ)π)) = ((π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)(+gβπ)(π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π))) |
61 | | eqidd 2734 |
. . . . . . . . 9
β’
(((((π β
β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β§ (π₯ = π β§ π¦ = π)) β πΆ = πΆ) |
62 | 45, 61, 48, 52, 49 | ovmpod 7511 |
. . . . . . . 8
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π) = πΆ) |
63 | 53, 62 | oveq12d 7379 |
. . . . . . 7
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)(+gβπ)(π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)) = (πΆ(+gβπ)πΆ)) |
64 | | eqidd 2734 |
. . . . . . . 8
β’
(((((π β
β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β§ (π₯ = (π(+gβπ)π) β§ π¦ = π)) β πΆ = πΆ) |
65 | 6, 41 | ringacl 20007 |
. . . . . . . . 9
β’ ((π β Ring β§ π β π΅ β§ π β π΅) β (π(+gβπ)π) β π΅) |
66 | 56, 47, 48, 65 | syl3anc 1372 |
. . . . . . . 8
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π(+gβπ)π) β π΅) |
67 | 45, 64, 66, 52, 49 | ovmpod 7511 |
. . . . . . 7
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π(+gβπ)π)(π₯ β π΅, π¦ β π΅ β¦ πΆ)π) = πΆ) |
68 | 44, 63, 67 | 3eqtr4rd 2784 |
. . . . . 6
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π(+gβπ)π)(π₯ β π΅, π¦ β π΅ β¦ πΆ)π) = ((π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)(+gβπ)(π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π))) |
69 | 60, 68 | jca 513 |
. . . . 5
β’ ((((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π(π₯ β π΅, π¦ β π΅ β¦ πΆ)(π(+gβπ)π)) = ((π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)(+gβπ)(π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)) β§ ((π(+gβπ)π)(π₯ β π΅, π¦ β π΅ β¦ πΆ)π) = ((π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)(+gβπ)(π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)))) |
70 | 69 | ralrimivvva 3197 |
. . . 4
β’ (((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β βπ β π΅ βπ β π΅ βπ β π΅ ((π(π₯ β π΅, π¦ β π΅ β¦ πΆ)(π(+gβπ)π)) = ((π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)(+gβπ)(π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)) β§ ((π(+gβπ)π)(π₯ β π΅, π¦ β π΅ β¦ πΆ)π) = ((π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)(+gβπ)(π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)))) |
71 | 16, 32, 70 | 3jca 1129 |
. . 3
β’ (((π β β β§ πΆ = 0 ) β§ πΆ β π΅) β (π β Abel β§ (mulGrpβπ) β Smgrp β§
βπ β π΅ βπ β π΅ βπ β π΅ ((π(π₯ β π΅, π¦ β π΅ β¦ πΆ)(π(+gβπ)π)) = ((π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)(+gβπ)(π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)) β§ ((π(+gβπ)π)(π₯ β π΅, π¦ β π΅ β¦ πΆ)π) = ((π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)(+gβπ)(π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π))))) |
72 | 13, 71 | mpdan 686 |
. 2
β’ ((π β β β§ πΆ = 0 ) β (π β Abel β§
(mulGrpβπ) β
Smgrp β§ βπ
β π΅ βπ β π΅ βπ β π΅ ((π(π₯ β π΅, π¦ β π΅ β¦ πΆ)(π(+gβπ)π)) = ((π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)(+gβπ)(π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)) β§ ((π(+gβπ)π)(π₯ β π΅, π¦ β π΅ β¦ πΆ)π) = ((π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)(+gβπ)(π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π))))) |
73 | | plusgid 17168 |
. . . . 5
β’
+g = Slot (+gβndx) |
74 | | plusgndxnmulrndx 17186 |
. . . . 5
β’
(+gβndx) β
(.rβndx) |
75 | 73, 74 | setsnid 17089 |
. . . 4
β’
(+gβπ) = (+gβ(π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©)) |
76 | 14 | fveq2i 6849 |
. . . 4
β’
(+gβπ) = (+gβ(π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©)) |
77 | 75, 76 | eqtr4i 2764 |
. . 3
β’
(+gβπ) = (+gβπ) |
78 | 14 | eqcomi 2742 |
. . . . 5
β’ (π sSet
β¨(.rβndx), (π₯ β π΅, π¦ β π΅ β¦ πΆ)β©) = π |
79 | 78 | fveq2i 6849 |
. . . 4
β’
(.rβ(π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©)) = (.rβπ) |
80 | 26, 79 | eqtri 2761 |
. . 3
β’ (π₯ β π΅, π¦ β π΅ β¦ πΆ) = (.rβπ) |
81 | 18, 17, 77, 80 | isrng 46264 |
. 2
β’ (π β Rng β (π β Abel β§
(mulGrpβπ) β
Smgrp β§ βπ
β π΅ βπ β π΅ βπ β π΅ ((π(π₯ β π΅, π¦ β π΅ β¦ πΆ)(π(+gβπ)π)) = ((π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)(+gβπ)(π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)) β§ ((π(+gβπ)π)(π₯ β π΅, π¦ β π΅ β¦ πΆ)π) = ((π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π)(+gβπ)(π(π₯ β π΅, π¦ β π΅ β¦ πΆ)π))))) |
82 | 72, 81 | sylibr 233 |
1
β’ ((π β β β§ πΆ = 0 ) β π β Rng) |