Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 9-Feb-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdleme30.b | |
|
cdleme30.l | |
||
cdleme30.j | |
||
cdleme30.m | |
||
cdleme30.a | |
||
cdleme30.h | |
||
Assertion | cdleme30a | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdleme30.b | |
|
2 | cdleme30.l | |
|
3 | cdleme30.j | |
|
4 | cdleme30.m | |
|
5 | cdleme30.a | |
|
6 | cdleme30.h | |
|
7 | simp1l | |
|
8 | 7 | hllatd | |
9 | simp21 | |
|
10 | 1 5 | atbase | |
11 | 9 10 | syl | |
12 | simp23 | |
|
13 | simp1r | |
|
14 | 1 6 | lhpbase | |
15 | 13 14 | syl | |
16 | 1 4 | latmcl | |
17 | 8 12 15 16 | syl3anc | |
18 | simp22l | |
|
19 | 1 3 | latjass | |
20 | 8 11 17 18 19 | syl13anc | |
21 | simp3l | |
|
22 | simp3r | |
|
23 | 1 2 4 | latmlem1 | |
24 | 8 18 12 15 23 | syl13anc | |
25 | 22 24 | mpd | |
26 | 1 4 | latmcl | |
27 | 8 18 15 26 | syl3anc | |
28 | 1 2 3 | latjlej2 | |
29 | 8 27 17 11 28 | syl13anc | |
30 | 25 29 | mpd | |
31 | 21 30 | eqbrtrrd | |
32 | 1 3 | latjcl | |
33 | 8 11 17 32 | syl3anc | |
34 | 1 2 3 | latleeqj2 | |
35 | 8 18 33 34 | syl3anc | |
36 | 31 35 | mpbid | |
37 | simp1 | |
|
38 | 1 2 3 4 6 | lhpmod2i2 | |
39 | 37 12 18 22 38 | syl121anc | |
40 | 39 | oveq2d | |
41 | simp22 | |
|
42 | eqid | |
|
43 | 1 2 3 42 6 | lhpj1 | |
44 | 37 41 43 | syl2anc | |
45 | 44 | oveq2d | |
46 | hlol | |
|
47 | 7 46 | syl | |
48 | 1 4 42 | olm11 | |
49 | 47 12 48 | syl2anc | |
50 | 45 49 | eqtrd | |
51 | 50 | oveq2d | |
52 | 1 2 3 | latlej1 | |
53 | 8 11 27 52 | syl3anc | |
54 | 53 21 | breqtrd | |
55 | 1 2 8 11 18 12 54 22 | lattrd | |
56 | 1 2 3 | latleeqj1 | |
57 | 8 11 12 56 | syl3anc | |
58 | 55 57 | mpbid | |
59 | 40 51 58 | 3eqtrd | |
60 | 20 36 59 | 3eqtr3d | |