Description: Part of proof of Lemma E in Crawley p. 113. Show that f(x) is one-to-one on P .\/ Q line. TODO: FIX COMMENT. (Contributed by NM, 13-Mar-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdleme37.l | |
|
cdleme37.j | |
||
cdleme37.m | |
||
cdleme37.a | |
||
cdleme37.h | |
||
cdleme37.u | |
||
cdleme37.e | |
||
cdleme37.d | |
||
cdleme37.v | |
||
cdleme37.x | |
||
cdleme37.c | |
||
cdleme37.g | |
||
Assertion | cdleme37m | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdleme37.l | |
|
2 | cdleme37.j | |
|
3 | cdleme37.m | |
|
4 | cdleme37.a | |
|
5 | cdleme37.h | |
|
6 | cdleme37.u | |
|
7 | cdleme37.e | |
|
8 | cdleme37.d | |
|
9 | cdleme37.v | |
|
10 | cdleme37.x | |
|
11 | cdleme37.c | |
|
12 | cdleme37.g | |
|
13 | simp1 | |
|
14 | simp23 | |
|
15 | simp32l | |
|
16 | simp33l | |
|
17 | simp21 | |
|
18 | simp32r | |
|
19 | simp33r | |
|
20 | simp31r | |
|
21 | 18 19 20 | 3jca | |
22 | eqid | |
|
23 | eqid | |
|
24 | eqid | |
|
25 | eqid | |
|
26 | 1 2 3 4 5 6 7 8 22 23 24 25 | cdleme21k | |
27 | 13 14 15 16 17 21 26 | syl132anc | |
28 | simp11 | |
|
29 | simp12l | |
|
30 | simp13l | |
|
31 | 1 2 3 4 5 6 | cdleme4 | |
32 | 28 29 30 14 20 31 | syl131anc | |
33 | 1 2 3 4 5 6 7 | cdleme2 | |
34 | 28 29 30 15 33 | syl13anc | |
35 | 9 34 | eqtrid | |
36 | 35 | oveq2d | |
37 | 32 36 | eqtr4d | |
38 | simp11l | |
|
39 | simp23l | |
|
40 | 15 | simpld | |
41 | 2 4 | hlatjcom | |
42 | 38 39 40 41 | syl3anc | |
43 | 42 | oveq1d | |
44 | 43 | oveq2d | |
45 | 37 44 | oveq12d | |
46 | 11 45 | eqtr4id | |
47 | 1 2 3 4 5 6 8 | cdleme2 | |
48 | 28 29 30 16 47 | syl13anc | |
49 | 10 48 | eqtrid | |
50 | 49 | oveq2d | |
51 | 32 50 | eqtr4d | |
52 | 16 | simpld | |
53 | 2 4 | hlatjcom | |
54 | 38 39 52 53 | syl3anc | |
55 | 54 | oveq1d | |
56 | 55 | oveq2d | |
57 | 51 56 | oveq12d | |
58 | 12 57 | eqtr4id | |
59 | 27 46 58 | 3eqtr4d | |