Step | Hyp | Ref
| Expression |
1 | | dvhgrp.h |
. . . . 5
|
2 | | dvhgrp.t |
. . . . 5
|
3 | | dvhgrp.e |
. . . . 5
|
4 | | dvhgrp.u |
. . . . 5
|
5 | | eqid 2622 |
. . . . 5
|
6 | 1, 2, 3, 4, 5 | dvhvbase 36376 |
. . . 4
|
7 | 6 | eqcomd 2628 |
. . 3
|
8 | | dvhgrp.a |
. . . 4
|
9 | 8 | a1i 11 |
. . 3
|
10 | | dvhgrp.d |
. . . 4
Scalar |
11 | 10 | a1i 11 |
. . 3
Scalar |
12 | | dvhlvec.s |
. . . 4
|
13 | 12 | a1i 11 |
. . 3
|
14 | | eqid 2622 |
. . . . 5
|
15 | 1, 3, 4, 10, 14 | dvhbase 36372 |
. . . 4
|
16 | 15 | eqcomd 2628 |
. . 3
|
17 | | dvhgrp.p |
. . . 4
|
18 | 17 | a1i 11 |
. . 3
|
19 | | dvhlvec.m |
. . . 4
|
20 | 19 | a1i 11 |
. . 3
|
21 | | eqid 2622 |
. . . . . 6
|
22 | 1, 21, 4, 10 | dvhsca 36371 |
. . . . 5
|
23 | 22 | fveq2d 6195 |
. . . 4
|
24 | | eqid 2622 |
. . . . 5
|
25 | 1, 2, 21, 24 | erng1r 36283 |
. . . 4
|
26 | 23, 25 | eqtr2d 2657 |
. . 3
|
27 | 1, 21 | erngdv 36281 |
. . . . 5
|
28 | 22, 27 | eqeltrd 2701 |
. . . 4
|
29 | | drngring 18754 |
. . . 4
|
30 | 28, 29 | syl 17 |
. . 3
|
31 | | dvhgrp.b |
. . . 4
|
32 | | dvhgrp.o |
. . . 4
|
33 | | dvhgrp.i |
. . . 4
|
34 | 31, 1, 2, 3, 4, 10,
17, 8, 32, 33 | dvhgrp 36396 |
. . 3
|
35 | 1, 2, 3, 4, 12 | dvhvscacl 36392 |
. . . 4
|
36 | 35 | 3impb 1260 |
. . 3
|
37 | | simpl 473 |
. . . . . . 7
|
38 | | simpr1 1067 |
. . . . . . 7
|
39 | | simpr2 1068 |
. . . . . . . 8
|
40 | | xp1st 7198 |
. . . . . . . 8
|
41 | 39, 40 | syl 17 |
. . . . . . 7
|
42 | | simpr3 1069 |
. . . . . . . 8
|
43 | | xp1st 7198 |
. . . . . . . 8
|
44 | 42, 43 | syl 17 |
. . . . . . 7
|
45 | 1, 2, 3 | tendospdi1 36309 |
. . . . . . 7
|
46 | 37, 38, 41, 44, 45 | syl13anc 1328 |
. . . . . 6
|
47 | 1, 2, 3, 4, 10, 8,
17 | dvhvadd 36381 |
. . . . . . . . . 10
|
48 | 47 | 3adantr1 1220 |
. . . . . . . . 9
|
49 | 48 | fveq2d 6195 |
. . . . . . . 8
|
50 | | fvex 6201 |
. . . . . . . . . 10
|
51 | | fvex 6201 |
. . . . . . . . . 10
|
52 | 50, 51 | coex 7118 |
. . . . . . . . 9
|
53 | | ovex 6678 |
. . . . . . . . 9
|
54 | 52, 53 | op1st 7176 |
. . . . . . . 8
|
55 | 49, 54 | syl6eq 2672 |
. . . . . . 7
|
56 | 55 | fveq2d 6195 |
. . . . . 6
|
57 | 1, 2, 3, 4, 12 | dvhvsca 36390 |
. . . . . . . . . 10
|
58 | 57 | 3adantr3 1222 |
. . . . . . . . 9
|
59 | 58 | fveq2d 6195 |
. . . . . . . 8
|
60 | | fvex 6201 |
. . . . . . . . 9
|
61 | | vex 3203 |
. . . . . . . . . 10
|
62 | | fvex 6201 |
. . . . . . . . . 10
|
63 | 61, 62 | coex 7118 |
. . . . . . . . 9
|
64 | 60, 63 | op1st 7176 |
. . . . . . . 8
|
65 | 59, 64 | syl6eq 2672 |
. . . . . . 7
|
66 | 1, 2, 3, 4, 12 | dvhvsca 36390 |
. . . . . . . . . 10
|
67 | 66 | 3adantr2 1221 |
. . . . . . . . 9
|
68 | 67 | fveq2d 6195 |
. . . . . . . 8
|
69 | | fvex 6201 |
. . . . . . . . 9
|
70 | | fvex 6201 |
. . . . . . . . . 10
|
71 | 61, 70 | coex 7118 |
. . . . . . . . 9
|
72 | 69, 71 | op1st 7176 |
. . . . . . . 8
|
73 | 68, 72 | syl6eq 2672 |
. . . . . . 7
|
74 | 65, 73 | coeq12d 5286 |
. . . . . 6
|
75 | 46, 56, 74 | 3eqtr4d 2666 |
. . . . 5
|
76 | 30 | adantr 481 |
. . . . . . . 8
|
77 | 16 | adantr 481 |
. . . . . . . . 9
|
78 | 38, 77 | eleqtrd 2703 |
. . . . . . . 8
|
79 | | xp2nd 7199 |
. . . . . . . . . 10
|
80 | 39, 79 | syl 17 |
. . . . . . . . 9
|
81 | 80, 77 | eleqtrd 2703 |
. . . . . . . 8
|
82 | | xp2nd 7199 |
. . . . . . . . . 10
|
83 | 42, 82 | syl 17 |
. . . . . . . . 9
|
84 | 83, 77 | eleqtrd 2703 |
. . . . . . . 8
|
85 | 14, 17, 19 | ringdi 18566 |
. . . . . . . 8
|
86 | 76, 78, 81, 84, 85 | syl13anc 1328 |
. . . . . . 7
|
87 | 14, 17 | ringacl 18578 |
. . . . . . . . . 10
|
88 | 76, 81, 84, 87 | syl3anc 1326 |
. . . . . . . . 9
|
89 | 88, 77 | eleqtrrd 2704 |
. . . . . . . 8
|
90 | 1, 2, 3, 4, 10, 19 | dvhmulr 36375 |
. . . . . . . 8
|
91 | 37, 38, 89, 90 | syl12anc 1324 |
. . . . . . 7
|
92 | 1, 2, 3, 4, 10, 19 | dvhmulr 36375 |
. . . . . . . . 9
|
93 | 37, 38, 80, 92 | syl12anc 1324 |
. . . . . . . 8
|
94 | 1, 2, 3, 4, 10, 19 | dvhmulr 36375 |
. . . . . . . . 9
|
95 | 37, 38, 83, 94 | syl12anc 1324 |
. . . . . . . 8
|
96 | 93, 95 | oveq12d 6668 |
. . . . . . 7
|
97 | 86, 91, 96 | 3eqtr3d 2664 |
. . . . . 6
|
98 | 48 | fveq2d 6195 |
. . . . . . . 8
|
99 | 52, 53 | op2nd 7177 |
. . . . . . . 8
|
100 | 98, 99 | syl6eq 2672 |
. . . . . . 7
|
101 | 100 | coeq2d 5284 |
. . . . . 6
|
102 | 58 | fveq2d 6195 |
. . . . . . . 8
|
103 | 60, 63 | op2nd 7177 |
. . . . . . . 8
|
104 | 102, 103 | syl6eq 2672 |
. . . . . . 7
|
105 | 67 | fveq2d 6195 |
. . . . . . . 8
|
106 | 69, 71 | op2nd 7177 |
. . . . . . . 8
|
107 | 105, 106 | syl6eq 2672 |
. . . . . . 7
|
108 | 104, 107 | oveq12d 6668 |
. . . . . 6
|
109 | 97, 101, 108 | 3eqtr4d 2666 |
. . . . 5
|
110 | 75, 109 | opeq12d 4410 |
. . . 4
|
111 | 1, 2, 3, 4, 10, 17, 8 | dvhvaddcl 36384 |
. . . . . 6
|
112 | 111 | 3adantr1 1220 |
. . . . 5
|
113 | 1, 2, 3, 4, 12 | dvhvsca 36390 |
. . . . 5
|
114 | 37, 38, 112, 113 | syl12anc 1324 |
. . . 4
|
115 | 35 | 3adantr3 1222 |
. . . . 5
|
116 | 1, 2, 3, 4, 12 | dvhvscacl 36392 |
. . . . . 6
|
117 | 116 | 3adantr2 1221 |
. . . . 5
|
118 | 1, 2, 3, 4, 10, 8,
17 | dvhvadd 36381 |
. . . . 5
|
119 | 37, 115, 117, 118 | syl12anc 1324 |
. . . 4
|
120 | 110, 114,
119 | 3eqtr4d 2666 |
. . 3
|
121 | | simpl 473 |
. . . . . . 7
|
122 | | simpr1 1067 |
. . . . . . 7
|
123 | | simpr2 1068 |
. . . . . . 7
|
124 | | simpr3 1069 |
. . . . . . . 8
|
125 | 124, 43 | syl 17 |
. . . . . . 7
|
126 | | eqid 2622 |
. . . . . . . 8
|
127 | 1, 2, 3, 21, 126 | erngplus2 36092 |
. . . . . . 7
|
128 | 121, 122,
123, 125, 127 | syl13anc 1328 |
. . . . . 6
|
129 | 22 | fveq2d 6195 |
. . . . . . . . . 10
|
130 | 17, 129 | syl5eq 2668 |
. . . . . . . . 9
|
131 | 130 | oveqd 6667 |
. . . . . . . 8
|
132 | 131 | fveq1d 6193 |
. . . . . . 7
|
133 | 132 | adantr 481 |
. . . . . 6
|
134 | 66 | 3adantr2 1221 |
. . . . . . . . 9
|
135 | 134 | fveq2d 6195 |
. . . . . . . 8
|
136 | 135, 72 | syl6eq 2672 |
. . . . . . 7
|
137 | 1, 2, 3, 4, 12 | dvhvsca 36390 |
. . . . . . . . . 10
|
138 | 137 | 3adantr1 1220 |
. . . . . . . . 9
|
139 | 138 | fveq2d 6195 |
. . . . . . . 8
|
140 | | fvex 6201 |
. . . . . . . . 9
|
141 | | vex 3203 |
. . . . . . . . . 10
|
142 | 141, 70 | coex 7118 |
. . . . . . . . 9
|
143 | 140, 142 | op1st 7176 |
. . . . . . . 8
|
144 | 139, 143 | syl6eq 2672 |
. . . . . . 7
|
145 | 136, 144 | coeq12d 5286 |
. . . . . 6
|
146 | 128, 133,
145 | 3eqtr4d 2666 |
. . . . 5
|
147 | 30 | adantr 481 |
. . . . . . . 8
|
148 | 16 | adantr 481 |
. . . . . . . . 9
|
149 | 122, 148 | eleqtrd 2703 |
. . . . . . . 8
|
150 | 123, 148 | eleqtrd 2703 |
. . . . . . . 8
|
151 | 124, 82 | syl 17 |
. . . . . . . . 9
|
152 | 151, 148 | eleqtrd 2703 |
. . . . . . . 8
|
153 | 14, 17, 19 | ringdir 18567 |
. . . . . . . 8
|
154 | 147, 149,
150, 152, 153 | syl13anc 1328 |
. . . . . . 7
|
155 | 14, 17 | ringacl 18578 |
. . . . . . . . . 10
|
156 | 147, 149,
150, 155 | syl3anc 1326 |
. . . . . . . . 9
|
157 | 156, 148 | eleqtrrd 2704 |
. . . . . . . 8
|
158 | 1, 2, 3, 4, 10, 19 | dvhmulr 36375 |
. . . . . . . 8
|
159 | 121, 157,
151, 158 | syl12anc 1324 |
. . . . . . 7
|
160 | 121, 122,
151, 94 | syl12anc 1324 |
. . . . . . . 8
|
161 | 1, 2, 3, 4, 10, 19 | dvhmulr 36375 |
. . . . . . . . 9
|
162 | 121, 123,
151, 161 | syl12anc 1324 |
. . . . . . . 8
|
163 | 160, 162 | oveq12d 6668 |
. . . . . . 7
|
164 | 154, 159,
163 | 3eqtr3d 2664 |
. . . . . 6
|
165 | 134 | fveq2d 6195 |
. . . . . . . 8
|
166 | 165, 106 | syl6eq 2672 |
. . . . . . 7
|
167 | 138 | fveq2d 6195 |
. . . . . . . 8
|
168 | 140, 142 | op2nd 7177 |
. . . . . . . 8
|
169 | 167, 168 | syl6eq 2672 |
. . . . . . 7
|
170 | 166, 169 | oveq12d 6668 |
. . . . . 6
|
171 | 164, 170 | eqtr4d 2659 |
. . . . 5
|
172 | 146, 171 | opeq12d 4410 |
. . . 4
|
173 | 1, 2, 3, 4, 12 | dvhvsca 36390 |
. . . . 5
|
174 | 121, 157,
124, 173 | syl12anc 1324 |
. . . 4
|
175 | 116 | 3adantr2 1221 |
. . . . 5
|
176 | 1, 2, 3, 4, 12 | dvhvscacl 36392 |
. . . . . 6
|
177 | 176 | 3adantr1 1220 |
. . . . 5
|
178 | 1, 2, 3, 4, 10, 8,
17 | dvhvadd 36381 |
. . . . 5
|
179 | 121, 175,
177, 178 | syl12anc 1324 |
. . . 4
|
180 | 172, 174,
179 | 3eqtr4d 2666 |
. . 3
|
181 | 1, 2, 3 | tendocoval 36054 |
. . . . . . 7
|
182 | 121, 122,
123, 125, 181 | syl121anc 1331 |
. . . . . 6
|
183 | | coass 5654 |
. . . . . . 7
|
184 | 183 | a1i 11 |
. . . . . 6
|
185 | 182, 184 | opeq12d 4410 |
. . . . 5
|
186 | 1, 3 | tendococl 36060 |
. . . . . . 7
|
187 | 121, 122,
123, 186 | syl3anc 1326 |
. . . . . 6
|
188 | 1, 2, 3, 4, 12 | dvhvsca 36390 |
. . . . . 6
|
189 | 121, 187,
124, 188 | syl12anc 1324 |
. . . . 5
|
190 | 1, 2, 3 | tendocl 36055 |
. . . . . . 7
|
191 | 121, 123,
125, 190 | syl3anc 1326 |
. . . . . 6
|
192 | 1, 3 | tendococl 36060 |
. . . . . . 7
|
193 | 121, 123,
151, 192 | syl3anc 1326 |
. . . . . 6
|
194 | 1, 2, 3, 4, 12 | dvhopvsca 36391 |
. . . . . 6
|
195 | 121, 122,
191, 193, 194 | syl13anc 1328 |
. . . . 5
|
196 | 185, 189,
195 | 3eqtr4d 2666 |
. . . 4
|
197 | 1, 2, 3, 4, 10, 19 | dvhmulr 36375 |
. . . . . 6
|
198 | 197 | 3adantr3 1222 |
. . . . 5
|
199 | 198 | oveq1d 6665 |
. . . 4
|
200 | 138 | oveq2d 6666 |
. . . 4
|
201 | 196, 199,
200 | 3eqtr4d 2666 |
. . 3
|
202 | | xp1st 7198 |
. . . . . . 7
|
203 | 202 | adantl 482 |
. . . . . 6
|
204 | | tendospid 36306 |
. . . . . 6
|
205 | 203, 204 | syl 17 |
. . . . 5
|
206 | | xp2nd 7199 |
. . . . . . 7
|
207 | 1, 2, 3 | tendof 36051 |
. . . . . . 7
|
208 | 206, 207 | sylan2 491 |
. . . . . 6
|
209 | | fcoi2 6079 |
. . . . . 6
|
210 | 208, 209 | syl 17 |
. . . . 5
|
211 | 205, 210 | opeq12d 4410 |
. . . 4
|
212 | 1, 2, 3 | tendoidcl 36057 |
. . . . . 6
|
213 | 212 | anim1i 592 |
. . . . 5
|
214 | 1, 2, 3, 4, 12 | dvhvsca 36390 |
. . . . 5
|
215 | 213, 214 | syldan 487 |
. . . 4
|
216 | | 1st2nd2 7205 |
. . . . 5
|
217 | 216 | adantl 482 |
. . . 4
|
218 | 211, 215,
217 | 3eqtr4d 2666 |
. . 3
|
219 | 7, 9, 11, 13, 16, 18, 20, 26, 30, 34, 36, 120, 180, 201, 218 | islmodd 18869 |
. 2
|
220 | 10 | islvec 19104 |
. 2
|
221 | 219, 28, 220 | sylanbrc 698 |
1
|