Step | Hyp | Ref
| Expression |
1 | | prdsringd.y |
. . 3
β’ π = (πXsπ
) |
2 | | prdsringd.i |
. . 3
β’ (π β πΌ β π) |
3 | | prdsringd.s |
. . 3
β’ (π β π β π) |
4 | | prdsringd.r |
. . . 4
β’ (π β π
:πΌβΆRing) |
5 | | ringgrp 19977 |
. . . . 5
β’ (π₯ β Ring β π₯ β Grp) |
6 | 5 | ssriv 3952 |
. . . 4
β’ Ring
β Grp |
7 | | fss 6689 |
. . . 4
β’ ((π
:πΌβΆRing β§ Ring β Grp) β
π
:πΌβΆGrp) |
8 | 4, 6, 7 | sylancl 587 |
. . 3
β’ (π β π
:πΌβΆGrp) |
9 | 1, 2, 3, 8 | prdsgrpd 18865 |
. 2
β’ (π β π β Grp) |
10 | | eqid 2733 |
. . . 4
β’ (πXs(mulGrp β π
)) = (πXs(mulGrp β π
)) |
11 | | mgpf 19987 |
. . . . 5
β’ (mulGrp
βΎ Ring):RingβΆMnd |
12 | | fco2 6699 |
. . . . 5
β’ (((mulGrp
βΎ Ring):RingβΆMnd β§ π
:πΌβΆRing) β (mulGrp β π
):πΌβΆMnd) |
13 | 11, 4, 12 | sylancr 588 |
. . . 4
β’ (π β (mulGrp β π
):πΌβΆMnd) |
14 | 10, 2, 3, 13 | prdsmndd 18597 |
. . 3
β’ (π β (πXs(mulGrp β π
)) β Mnd) |
15 | | eqidd 2734 |
. . . 4
β’ (π β
(Baseβ(mulGrpβπ)) = (Baseβ(mulGrpβπ))) |
16 | | eqid 2733 |
. . . . . 6
β’
(mulGrpβπ) =
(mulGrpβπ) |
17 | 4 | ffnd 6673 |
. . . . . 6
β’ (π β π
Fn πΌ) |
18 | 1, 16, 10, 2, 3, 17 | prdsmgp 20042 |
. . . . 5
β’ (π β
((Baseβ(mulGrpβπ)) = (Baseβ(πXs(mulGrp β π
))) β§
(+gβ(mulGrpβπ)) = (+gβ(πXs(mulGrp β π
))))) |
19 | 18 | simpld 496 |
. . . 4
β’ (π β
(Baseβ(mulGrpβπ)) = (Baseβ(πXs(mulGrp β π
)))) |
20 | 18 | simprd 497 |
. . . . 5
β’ (π β
(+gβ(mulGrpβπ)) = (+gβ(πXs(mulGrp β π
)))) |
21 | 20 | oveqdr 7389 |
. . . 4
β’ ((π β§ (π₯ β (Baseβ(mulGrpβπ)) β§ π¦ β (Baseβ(mulGrpβπ)))) β (π₯(+gβ(mulGrpβπ))π¦) = (π₯(+gβ(πXs(mulGrp β π
)))π¦)) |
22 | 15, 19, 21 | mndpropd 18589 |
. . 3
β’ (π β ((mulGrpβπ) β Mnd β (πXs(mulGrp β π
)) β Mnd)) |
23 | 14, 22 | mpbird 257 |
. 2
β’ (π β (mulGrpβπ) β Mnd) |
24 | 4 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π
:πΌβΆRing) |
25 | 24 | ffvelcdmda 7039 |
. . . . . . . 8
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β (π
βπ€) β Ring) |
26 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
27 | 3 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π β π) |
28 | 27 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β π β π) |
29 | 2 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β πΌ β π) |
30 | 29 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β πΌ β π) |
31 | 17 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π
Fn πΌ) |
32 | 31 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β π
Fn πΌ) |
33 | | simplr1 1216 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β π₯ β (Baseβπ)) |
34 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β π€ β πΌ) |
35 | 1, 26, 28, 30, 32, 33, 34 | prdsbasprj 17362 |
. . . . . . . 8
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β (π₯βπ€) β (Baseβ(π
βπ€))) |
36 | | simpr2 1196 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π¦ β (Baseβπ)) |
37 | 36 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β π¦ β (Baseβπ)) |
38 | 1, 26, 28, 30, 32, 37, 34 | prdsbasprj 17362 |
. . . . . . . 8
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β (π¦βπ€) β (Baseβ(π
βπ€))) |
39 | | simpr3 1197 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π§ β (Baseβπ)) |
40 | 39 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β π§ β (Baseβπ)) |
41 | 1, 26, 28, 30, 32, 40, 34 | prdsbasprj 17362 |
. . . . . . . 8
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β (π§βπ€) β (Baseβ(π
βπ€))) |
42 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβ(π
βπ€)) = (Baseβ(π
βπ€)) |
43 | | eqid 2733 |
. . . . . . . . 9
β’
(+gβ(π
βπ€)) = (+gβ(π
βπ€)) |
44 | | eqid 2733 |
. . . . . . . . 9
β’
(.rβ(π
βπ€)) = (.rβ(π
βπ€)) |
45 | 42, 43, 44 | ringdi 19995 |
. . . . . . . 8
β’ (((π
βπ€) β Ring β§ ((π₯βπ€) β (Baseβ(π
βπ€)) β§ (π¦βπ€) β (Baseβ(π
βπ€)) β§ (π§βπ€) β (Baseβ(π
βπ€)))) β ((π₯βπ€)(.rβ(π
βπ€))((π¦βπ€)(+gβ(π
βπ€))(π§βπ€))) = (((π₯βπ€)(.rβ(π
βπ€))(π¦βπ€))(+gβ(π
βπ€))((π₯βπ€)(.rβ(π
βπ€))(π§βπ€)))) |
46 | 25, 35, 38, 41, 45 | syl13anc 1373 |
. . . . . . 7
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β ((π₯βπ€)(.rβ(π
βπ€))((π¦βπ€)(+gβ(π
βπ€))(π§βπ€))) = (((π₯βπ€)(.rβ(π
βπ€))(π¦βπ€))(+gβ(π
βπ€))((π₯βπ€)(.rβ(π
βπ€))(π§βπ€)))) |
47 | | eqid 2733 |
. . . . . . . . 9
β’
(+gβπ) = (+gβπ) |
48 | 1, 26, 28, 30, 32, 37, 40, 47, 34 | prdsplusgfval 17364 |
. . . . . . . 8
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β ((π¦(+gβπ)π§)βπ€) = ((π¦βπ€)(+gβ(π
βπ€))(π§βπ€))) |
49 | 48 | oveq2d 7377 |
. . . . . . 7
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β ((π₯βπ€)(.rβ(π
βπ€))((π¦(+gβπ)π§)βπ€)) = ((π₯βπ€)(.rβ(π
βπ€))((π¦βπ€)(+gβ(π
βπ€))(π§βπ€)))) |
50 | | eqid 2733 |
. . . . . . . . 9
β’
(.rβπ) = (.rβπ) |
51 | 1, 26, 28, 30, 32, 33, 37, 50, 34 | prdsmulrfval 17366 |
. . . . . . . 8
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β ((π₯(.rβπ)π¦)βπ€) = ((π₯βπ€)(.rβ(π
βπ€))(π¦βπ€))) |
52 | 1, 26, 28, 30, 32, 33, 40, 50, 34 | prdsmulrfval 17366 |
. . . . . . . 8
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β ((π₯(.rβπ)π§)βπ€) = ((π₯βπ€)(.rβ(π
βπ€))(π§βπ€))) |
53 | 51, 52 | oveq12d 7379 |
. . . . . . 7
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β (((π₯(.rβπ)π¦)βπ€)(+gβ(π
βπ€))((π₯(.rβπ)π§)βπ€)) = (((π₯βπ€)(.rβ(π
βπ€))(π¦βπ€))(+gβ(π
βπ€))((π₯βπ€)(.rβ(π
βπ€))(π§βπ€)))) |
54 | 46, 49, 53 | 3eqtr4d 2783 |
. . . . . 6
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β ((π₯βπ€)(.rβ(π
βπ€))((π¦(+gβπ)π§)βπ€)) = (((π₯(.rβπ)π¦)βπ€)(+gβ(π
βπ€))((π₯(.rβπ)π§)βπ€))) |
55 | 54 | mpteq2dva 5209 |
. . . . 5
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π€ β πΌ β¦ ((π₯βπ€)(.rβ(π
βπ€))((π¦(+gβπ)π§)βπ€))) = (π€ β πΌ β¦ (((π₯(.rβπ)π¦)βπ€)(+gβ(π
βπ€))((π₯(.rβπ)π§)βπ€)))) |
56 | | simpr1 1195 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π₯ β (Baseβπ)) |
57 | | ringmnd 19982 |
. . . . . . . . . 10
β’ (π₯ β Ring β π₯ β Mnd) |
58 | 57 | ssriv 3952 |
. . . . . . . . 9
β’ Ring
β Mnd |
59 | | fss 6689 |
. . . . . . . . 9
β’ ((π
:πΌβΆRing β§ Ring β Mnd) β
π
:πΌβΆMnd) |
60 | 4, 58, 59 | sylancl 587 |
. . . . . . . 8
β’ (π β π
:πΌβΆMnd) |
61 | 60 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π
:πΌβΆMnd) |
62 | 1, 26, 47, 27, 29, 61, 36, 39 | prdsplusgcl 18595 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π¦(+gβπ)π§) β (Baseβπ)) |
63 | 1, 26, 27, 29, 31, 56, 62, 50 | prdsmulrval 17365 |
. . . . 5
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π₯(.rβπ)(π¦(+gβπ)π§)) = (π€ β πΌ β¦ ((π₯βπ€)(.rβ(π
βπ€))((π¦(+gβπ)π§)βπ€)))) |
64 | 1, 26, 50, 27, 29, 24, 56, 36 | prdsmulrcl 20043 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π₯(.rβπ)π¦) β (Baseβπ)) |
65 | 1, 26, 50, 27, 29, 24, 56, 39 | prdsmulrcl 20043 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π₯(.rβπ)π§) β (Baseβπ)) |
66 | 1, 26, 27, 29, 31, 64, 65, 47 | prdsplusgval 17363 |
. . . . 5
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β ((π₯(.rβπ)π¦)(+gβπ)(π₯(.rβπ)π§)) = (π€ β πΌ β¦ (((π₯(.rβπ)π¦)βπ€)(+gβ(π
βπ€))((π₯(.rβπ)π§)βπ€)))) |
67 | 55, 63, 66 | 3eqtr4d 2783 |
. . . 4
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π₯(.rβπ)(π¦(+gβπ)π§)) = ((π₯(.rβπ)π¦)(+gβπ)(π₯(.rβπ)π§))) |
68 | 42, 43, 44 | ringdir 19996 |
. . . . . . . 8
β’ (((π
βπ€) β Ring β§ ((π₯βπ€) β (Baseβ(π
βπ€)) β§ (π¦βπ€) β (Baseβ(π
βπ€)) β§ (π§βπ€) β (Baseβ(π
βπ€)))) β (((π₯βπ€)(+gβ(π
βπ€))(π¦βπ€))(.rβ(π
βπ€))(π§βπ€)) = (((π₯βπ€)(.rβ(π
βπ€))(π§βπ€))(+gβ(π
βπ€))((π¦βπ€)(.rβ(π
βπ€))(π§βπ€)))) |
69 | 25, 35, 38, 41, 68 | syl13anc 1373 |
. . . . . . 7
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β (((π₯βπ€)(+gβ(π
βπ€))(π¦βπ€))(.rβ(π
βπ€))(π§βπ€)) = (((π₯βπ€)(.rβ(π
βπ€))(π§βπ€))(+gβ(π
βπ€))((π¦βπ€)(.rβ(π
βπ€))(π§βπ€)))) |
70 | 1, 26, 28, 30, 32, 33, 37, 47, 34 | prdsplusgfval 17364 |
. . . . . . . 8
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β ((π₯(+gβπ)π¦)βπ€) = ((π₯βπ€)(+gβ(π
βπ€))(π¦βπ€))) |
71 | 70 | oveq1d 7376 |
. . . . . . 7
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β (((π₯(+gβπ)π¦)βπ€)(.rβ(π
βπ€))(π§βπ€)) = (((π₯βπ€)(+gβ(π
βπ€))(π¦βπ€))(.rβ(π
βπ€))(π§βπ€))) |
72 | 1, 26, 28, 30, 32, 37, 40, 50, 34 | prdsmulrfval 17366 |
. . . . . . . 8
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β ((π¦(.rβπ)π§)βπ€) = ((π¦βπ€)(.rβ(π
βπ€))(π§βπ€))) |
73 | 52, 72 | oveq12d 7379 |
. . . . . . 7
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β (((π₯(.rβπ)π§)βπ€)(+gβ(π
βπ€))((π¦(.rβπ)π§)βπ€)) = (((π₯βπ€)(.rβ(π
βπ€))(π§βπ€))(+gβ(π
βπ€))((π¦βπ€)(.rβ(π
βπ€))(π§βπ€)))) |
74 | 69, 71, 73 | 3eqtr4d 2783 |
. . . . . 6
β’ (((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β§ π€ β πΌ) β (((π₯(+gβπ)π¦)βπ€)(.rβ(π
βπ€))(π§βπ€)) = (((π₯(.rβπ)π§)βπ€)(+gβ(π
βπ€))((π¦(.rβπ)π§)βπ€))) |
75 | 74 | mpteq2dva 5209 |
. . . . 5
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π€ β πΌ β¦ (((π₯(+gβπ)π¦)βπ€)(.rβ(π
βπ€))(π§βπ€))) = (π€ β πΌ β¦ (((π₯(.rβπ)π§)βπ€)(+gβ(π
βπ€))((π¦(.rβπ)π§)βπ€)))) |
76 | 1, 26, 47, 27, 29, 61, 56, 36 | prdsplusgcl 18595 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π₯(+gβπ)π¦) β (Baseβπ)) |
77 | 1, 26, 27, 29, 31, 76, 39, 50 | prdsmulrval 17365 |
. . . . 5
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β ((π₯(+gβπ)π¦)(.rβπ)π§) = (π€ β πΌ β¦ (((π₯(+gβπ)π¦)βπ€)(.rβ(π
βπ€))(π§βπ€)))) |
78 | 1, 26, 50, 27, 29, 24, 36, 39 | prdsmulrcl 20043 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π¦(.rβπ)π§) β (Baseβπ)) |
79 | 1, 26, 27, 29, 31, 65, 78, 47 | prdsplusgval 17363 |
. . . . 5
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β ((π₯(.rβπ)π§)(+gβπ)(π¦(.rβπ)π§)) = (π€ β πΌ β¦ (((π₯(.rβπ)π§)βπ€)(+gβ(π
βπ€))((π¦(.rβπ)π§)βπ€)))) |
80 | 75, 77, 79 | 3eqtr4d 2783 |
. . . 4
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β ((π₯(+gβπ)π¦)(.rβπ)π§) = ((π₯(.rβπ)π§)(+gβπ)(π¦(.rβπ)π§))) |
81 | 67, 80 | jca 513 |
. . 3
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β ((π₯(.rβπ)(π¦(+gβπ)π§)) = ((π₯(.rβπ)π¦)(+gβπ)(π₯(.rβπ)π§)) β§ ((π₯(+gβπ)π¦)(.rβπ)π§) = ((π₯(.rβπ)π§)(+gβπ)(π¦(.rβπ)π§)))) |
82 | 81 | ralrimivvva 3197 |
. 2
β’ (π β βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)βπ§ β (Baseβπ)((π₯(.rβπ)(π¦(+gβπ)π§)) = ((π₯(.rβπ)π¦)(+gβπ)(π₯(.rβπ)π§)) β§ ((π₯(+gβπ)π¦)(.rβπ)π§) = ((π₯(.rβπ)π§)(+gβπ)(π¦(.rβπ)π§)))) |
83 | 26, 16, 47, 50 | isring 19976 |
. 2
β’ (π β Ring β (π β Grp β§
(mulGrpβπ) β Mnd
β§ βπ₯ β
(Baseβπ)βπ¦ β (Baseβπ)βπ§ β (Baseβπ)((π₯(.rβπ)(π¦(+gβπ)π§)) = ((π₯(.rβπ)π¦)(+gβπ)(π₯(.rβπ)π§)) β§ ((π₯(+gβπ)π¦)(.rβπ)π§) = ((π₯(.rβπ)π§)(+gβπ)(π¦(.rβπ)π§))))) |
84 | 9, 23, 82, 83 | syl3anbrc 1344 |
1
β’ (π β π β Ring) |