Description: TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemg2inv.h | |
|
cdlemg2inv.t | |
||
cdlemg2j.l | |
||
cdlemg2j.j | |
||
cdlemg2j.a | |
||
cdlemg2j.m | |
||
cdlemg2j.u | |
||
Assertion | cdlemg2m | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemg2inv.h | |
|
2 | cdlemg2inv.t | |
|
3 | cdlemg2j.l | |
|
4 | cdlemg2j.j | |
|
5 | cdlemg2j.a | |
|
6 | cdlemg2j.m | |
|
7 | cdlemg2j.u | |
|
8 | 1 2 3 4 5 6 7 | cdlemg2k | |
9 | 8 | oveq1d | |
10 | simp1 | |
|
11 | simp3 | |
|
12 | simp2l | |
|
13 | eqid | |
|
14 | 3 6 13 5 1 2 | ltrnmw | |
15 | 10 11 12 14 | syl3anc | |
16 | 15 | oveq1d | |
17 | simp1l | |
|
18 | 3 5 1 2 | ltrnel | |
19 | 10 11 12 18 | syl3anc | |
20 | 19 | simpld | |
21 | simp1r | |
|
22 | simp2ll | |
|
23 | simp2rl | |
|
24 | eqid | |
|
25 | 3 4 6 5 1 7 24 | cdleme0aa | |
26 | 17 21 22 23 25 | syl211anc | |
27 | 24 1 | lhpbase | |
28 | 21 27 | syl | |
29 | 17 | hllatd | |
30 | 24 4 5 | hlatjcl | |
31 | 17 22 23 30 | syl3anc | |
32 | 24 3 6 | latmle2 | |
33 | 29 31 28 32 | syl3anc | |
34 | 7 33 | eqbrtrid | |
35 | 24 3 4 6 5 | atmod4i2 | |
36 | 17 20 26 28 34 35 | syl131anc | |
37 | hlol | |
|
38 | 17 37 | syl | |
39 | 24 4 13 | olj02 | |
40 | 38 26 39 | syl2anc | |
41 | 16 36 40 | 3eqtr3d | |
42 | 9 41 | eqtrd | |