Description: Lemmma for mapdh6N . Part (6) in Baer p. 47 line 38. (Contributed by NM, 1-May-2015) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mapdh.q | |
|
mapdh.i | |
||
mapdh.h | |
||
mapdh.m | |
||
mapdh.u | |
||
mapdh.v | |
||
mapdh.s | |
||
mapdhc.o | |
||
mapdh.n | |
||
mapdh.c | |
||
mapdh.d | |
||
mapdh.r | |
||
mapdh.j | |
||
mapdh.k | |
||
mapdhc.f | |
||
mapdh.mn | |
||
mapdhcl.x | |
||
mapdh.p | |
||
mapdh.a | |
||
mapdh6d.xn | |
||
mapdh6d.yz | |
||
mapdh6d.y | |
||
mapdh6d.z | |
||
mapdh6d.w | |
||
mapdh6d.wn | |
||
Assertion | mapdh6eN | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mapdh.q | |
|
2 | mapdh.i | |
|
3 | mapdh.h | |
|
4 | mapdh.m | |
|
5 | mapdh.u | |
|
6 | mapdh.v | |
|
7 | mapdh.s | |
|
8 | mapdhc.o | |
|
9 | mapdh.n | |
|
10 | mapdh.c | |
|
11 | mapdh.d | |
|
12 | mapdh.r | |
|
13 | mapdh.j | |
|
14 | mapdh.k | |
|
15 | mapdhc.f | |
|
16 | mapdh.mn | |
|
17 | mapdhcl.x | |
|
18 | mapdh.p | |
|
19 | mapdh.a | |
|
20 | mapdh6d.xn | |
|
21 | mapdh6d.yz | |
|
22 | mapdh6d.y | |
|
23 | mapdh6d.z | |
|
24 | mapdh6d.w | |
|
25 | mapdh6d.wn | |
|
26 | 3 5 14 | dvhlmod | |
27 | 24 | eldifad | |
28 | 22 | eldifad | |
29 | 6 18 | lmodvacl | |
30 | 26 27 28 29 | syl3anc | |
31 | 3 5 14 | dvhlvec | |
32 | 17 | eldifad | |
33 | 6 9 31 27 32 28 25 | lspindpi | |
34 | 33 | simprd | |
35 | 6 18 8 9 26 27 28 34 | lmodindp1 | |
36 | eldifsn | |
|
37 | 30 35 36 | sylanbrc | |
38 | 23 | eldifad | |
39 | 6 9 31 32 28 38 20 | lspindpi | |
40 | 39 | simpld | |
41 | 6 18 8 9 31 17 22 23 24 21 40 25 | mapdindp3 | |
42 | 6 18 8 9 31 17 22 23 24 21 40 25 | mapdindp4 | |
43 | 6 8 9 31 17 30 38 41 42 | lspindp1 | |
44 | 43 | simprd | |
45 | prcom | |
|
46 | 45 | fveq2i | |
47 | 46 | eleq2i | |
48 | 44 47 | sylnibr | |
49 | 6 9 31 38 32 30 42 | lspindpi | |
50 | 49 | simprd | |
51 | 50 | necomd | |
52 | eqidd | |
|
53 | eqidd | |
|
54 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 37 23 48 51 52 53 | mapdh6aN | |