Description: Lemmma for mapdh6N . Part (6) of Baer p. 47 line 39. (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 | mapdh6gN | |
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 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 | mapdh6dN | |
27 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 | mapdh6eN | |
28 | 3 5 14 | dvhlmod | |
29 | 24 | eldifad | |
30 | 22 | eldifad | |
31 | 23 | eldifad | |
32 | 6 18 | lmodass | |
33 | 28 29 30 31 32 | syl13anc | |
34 | 33 | oteq3d | |
35 | 34 | fveq2d | |
36 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 | mapdh6fN | |
37 | 36 | oveq1d | |
38 | 27 35 37 | 3eqtr3d | |
39 | 26 38 | eqtr3d | |