Description: Part of proof of Lemma K of Crawley p. 118. (Contributed by NM, 29-Jun-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemk.b | |
|
cdlemk.l | |
||
cdlemk.j | |
||
cdlemk.a | |
||
cdlemk.h | |
||
cdlemk.t | |
||
cdlemk.r | |
||
cdlemk.m | |
||
Assertion | cdlemk9 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemk.b | |
|
2 | cdlemk.l | |
|
3 | cdlemk.j | |
|
4 | cdlemk.a | |
|
5 | cdlemk.h | |
|
6 | cdlemk.t | |
|
7 | cdlemk.r | |
|
8 | cdlemk.m | |
|
9 | 1 2 3 4 5 6 7 8 | cdlemk8 | |
10 | 9 | oveq1d | |
11 | simp1 | |
|
12 | 2 4 5 6 | ltrnel | |
13 | 12 | 3adant2r | |
14 | eqid | |
|
15 | 2 8 14 4 5 | lhpmat | |
16 | 11 13 15 | syl2anc | |
17 | 16 | oveq1d | |
18 | simp1l | |
|
19 | simp2l | |
|
20 | simp3l | |
|
21 | 2 4 5 6 | ltrnat | |
22 | 11 19 20 21 | syl3anc | |
23 | simp2r | |
|
24 | 5 6 | ltrncnv | |
25 | 11 19 24 | syl2anc | |
26 | 5 6 | ltrnco | |
27 | 11 23 25 26 | syl3anc | |
28 | 1 5 6 7 | trlcl | |
29 | 11 27 28 | syl2anc | |
30 | simp1r | |
|
31 | 1 5 | lhpbase | |
32 | 30 31 | syl | |
33 | 2 5 6 7 | trlle | |
34 | 11 27 33 | syl2anc | |
35 | 1 2 3 8 4 | atmod4i2 | |
36 | 18 22 29 32 34 35 | syl131anc | |
37 | hlol | |
|
38 | 18 37 | syl | |
39 | 1 3 14 | olj02 | |
40 | 38 29 39 | syl2anc | |
41 | 17 36 40 | 3eqtr3d | |
42 | 10 41 | eqtrd | |