Step | Hyp | Ref
| Expression |
1 | | oveq1 6657 |
. . . . . . . 8
|
2 | | oveq1 6657 |
. . . . . . . . 9
|
3 | 2 | oveq1d 6665 |
. . . . . . . 8
|
4 | 1, 3 | eqeq12d 2637 |
. . . . . . 7
|
5 | 4 | imbi2d 330 |
. . . . . 6
|
6 | | oveq1 6657 |
. . . . . . . 8
|
7 | | oveq1 6657 |
. . . . . . . . 9
|
8 | 7 | oveq1d 6665 |
. . . . . . . 8
|
9 | 6, 8 | eqeq12d 2637 |
. . . . . . 7
|
10 | 9 | imbi2d 330 |
. . . . . 6
|
11 | | oveq1 6657 |
. . . . . . . 8
|
12 | | oveq1 6657 |
. . . . . . . . 9
|
13 | 12 | oveq1d 6665 |
. . . . . . . 8
|
14 | 11, 13 | eqeq12d 2637 |
. . . . . . 7
|
15 | 14 | imbi2d 330 |
. . . . . 6
|
16 | | oveq1 6657 |
. . . . . . . 8
|
17 | | oveq1 6657 |
. . . . . . . . 9
|
18 | 17 | oveq1d 6665 |
. . . . . . . 8
|
19 | 16, 18 | eqeq12d 2637 |
. . . . . . 7
|
20 | 19 | imbi2d 330 |
. . . . . 6
|
21 | | simpr 477 |
. . . . . . . 8
|
22 | | simpr 477 |
. . . . . . . . 9
|
23 | 22 | adantr 481 |
. . . . . . . 8
|
24 | | lmodvsmmulgdi.v |
. . . . . . . . 9
|
25 | | lmodvsmmulgdi.f |
. . . . . . . . 9
Scalar |
26 | | lmodvsmmulgdi.s |
. . . . . . . . 9
|
27 | | eqid 2622 |
. . . . . . . . 9
|
28 | | eqid 2622 |
. . . . . . . . 9
|
29 | 24, 25, 26, 27, 28 | lmod0vs 18896 |
. . . . . . . 8
|
30 | 21, 23, 29 | syl2anc 693 |
. . . . . . 7
|
31 | | simpl 473 |
. . . . . . . . . 10
|
32 | 31 | adantr 481 |
. . . . . . . . 9
|
33 | | lmodvsmmulgdi.k |
. . . . . . . . . 10
|
34 | | lmodvsmmulgdi.e |
. . . . . . . . . 10
.g |
35 | 33, 27, 34 | mulg0 17546 |
. . . . . . . . 9
|
36 | 32, 35 | syl 17 |
. . . . . . . 8
|
37 | 36 | oveq1d 6665 |
. . . . . . 7
|
38 | 24, 25, 26, 33 | lmodvscl 18880 |
. . . . . . . . 9
|
39 | 21, 32, 23, 38 | syl3anc 1326 |
. . . . . . . 8
|
40 | | lmodvsmmulgdi.p |
. . . . . . . . 9
.g |
41 | 24, 28, 40 | mulg0 17546 |
. . . . . . . 8
|
42 | 39, 41 | syl 17 |
. . . . . . 7
|
43 | 30, 37, 42 | 3eqtr4rd 2667 |
. . . . . 6
|
44 | | lmodgrp 18870 |
. . . . . . . . . . . . . 14
|
45 | | grpmnd 17429 |
. . . . . . . . . . . . . 14
|
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . 13
|
47 | 46 | adantl 482 |
. . . . . . . . . . . 12
|
48 | 47 | adantl 482 |
. . . . . . . . . . 11
|
49 | | simpl 473 |
. . . . . . . . . . 11
|
50 | 39 | adantl 482 |
. . . . . . . . . . 11
|
51 | | eqid 2622 |
. . . . . . . . . . . 12
|
52 | 24, 40, 51 | mulgnn0p1 17552 |
. . . . . . . . . . 11
|
53 | 48, 49, 50, 52 | syl3anc 1326 |
. . . . . . . . . 10
|
54 | 53 | adantr 481 |
. . . . . . . . 9
|
55 | | oveq1 6657 |
. . . . . . . . . 10
|
56 | 21 | adantl 482 |
. . . . . . . . . . . 12
|
57 | 25 | lmodring 18871 |
. . . . . . . . . . . . . . . 16
|
58 | | ringmnd 18556 |
. . . . . . . . . . . . . . . 16
|
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . 15
|
60 | 59 | adantl 482 |
. . . . . . . . . . . . . 14
|
61 | 60 | adantl 482 |
. . . . . . . . . . . . 13
|
62 | | simprll 802 |
. . . . . . . . . . . . 13
|
63 | 33, 34 | mulgnn0cl 17558 |
. . . . . . . . . . . . 13
|
64 | 61, 49, 62, 63 | syl3anc 1326 |
. . . . . . . . . . . 12
|
65 | 23 | adantl 482 |
. . . . . . . . . . . 12
|
66 | | eqid 2622 |
. . . . . . . . . . . . 13
|
67 | 24, 51, 25, 26, 33, 66 | lmodvsdir 18887 |
. . . . . . . . . . . 12
|
68 | 56, 64, 62, 65, 67 | syl13anc 1328 |
. . . . . . . . . . 11
|
69 | 33, 34, 66 | mulgnn0p1 17552 |
. . . . . . . . . . . . . 14
|
70 | 61, 49, 62, 69 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
71 | 70 | eqcomd 2628 |
. . . . . . . . . . . 12
|
72 | 71 | oveq1d 6665 |
. . . . . . . . . . 11
|
73 | 68, 72 | eqtr3d 2658 |
. . . . . . . . . 10
|
74 | 55, 73 | sylan9eqr 2678 |
. . . . . . . . 9
|
75 | 54, 74 | eqtrd 2656 |
. . . . . . . 8
|
76 | 75 | exp31 630 |
. . . . . . 7
|
77 | 76 | a2d 29 |
. . . . . 6
|
78 | 5, 10, 15, 20, 43, 77 | nn0ind 11472 |
. . . . 5
|
79 | 78 | exp4c 636 |
. . . 4
|
80 | 79 | com12 32 |
. . 3
|
81 | 80 | 3imp 1256 |
. 2
|
82 | 81 | impcom 446 |
1
|