Step | Hyp | Ref
| Expression |
1 | | prdsringd.y |
. . 3
s |
2 | | prdsringd.i |
. . 3
|
3 | | prdsringd.s |
. . 3
|
4 | | prdsringd.r |
. . . 4
|
5 | | ringgrp 18552 |
. . . . 5
|
6 | 5 | ssriv 3607 |
. . . 4
|
7 | | fss 6056 |
. . . 4
|
8 | 4, 6, 7 | sylancl 694 |
. . 3
|
9 | 1, 2, 3, 8 | prdsgrpd 17525 |
. 2
|
10 | | eqid 2622 |
. . . 4
smulGrp
smulGrp
|
11 | | mgpf 18559 |
. . . . 5
mulGrp |
12 | | fco2 6059 |
. . . . 5
mulGrp mulGrp |
13 | 11, 4, 12 | sylancr 695 |
. . . 4
mulGrp
|
14 | 10, 2, 3, 13 | prdsmndd 17323 |
. . 3
smulGrp
|
15 | | eqidd 2623 |
. . . 4
mulGrp mulGrp |
16 | | eqid 2622 |
. . . . . 6
mulGrp mulGrp |
17 | | ffn 6045 |
. . . . . . 7
|
18 | 4, 17 | syl 17 |
. . . . . 6
|
19 | 1, 16, 10, 2, 3, 18 | prdsmgp 18610 |
. . . . 5
mulGrp smulGrp
mulGrp smulGrp
|
20 | 19 | simpld 475 |
. . . 4
mulGrp smulGrp
|
21 | 19 | simprd 479 |
. . . . 5
mulGrp smulGrp
|
22 | 21 | oveqdr 6674 |
. . . 4
mulGrp
mulGrp mulGrp smulGrp
|
23 | 15, 20, 22 | mndpropd 17316 |
. . 3
mulGrp
smulGrp |
24 | 14, 23 | mpbird 247 |
. 2
mulGrp |
25 | 4 | adantr 481 |
. . . . . . . . 9
|
26 | 25 | ffvelrnda 6359 |
. . . . . . . 8
|
27 | | eqid 2622 |
. . . . . . . . 9
|
28 | 3 | adantr 481 |
. . . . . . . . . 10
|
29 | 28 | adantr 481 |
. . . . . . . . 9
|
30 | 2 | adantr 481 |
. . . . . . . . . 10
|
31 | 30 | adantr 481 |
. . . . . . . . 9
|
32 | 18 | adantr 481 |
. . . . . . . . . 10
|
33 | 32 | adantr 481 |
. . . . . . . . 9
|
34 | | simplr1 1103 |
. . . . . . . . 9
|
35 | | simpr 477 |
. . . . . . . . 9
|
36 | 1, 27, 29, 31, 33, 34, 35 | prdsbasprj 16132 |
. . . . . . . 8
|
37 | | simpr2 1068 |
. . . . . . . . . 10
|
38 | 37 | adantr 481 |
. . . . . . . . 9
|
39 | 1, 27, 29, 31, 33, 38, 35 | prdsbasprj 16132 |
. . . . . . . 8
|
40 | | simpr3 1069 |
. . . . . . . . . 10
|
41 | 40 | adantr 481 |
. . . . . . . . 9
|
42 | 1, 27, 29, 31, 33, 41, 35 | prdsbasprj 16132 |
. . . . . . . 8
|
43 | | eqid 2622 |
. . . . . . . . 9
|
44 | | eqid 2622 |
. . . . . . . . 9
|
45 | | eqid 2622 |
. . . . . . . . 9
|
46 | 43, 44, 45 | ringdi 18566 |
. . . . . . . 8
|
47 | 26, 36, 39, 42, 46 | syl13anc 1328 |
. . . . . . 7
|
48 | | eqid 2622 |
. . . . . . . . 9
|
49 | 1, 27, 29, 31, 33, 38, 41, 48, 35 | prdsplusgfval 16134 |
. . . . . . . 8
|
50 | 49 | oveq2d 6666 |
. . . . . . 7
|
51 | | eqid 2622 |
. . . . . . . . 9
|
52 | 1, 27, 29, 31, 33, 34, 38, 51, 35 | prdsmulrfval 16136 |
. . . . . . . 8
|
53 | 1, 27, 29, 31, 33, 34, 41, 51, 35 | prdsmulrfval 16136 |
. . . . . . . 8
|
54 | 52, 53 | oveq12d 6668 |
. . . . . . 7
|
55 | 47, 50, 54 | 3eqtr4d 2666 |
. . . . . 6
|
56 | 55 | mpteq2dva 4744 |
. . . . 5
|
57 | | simpr1 1067 |
. . . . . 6
|
58 | | ringmnd 18556 |
. . . . . . . . . 10
|
59 | 58 | ssriv 3607 |
. . . . . . . . 9
|
60 | | fss 6056 |
. . . . . . . . 9
|
61 | 4, 59, 60 | sylancl 694 |
. . . . . . . 8
|
62 | 61 | adantr 481 |
. . . . . . 7
|
63 | 1, 27, 48, 28, 30, 62, 37, 40 | prdsplusgcl 17321 |
. . . . . 6
|
64 | 1, 27, 28, 30, 32, 57, 63, 51 | prdsmulrval 16135 |
. . . . 5
|
65 | 1, 27, 51, 28, 30, 25, 57, 37 | prdsmulrcl 18611 |
. . . . . 6
|
66 | 1, 27, 51, 28, 30, 25, 57, 40 | prdsmulrcl 18611 |
. . . . . 6
|
67 | 1, 27, 28, 30, 32, 65, 66, 48 | prdsplusgval 16133 |
. . . . 5
|
68 | 56, 64, 67 | 3eqtr4d 2666 |
. . . 4
|
69 | 43, 44, 45 | ringdir 18567 |
. . . . . . . 8
|
70 | 26, 36, 39, 42, 69 | syl13anc 1328 |
. . . . . . 7
|
71 | 1, 27, 29, 31, 33, 34, 38, 48, 35 | prdsplusgfval 16134 |
. . . . . . . 8
|
72 | 71 | oveq1d 6665 |
. . . . . . 7
|
73 | 1, 27, 29, 31, 33, 38, 41, 51, 35 | prdsmulrfval 16136 |
. . . . . . . 8
|
74 | 53, 73 | oveq12d 6668 |
. . . . . . 7
|
75 | 70, 72, 74 | 3eqtr4d 2666 |
. . . . . 6
|
76 | 75 | mpteq2dva 4744 |
. . . . 5
|
77 | 1, 27, 48, 28, 30, 62, 57, 37 | prdsplusgcl 17321 |
. . . . . 6
|
78 | 1, 27, 28, 30, 32, 77, 40, 51 | prdsmulrval 16135 |
. . . . 5
|
79 | 1, 27, 51, 28, 30, 25, 37, 40 | prdsmulrcl 18611 |
. . . . . 6
|
80 | 1, 27, 28, 30, 32, 66, 79, 48 | prdsplusgval 16133 |
. . . . 5
|
81 | 76, 78, 80 | 3eqtr4d 2666 |
. . . 4
|
82 | 68, 81 | jca 554 |
. . 3
|
83 | 82 | ralrimivvva 2972 |
. 2
|
84 | 27, 16, 48, 51 | isring 18551 |
. 2
mulGrp |
85 | 9, 24, 83, 84 | syl3anbrc 1246 |
1
|