Step | Hyp | Ref
| Expression |
1 | | eqidd 2623 |
. 2
|
2 | | eqidd 2623 |
. 2
|
3 | | prdslmodd.y |
. . 3
s |
4 | | prdslmodd.s |
. . 3
|
5 | | prdslmodd.rm |
. . . 4
|
6 | | prdslmodd.i |
. . . 4
|
7 | | fex 6490 |
. . . 4
|
8 | 5, 6, 7 | syl2anc 693 |
. . 3
|
9 | 3, 4, 8 | prdssca 16116 |
. 2
Scalar |
10 | | eqidd 2623 |
. 2
|
11 | | eqidd 2623 |
. 2
|
12 | | eqidd 2623 |
. 2
|
13 | | eqidd 2623 |
. 2
|
14 | | eqidd 2623 |
. 2
|
15 | | lmodgrp 18870 |
. . . . 5
|
16 | 15 | ssriv 3607 |
. . . 4
|
17 | | fss 6056 |
. . . 4
|
18 | 5, 16, 17 | sylancl 694 |
. . 3
|
19 | 3, 6, 4, 18 | prdsgrpd 17525 |
. 2
|
20 | | eqid 2622 |
. . . 4
|
21 | | eqid 2622 |
. . . 4
|
22 | | eqid 2622 |
. . . 4
|
23 | 4 | adantr 481 |
. . . 4
|
24 | | elex 3212 |
. . . . . 6
|
25 | 6, 24 | syl 17 |
. . . . 5
|
26 | 25 | adantr 481 |
. . . 4
|
27 | 5 | adantr 481 |
. . . 4
|
28 | | simprl 794 |
. . . 4
|
29 | | simprr 796 |
. . . 4
|
30 | | prdslmodd.rs |
. . . . 5
Scalar |
31 | 30 | adantlr 751 |
. . . 4
Scalar |
32 | 3, 20, 21, 22, 23, 26, 27, 28, 29, 31 | prdsvscacl 18968 |
. . 3
|
33 | 32 | 3impb 1260 |
. 2
|
34 | 5 | ffvelrnda 6359 |
. . . . . . 7
|
35 | 34 | adantlr 751 |
. . . . . 6
|
36 | | simplr1 1103 |
. . . . . . 7
|
37 | 30 | fveq2d 6195 |
. . . . . . . 8
Scalar |
38 | 37 | adantlr 751 |
. . . . . . 7
Scalar |
39 | 36, 38 | eleqtrrd 2704 |
. . . . . 6
Scalar |
40 | 4 | ad2antrr 762 |
. . . . . . 7
|
41 | 25 | ad2antrr 762 |
. . . . . . 7
|
42 | | ffn 6045 |
. . . . . . . . 9
|
43 | 5, 42 | syl 17 |
. . . . . . . 8
|
44 | 43 | ad2antrr 762 |
. . . . . . 7
|
45 | | simplr2 1104 |
. . . . . . 7
|
46 | | simpr 477 |
. . . . . . 7
|
47 | 3, 20, 40, 41, 44, 45, 46 | prdsbasprj 16132 |
. . . . . 6
|
48 | | simplr3 1105 |
. . . . . . 7
|
49 | 3, 20, 40, 41, 44, 48, 46 | prdsbasprj 16132 |
. . . . . 6
|
50 | | eqid 2622 |
. . . . . . 7
|
51 | | eqid 2622 |
. . . . . . 7
|
52 | | eqid 2622 |
. . . . . . 7
Scalar Scalar |
53 | | eqid 2622 |
. . . . . . 7
|
54 | | eqid 2622 |
. . . . . . 7
Scalar Scalar |
55 | 50, 51, 52, 53, 54 | lmodvsdi 18886 |
. . . . . 6
Scalar |
56 | 35, 39, 47, 49, 55 | syl13anc 1328 |
. . . . 5
|
57 | | eqid 2622 |
. . . . . . 7
|
58 | 3, 20, 40, 41, 44, 45, 48, 57, 46 | prdsplusgfval 16134 |
. . . . . 6
|
59 | 58 | oveq2d 6666 |
. . . . 5
|
60 | 3, 20, 21, 22, 40, 41, 44, 36, 45, 46 | prdsvscafval 16140 |
. . . . . 6
|
61 | 3, 20, 21, 22, 40, 41, 44, 36, 48, 46 | prdsvscafval 16140 |
. . . . . 6
|
62 | 60, 61 | oveq12d 6668 |
. . . . 5
|
63 | 56, 59, 62 | 3eqtr4d 2666 |
. . . 4
|
64 | 63 | mpteq2dva 4744 |
. . 3
|
65 | 4 | adantr 481 |
. . . 4
|
66 | 25 | adantr 481 |
. . . 4
|
67 | 43 | adantr 481 |
. . . 4
|
68 | | simpr1 1067 |
. . . 4
|
69 | 19 | adantr 481 |
. . . . 5
|
70 | | simpr2 1068 |
. . . . 5
|
71 | | simpr3 1069 |
. . . . 5
|
72 | 20, 57 | grpcl 17430 |
. . . . 5
|
73 | 69, 70, 71, 72 | syl3anc 1326 |
. . . 4
|
74 | 3, 20, 21, 22, 65, 66, 67, 68, 73 | prdsvscaval 16139 |
. . 3
|
75 | 32 | 3adantr3 1222 |
. . . 4
|
76 | 4 | adantr 481 |
. . . . . 6
|
77 | 25 | adantr 481 |
. . . . . 6
|
78 | 5 | adantr 481 |
. . . . . 6
|
79 | | simprl 794 |
. . . . . 6
|
80 | | simprr 796 |
. . . . . 6
|
81 | 30 | adantlr 751 |
. . . . . 6
Scalar |
82 | 3, 20, 21, 22, 76, 77, 78, 79, 80, 81 | prdsvscacl 18968 |
. . . . 5
|
83 | 82 | 3adantr2 1221 |
. . . 4
|
84 | 3, 20, 65, 66, 67, 75, 83, 57 | prdsplusgval 16133 |
. . 3
|
85 | 64, 74, 84 | 3eqtr4d 2666 |
. 2
|
86 | 4 | ad2antrr 762 |
. . . . . . 7
|
87 | 25 | ad2antrr 762 |
. . . . . . 7
|
88 | 43 | ad2antrr 762 |
. . . . . . 7
|
89 | | simplr1 1103 |
. . . . . . 7
|
90 | | simplr3 1105 |
. . . . . . 7
|
91 | | simpr 477 |
. . . . . . 7
|
92 | 3, 20, 21, 22, 86, 87, 88, 89, 90, 91 | prdsvscafval 16140 |
. . . . . 6
|
93 | | simplr2 1104 |
. . . . . . 7
|
94 | 3, 20, 21, 22, 86, 87, 88, 93, 90, 91 | prdsvscafval 16140 |
. . . . . 6
|
95 | 92, 94 | oveq12d 6668 |
. . . . 5
|
96 | 34 | adantlr 751 |
. . . . . 6
|
97 | 37 | adantlr 751 |
. . . . . . 7
Scalar |
98 | 89, 97 | eleqtrrd 2704 |
. . . . . 6
Scalar |
99 | 93, 97 | eleqtrrd 2704 |
. . . . . 6
Scalar |
100 | 3, 20, 86, 87, 88, 90, 91 | prdsbasprj 16132 |
. . . . . 6
|
101 | | eqid 2622 |
. . . . . . 7
Scalar Scalar |
102 | 50, 51, 52, 53, 54, 101 | lmodvsdir 18887 |
. . . . . 6
Scalar Scalar Scalar |
103 | 96, 98, 99, 100, 102 | syl13anc 1328 |
. . . . 5
Scalar |
104 | 30 | adantlr 751 |
. . . . . . . 8
Scalar |
105 | 104 | fveq2d 6195 |
. . . . . . 7
Scalar |
106 | 105 | oveqd 6667 |
. . . . . 6
Scalar |
107 | 106 | oveq1d 6665 |
. . . . 5
Scalar |
108 | 95, 103, 107 | 3eqtr2rd 2663 |
. . . 4
|
109 | 108 | mpteq2dva 4744 |
. . 3
|
110 | 4 | adantr 481 |
. . . 4
|
111 | 25 | adantr 481 |
. . . 4
|
112 | 43 | adantr 481 |
. . . 4
|
113 | | simpr1 1067 |
. . . . 5
|
114 | | simpr2 1068 |
. . . . 5
|
115 | | eqid 2622 |
. . . . . 6
|
116 | 22, 115 | ringacl 18578 |
. . . . 5
|
117 | 110, 113,
114, 116 | syl3anc 1326 |
. . . 4
|
118 | | simpr3 1069 |
. . . 4
|
119 | 3, 20, 21, 22, 110, 111, 112, 117, 118 | prdsvscaval 16139 |
. . 3
|
120 | 82 | 3adantr2 1221 |
. . . 4
|
121 | 5 | adantr 481 |
. . . . 5
|
122 | 3, 20, 21, 22, 110, 111, 121, 114, 118, 104 | prdsvscacl 18968 |
. . . 4
|
123 | 3, 20, 110, 111, 112, 120, 122, 57 | prdsplusgval 16133 |
. . 3
|
124 | 109, 119,
123 | 3eqtr4d 2666 |
. 2
|
125 | 94 | oveq2d 6666 |
. . . . 5
|
126 | | eqid 2622 |
. . . . . . 7
Scalar Scalar |
127 | 50, 52, 53, 54, 126 | lmodvsass 18888 |
. . . . . 6
Scalar Scalar Scalar |
128 | 96, 98, 99, 100, 127 | syl13anc 1328 |
. . . . 5
Scalar |
129 | 104 | fveq2d 6195 |
. . . . . . 7
Scalar |
130 | 129 | oveqd 6667 |
. . . . . 6
Scalar |
131 | 130 | oveq1d 6665 |
. . . . 5
Scalar |
132 | 125, 128,
131 | 3eqtr2rd 2663 |
. . . 4
|
133 | 132 | mpteq2dva 4744 |
. . 3
|
134 | | eqid 2622 |
. . . . . 6
|
135 | 22, 134 | ringcl 18561 |
. . . . 5
|
136 | 110, 113,
114, 135 | syl3anc 1326 |
. . . 4
|
137 | 3, 20, 21, 22, 110, 111, 112, 136, 118 | prdsvscaval 16139 |
. . 3
|
138 | 3, 20, 21, 22, 110, 111, 112, 113, 122 | prdsvscaval 16139 |
. . 3
|
139 | 133, 137,
138 | 3eqtr4d 2666 |
. 2
|
140 | 30 | fveq2d 6195 |
. . . . . . 7
Scalar |
141 | 140 | adantlr 751 |
. . . . . 6
Scalar |
142 | 141 | oveq1d 6665 |
. . . . 5
Scalar |
143 | 34 | adantlr 751 |
. . . . . 6
|
144 | 4 | ad2antrr 762 |
. . . . . . 7
|
145 | 25 | ad2antrr 762 |
. . . . . . 7
|
146 | 43 | ad2antrr 762 |
. . . . . . 7
|
147 | | simplr 792 |
. . . . . . 7
|
148 | | simpr 477 |
. . . . . . 7
|
149 | 3, 20, 144, 145, 146, 147, 148 | prdsbasprj 16132 |
. . . . . 6
|
150 | | eqid 2622 |
. . . . . . 7
Scalar Scalar |
151 | 50, 52, 53, 150 | lmodvs1 18891 |
. . . . . 6
Scalar |
152 | 143, 149,
151 | syl2anc 693 |
. . . . 5
Scalar |
153 | 142, 152 | eqtr3d 2658 |
. . . 4
|
154 | 153 | mpteq2dva 4744 |
. . 3
|
155 | 4 | adantr 481 |
. . . 4
|
156 | 25 | adantr 481 |
. . . 4
|
157 | 43 | adantr 481 |
. . . 4
|
158 | | eqid 2622 |
. . . . . . 7
|
159 | 22, 158 | ringidcl 18568 |
. . . . . 6
|
160 | 4, 159 | syl 17 |
. . . . 5
|
161 | 160 | adantr 481 |
. . . 4
|
162 | | simpr 477 |
. . . 4
|
163 | 3, 20, 21, 22, 155, 156, 157, 161, 162 | prdsvscaval 16139 |
. . 3
|
164 | 3, 20, 155, 156, 157, 162 | prdsbasfn 16131 |
. . . 4
|
165 | | dffn5 6241 |
. . . 4
|
166 | 164, 165 | sylib 208 |
. . 3
|
167 | 154, 163,
166 | 3eqtr4d 2666 |
. 2
|
168 | 1, 2, 9, 10, 11, 12, 13, 14, 4, 19, 33, 85, 124, 139, 167 | islmodd 18869 |
1
|