Proof of Theorem trlcolem
Step | Hyp | Ref
| Expression |
1 | | simp1l 1085 |
. . . . . 6
|
2 | | hllat 34650 |
. . . . . 6
|
3 | 1, 2 | syl 17 |
. . . . 5
|
4 | | simp3l 1089 |
. . . . . 6
|
5 | | eqid 2622 |
. . . . . . 7
|
6 | | trlcolem.a |
. . . . . . 7
|
7 | 5, 6 | atbase 34576 |
. . . . . 6
|
8 | 4, 7 | syl 17 |
. . . . 5
|
9 | | simp1 1061 |
. . . . . . 7
|
10 | | simp2r 1088 |
. . . . . . 7
|
11 | | trlco.l |
. . . . . . . 8
|
12 | | trlco.h |
. . . . . . . 8
|
13 | | trlco.t |
. . . . . . . 8
|
14 | 11, 6, 12, 13 | ltrnat 35426 |
. . . . . . 7
|
15 | 9, 10, 4, 14 | syl3anc 1326 |
. . . . . 6
|
16 | 5, 6 | atbase 34576 |
. . . . . 6
|
17 | 15, 16 | syl 17 |
. . . . 5
|
18 | | trlco.j |
. . . . . 6
|
19 | 5, 11, 18 | latlej1 17060 |
. . . . 5
|
20 | 3, 8, 17, 19 | syl3anc 1326 |
. . . 4
|
21 | 5, 18, 6 | hlatjcl 34653 |
. . . . . 6
|
22 | 1, 4, 15, 21 | syl3anc 1326 |
. . . . 5
|
23 | | simp2l 1087 |
. . . . . 6
|
24 | 5, 12, 13 | ltrncl 35411 |
. . . . . 6
|
25 | 9, 23, 17, 24 | syl3anc 1326 |
. . . . 5
|
26 | 5, 11, 18 | latjlej1 17065 |
. . . . 5
|
27 | 3, 8, 22, 25, 26 | syl13anc 1328 |
. . . 4
|
28 | 20, 27 | mpd 15 |
. . 3
|
29 | 5, 18 | latjcl 17051 |
. . . . 5
|
30 | 3, 8, 25, 29 | syl3anc 1326 |
. . . 4
|
31 | 5, 18 | latjcl 17051 |
. . . . 5
|
32 | 3, 22, 25, 31 | syl3anc 1326 |
. . . 4
|
33 | | simp1r 1086 |
. . . . 5
|
34 | 5, 12 | lhpbase 35284 |
. . . . 5
|
35 | 33, 34 | syl 17 |
. . . 4
|
36 | | trlcolem.m |
. . . . 5
|
37 | 5, 11, 36 | latmlem1 17081 |
. . . 4
|
38 | 3, 30, 32, 35, 37 | syl13anc 1328 |
. . 3
|
39 | 28, 38 | mpd 15 |
. 2
|
40 | 12, 13 | ltrnco 36007 |
. . . . 5
|
41 | 9, 23, 10, 40 | syl3anc 1326 |
. . . 4
|
42 | | trlco.r |
. . . . 5
|
43 | 11, 18, 36, 6, 12, 13, 42 | trlval2 35450 |
. . . 4
|
44 | 41, 43 | syld3an2 1373 |
. . 3
|
45 | 11, 6, 12, 13 | ltrncoval 35431 |
. . . . . 6
|
46 | 45 | 3adant3r 1323 |
. . . . 5
|
47 | 46 | oveq2d 6666 |
. . . 4
|
48 | 47 | oveq1d 6665 |
. . 3
|
49 | 44, 48 | eqtrd 2656 |
. 2
|
50 | 11, 6, 12, 13 | ltrnel 35425 |
. . . . . 6
|
51 | 10, 50 | syld3an2 1373 |
. . . . 5
|
52 | 11, 18, 36, 6, 12, 13, 42 | trlval2 35450 |
. . . . 5
|
53 | 9, 23, 51, 52 | syl3anc 1326 |
. . . 4
|
54 | 11, 18, 36, 6, 12, 13, 42 | trlval2 35450 |
. . . . 5
|
55 | 10, 54 | syld3an2 1373 |
. . . 4
|
56 | 53, 55 | oveq12d 6668 |
. . 3
|
57 | 11, 6, 12, 13 | ltrnat 35426 |
. . . . . . 7
|
58 | 9, 23, 15, 57 | syl3anc 1326 |
. . . . . 6
|
59 | 5, 18, 6 | hlatjcl 34653 |
. . . . . 6
|
60 | 1, 15, 58, 59 | syl3anc 1326 |
. . . . 5
|
61 | 5, 36 | latmcl 17052 |
. . . . 5
|
62 | 3, 60, 35, 61 | syl3anc 1326 |
. . . 4
|
63 | 5, 36 | latmcl 17052 |
. . . . 5
|
64 | 3, 22, 35, 63 | syl3anc 1326 |
. . . 4
|
65 | 5, 18 | latjcom 17059 |
. . . 4
|
66 | 3, 62, 64, 65 | syl3anc 1326 |
. . 3
|
67 | 5, 18 | latjcl 17051 |
. . . . . 6
|
68 | 3, 17, 25, 67 | syl3anc 1326 |
. . . . 5
|
69 | 5, 11, 36 | latmle2 17077 |
. . . . . 6
|
70 | 3, 22, 35, 69 | syl3anc 1326 |
. . . . 5
|
71 | 5, 11, 18, 36, 12 | lhpmod6i1 35325 |
. . . . 5
|
72 | 9, 64, 68, 70, 71 | syl121anc 1331 |
. . . 4
|
73 | 5, 18 | latjass 17095 |
. . . . . . 7
|
74 | 3, 64, 17, 25, 73 | syl13anc 1328 |
. . . . . 6
|
75 | 5, 11, 18 | latlej2 17061 |
. . . . . . . . . 10
|
76 | 3, 8, 17, 75 | syl3anc 1326 |
. . . . . . . . 9
|
77 | 5, 11, 18, 36, 12 | lhpmod2i2 35324 |
. . . . . . . . 9
|
78 | 9, 22, 17, 76, 77 | syl121anc 1331 |
. . . . . . . 8
|
79 | | eqid 2622 |
. . . . . . . . . . 11
|
80 | 11, 18, 79, 6, 12 | lhpjat1 35306 |
. . . . . . . . . 10
|
81 | 9, 51, 80 | syl2anc 693 |
. . . . . . . . 9
|
82 | 81 | oveq2d 6666 |
. . . . . . . 8
|
83 | | hlol 34648 |
. . . . . . . . . 10
|
84 | 1, 83 | syl 17 |
. . . . . . . . 9
|
85 | 5, 36, 79 | olm11 34514 |
. . . . . . . . 9
|
86 | 84, 22, 85 | syl2anc 693 |
. . . . . . . 8
|
87 | 78, 82, 86 | 3eqtrd 2660 |
. . . . . . 7
|
88 | 87 | oveq1d 6665 |
. . . . . 6
|
89 | 74, 88 | eqtr3d 2658 |
. . . . 5
|
90 | 89 | oveq1d 6665 |
. . . 4
|
91 | 72, 90 | eqtrd 2656 |
. . 3
|
92 | 56, 66, 91 | 3eqtrd 2660 |
. 2
|
93 | 39, 49, 92 | 3brtr4d 4685 |
1
|