Description: Part of proof of Lemma E in Crawley p. 113, last paragraph on p. 114. D , F , Y , G represent s_2, f(s), t_2, f(t). (Contributed by NM, 14-Nov-2012) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdleme19.l | |
|
cdleme19.j | |
||
cdleme19.m | |
||
cdleme19.a | |
||
cdleme19.h | |
||
cdleme19.u | |
||
cdleme19.f | |
||
cdleme19.g | |
||
cdleme19.d | |
||
cdleme19.y | |
||
cdleme20.v | |
||
Assertion | cdleme20aN | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdleme19.l | |
|
2 | cdleme19.j | |
|
3 | cdleme19.m | |
|
4 | cdleme19.a | |
|
5 | cdleme19.h | |
|
6 | cdleme19.u | |
|
7 | cdleme19.f | |
|
8 | cdleme19.g | |
|
9 | cdleme19.d | |
|
10 | cdleme19.y | |
|
11 | cdleme20.v | |
|
12 | 11 | oveq1i | |
13 | simp1l | |
|
14 | simp1r | |
|
15 | simp22 | |
|
16 | simp23 | |
|
17 | simp21 | |
|
18 | simp33 | |
|
19 | simp32 | |
|
20 | 1 2 3 4 5 9 | cdlemeda | |
21 | 13 14 15 16 17 18 19 20 | syl223anc | |
22 | simp31 | |
|
23 | eqid | |
|
24 | 23 2 4 | hlatjcl | |
25 | 13 15 22 24 | syl3anc | |
26 | 23 5 | lhpbase | |
27 | 14 26 | syl | |
28 | 13 | hllatd | |
29 | 23 2 4 | hlatjcl | |
30 | 13 17 15 29 | syl3anc | |
31 | 23 1 3 | latmle2 | |
32 | 28 30 27 31 | syl3anc | |
33 | 9 32 | eqbrtrid | |
34 | 23 1 2 3 4 | atmod4i1 | |
35 | 13 21 25 27 33 34 | syl131anc | |
36 | 1 2 3 4 5 9 | cdleme10 | |
37 | 13 14 17 15 16 36 | syl212anc | |
38 | 37 | oveq1d | |
39 | 2 4 | hlatj32 | |
40 | 13 15 21 22 39 | syl13anc | |
41 | 38 40 | eqtr3d | |
42 | 41 | oveq1d | |
43 | 35 42 | eqtr4d | |
44 | 12 43 | eqtrid | |