Step |
Hyp |
Ref |
Expression |
1 |
|
lcdvsubval.h |
|
2 |
|
lcdvsubval.u |
|
3 |
|
lcdvsubval.v |
|
4 |
|
lcdvsubval.r |
|
5 |
|
lcdvsubval.s |
|
6 |
|
lcdvsubval.c |
|
7 |
|
lcdvsubval.d |
|
8 |
|
lcdvsubval.m |
|
9 |
|
lcdvsubval.k |
|
10 |
|
lcdvsubval.f |
|
11 |
|
lcdvsubval.g |
|
12 |
|
lcdvsubval.x |
|
13 |
1 6 9
|
lcdlmod |
|
14 |
|
eqid |
|
15 |
|
eqid |
|
16 |
|
eqid |
|
17 |
|
eqid |
|
18 |
|
eqid |
|
19 |
7 14 8 15 16 17 18
|
lmodvsubval2 |
|
20 |
13 10 11 19
|
syl3anc |
|
21 |
20
|
fveq1d |
|
22 |
|
eqid |
|
23 |
|
eqid |
|
24 |
15
|
lmodfgrp |
|
25 |
13 24
|
syl |
|
26 |
15
|
lmodring |
|
27 |
13 26
|
syl |
|
28 |
|
eqid |
|
29 |
28 18
|
ringidcl |
|
30 |
27 29
|
syl |
|
31 |
28 17
|
grpinvcl |
|
32 |
25 30 31
|
syl2anc |
|
33 |
1 2 4 23 6 15 28 9
|
lcdsbase |
|
34 |
32 33
|
eleqtrd |
|
35 |
1 2 4 23 6 7 16 9 34 11
|
lcdvscl |
|
36 |
1 2 3 4 22 6 7 14 9 10 35 12
|
lcdvaddval |
|
37 |
|
eqid |
|
38 |
1 2 4 37 6 15 17 9
|
lcdneg |
|
39 |
|
eqid |
|
40 |
1 2 4 39 6 15 18 9
|
lcd1 |
|
41 |
38 40
|
fveq12d |
|
42 |
41
|
oveq1d |
|
43 |
42
|
fveq1d |
|
44 |
|
eqid |
|
45 |
1 2 9
|
dvhlmod |
|
46 |
4
|
lmodring |
|
47 |
45 46
|
syl |
|
48 |
|
ringgrp |
|
49 |
47 48
|
syl |
|
50 |
4 23 39
|
lmod1cl |
|
51 |
45 50
|
syl |
|
52 |
23 37
|
grpinvcl |
|
53 |
49 51 52
|
syl2anc |
|
54 |
1 2 3 4 23 44 6 7 16 9 53 11 12
|
lcdvsval |
|
55 |
1 2 3 4 23 6 7 9 11 12
|
lcdvbasecl |
|
56 |
23 44 39 37 47 55
|
rngnegr |
|
57 |
43 54 56
|
3eqtrd |
|
58 |
57
|
oveq2d |
|
59 |
1 2 3 4 23 6 7 9 10 12
|
lcdvbasecl |
|
60 |
23 22 37 5
|
grpsubval |
|
61 |
59 55 60
|
syl2anc |
|
62 |
58 61
|
eqtr4d |
|
63 |
21 36 62
|
3eqtrd |
|