Description: Lemma for lduallmod . (Contributed by NM, 22-Oct-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lduallmod.d | |
|
lduallmod.w | |
||
lduallmod.v | |
||
lduallmod.p | |
||
lduallmod.f | |
||
lduallmod.r | |
||
lduallmod.k | |
||
lduallmod.t | |
||
lduallmod.o | |
||
lduallmod.s | |
||
Assertion | lduallmodlem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lduallmod.d | |
|
2 | lduallmod.w | |
|
3 | lduallmod.v | |
|
4 | lduallmod.p | |
|
5 | lduallmod.f | |
|
6 | lduallmod.r | |
|
7 | lduallmod.k | |
|
8 | lduallmod.t | |
|
9 | lduallmod.o | |
|
10 | lduallmod.s | |
|
11 | eqid | |
|
12 | 5 1 11 2 | ldualvbase | |
13 | 12 | eqcomd | |
14 | eqidd | |
|
15 | eqid | |
|
16 | 6 9 1 15 2 | ldualsca | |
17 | 16 | eqcomd | |
18 | 10 | a1i | |
19 | 9 7 | opprbas | |
20 | 19 | a1i | |
21 | eqid | |
|
22 | 9 21 | oppradd | |
23 | 22 | a1i | |
24 | 16 | fveq2d | |
25 | eqid | |
|
26 | 9 25 | oppr1 | |
27 | 26 | a1i | |
28 | 6 | lmodring | |
29 | 9 | opprring | |
30 | 2 28 29 | 3syl | |
31 | 1 2 | ldualgrp | |
32 | 2 | 3ad2ant1 | |
33 | simp2 | |
|
34 | simp3 | |
|
35 | 5 6 7 1 10 32 33 34 | ldualvscl | |
36 | eqid | |
|
37 | 2 | adantr | |
38 | simpr1 | |
|
39 | simpr2 | |
|
40 | simpr3 | |
|
41 | 5 6 7 1 36 10 37 38 39 40 | ldualvsdi1 | |
42 | 2 | adantr | |
43 | simpr1 | |
|
44 | simpr2 | |
|
45 | simpr3 | |
|
46 | 5 6 21 7 1 36 10 42 43 44 45 | ldualvsdi2 | |
47 | eqid | |
|
48 | 5 6 7 1 15 47 10 42 43 44 45 | ldualvsass2 | |
49 | 2 | adantr | |
50 | 7 25 | ringidcl | |
51 | 2 28 50 | 3syl | |
52 | 51 | adantr | |
53 | simpr | |
|
54 | 5 3 6 7 8 1 10 49 52 53 | ldualvs | |
55 | 3 6 5 7 8 25 49 53 | lfl1sc | |
56 | 54 55 | eqtrd | |
57 | 13 14 17 18 20 23 24 27 30 31 35 41 46 48 56 | islmodd | |