Proof of Theorem cdleme7ga
Step | Hyp | Ref
| Expression |
1 | | cdleme4.g |
. 2
|
2 | | simp11l 1172 |
. . 3
|
3 | | simp12l 1174 |
. . . 4
|
4 | | simp13l 1176 |
. . . 4
|
5 | | eqid 2622 |
. . . . 5
|
6 | | cdleme4.j |
. . . . 5
|
7 | | cdleme4.a |
. . . . 5
|
8 | 5, 6, 7 | hlatjcl 34653 |
. . . 4
|
9 | 2, 3, 4, 8 | syl3anc 1326 |
. . 3
|
10 | | simp11 1091 |
. . . . 5
|
11 | | simp12 1092 |
. . . . 5
|
12 | | simp13 1093 |
. . . . 5
|
13 | | simp2r 1088 |
. . . . 5
|
14 | | simp31 1097 |
. . . . 5
|
15 | | simp33 1099 |
. . . . 5
|
16 | | cdleme4.l |
. . . . . 6
|
17 | | cdleme4.m |
. . . . . 6
|
18 | | cdleme4.h |
. . . . . 6
|
19 | | cdleme4.u |
. . . . . 6
|
20 | | cdleme4.f |
. . . . . 6
|
21 | 16, 6, 17, 7, 18, 19, 20 | cdleme3fa 35523 |
. . . . 5
|
22 | 10, 11, 12, 13, 14, 15, 21 | syl132anc 1344 |
. . . 4
|
23 | | simp2l 1087 |
. . . . 5
|
24 | | simp2rl 1130 |
. . . . 5
|
25 | | simp32 1098 |
. . . . 5
|
26 | | eqid 2622 |
. . . . . 6
|
27 | 16, 6, 17, 7, 18, 19, 20, 1, 26 | cdleme7b 35531 |
. . . . 5
|
28 | 10, 23, 24, 15, 25, 27 | syl113anc 1338 |
. . . 4
|
29 | 5, 6, 7 | hlatjcl 34653 |
. . . 4
|
30 | 2, 22, 28, 29 | syl3anc 1326 |
. . 3
|
31 | | hllat 34650 |
. . . . 5
|
32 | 2, 31 | syl 17 |
. . . 4
|
33 | | eqid 2622 |
. . . . 5
|
34 | | eqid 2622 |
. . . . 5
|
35 | 6, 7, 33, 34 | linepmap 35061 |
. . . 4
|
36 | 32, 3, 4, 14, 35 | syl31anc 1329 |
. . 3
|
37 | | simp2ll 1128 |
. . . . . . 7
|
38 | 5, 6, 7 | hlatjcl 34653 |
. . . . . . 7
|
39 | 2, 37, 24, 38 | syl3anc 1326 |
. . . . . 6
|
40 | | simp11r 1173 |
. . . . . . 7
|
41 | 5, 18 | lhpbase 35284 |
. . . . . . 7
|
42 | 40, 41 | syl 17 |
. . . . . 6
|
43 | 5, 16, 17 | latmle2 17077 |
. . . . . 6
|
44 | 32, 39, 42, 43 | syl3anc 1326 |
. . . . 5
|
45 | 16, 6, 17, 7, 18, 19, 20 | cdleme3 35524 |
. . . . . 6
|
46 | 10, 11, 12, 13, 14, 15, 45 | syl132anc 1344 |
. . . . 5
|
47 | | nbrne2 4673 |
. . . . . 6
|
48 | 47 | necomd 2849 |
. . . . 5
|
49 | 44, 46, 48 | syl2anc 693 |
. . . 4
|
50 | 6, 7, 33, 34 | linepmap 35061 |
. . . 4
|
51 | 32, 22, 28, 49, 50 | syl31anc 1329 |
. . 3
|
52 | 5, 7 | atbase 34576 |
. . . . . 6
|
53 | 22, 52 | syl 17 |
. . . . 5
|
54 | 5, 17 | latmcl 17052 |
. . . . . 6
|
55 | 32, 39, 42, 54 | syl3anc 1326 |
. . . . 5
|
56 | 5, 16, 6 | latlej2 17061 |
. . . . 5
|
57 | 32, 53, 55, 56 | syl3anc 1326 |
. . . 4
|
58 | 16, 6, 17, 7, 18, 19, 20, 1, 26 | cdleme7c 35532 |
. . . . . . . 8
|
59 | 10, 11, 4, 23, 13, 14, 25, 15, 58 | syl323anc 1356 |
. . . . . . 7
|
60 | 59 | necomd 2849 |
. . . . . 6
|
61 | | hlatl 34647 |
. . . . . . . 8
|
62 | 2, 61 | syl 17 |
. . . . . . 7
|
63 | 16, 6, 17, 7, 18, 19 | lhpat2 35331 |
. . . . . . . 8
|
64 | 10, 11, 4, 14, 63 | syl112anc 1330 |
. . . . . . 7
|
65 | 16, 7 | atncmp 34599 |
. . . . . . 7
|
66 | 62, 28, 64, 65 | syl3anc 1326 |
. . . . . 6
|
67 | 60, 66 | mpbird 247 |
. . . . 5
|
68 | 5, 16, 17 | latlem12 17078 |
. . . . . . . . 9
|
69 | 32, 55, 9, 42, 68 | syl13anc 1328 |
. . . . . . . 8
|
70 | 69 | biimpd 219 |
. . . . . . 7
|
71 | 44, 70 | mpan2d 710 |
. . . . . 6
|
72 | 19 | breq2i 4661 |
. . . . . 6
|
73 | 71, 72 | syl6ibr 242 |
. . . . 5
|
74 | 67, 73 | mtod 189 |
. . . 4
|
75 | | nbrne1 4672 |
. . . . 5
|
76 | 75 | necomd 2849 |
. . . 4
|
77 | 57, 74, 76 | syl2anc 693 |
. . 3
|
78 | 16, 6, 17, 7, 18, 19, 20, 1, 26 | cdleme7e 35534 |
. . . 4
|
79 | 1, 78 | syl5eqner 2869 |
. . 3
|
80 | | eqid 2622 |
. . . 4
|
81 | 5, 17, 80, 7, 33, 34 | 2lnat 35070 |
. . 3
|
82 | 2, 9, 30, 36, 51, 77, 79, 81 | syl322anc 1354 |
. 2
|
83 | 1, 82 | syl5eqel 2705 |
1
|