Step | Hyp | Ref
| Expression |
1 | | eqidd 2623 |
. 2
Scalar Scalar |
2 | | diblss.h |
. . . . 5
|
3 | | eqid 2622 |
. . . . 5
|
4 | | diblss.u |
. . . . 5
|
5 | | eqid 2622 |
. . . . 5
Scalar Scalar |
6 | | eqid 2622 |
. . . . 5
Scalar Scalar |
7 | 2, 3, 4, 5, 6 | dvhbase 36372 |
. . . 4
Scalar |
8 | 7 | eqcomd 2628 |
. . 3
Scalar |
9 | 8 | adantr 481 |
. 2
Scalar |
10 | | eqid 2622 |
. . . . 5
|
11 | | eqid 2622 |
. . . . 5
|
12 | 2, 10, 3, 4, 11 | dvhvbase 36376 |
. . . 4
|
13 | 12 | eqcomd 2628 |
. . 3
|
14 | 13 | adantr 481 |
. 2
|
15 | | eqidd 2623 |
. 2
|
16 | | eqidd 2623 |
. 2
|
17 | | diblss.s |
. . 3
|
18 | 17 | a1i 11 |
. 2
|
19 | | diblss.b |
. . . 4
|
20 | | diblss.l |
. . . 4
|
21 | | diblss.i |
. . . 4
|
22 | 19, 20, 2, 21, 4, 11 | dibss 36458 |
. . 3
|
23 | 22, 14 | sseqtr4d 3642 |
. 2
|
24 | 19, 20, 2, 21 | dibn0 36442 |
. 2
|
25 | | fvex 6201 |
. . . . . . 7
|
26 | | vex 3203 |
. . . . . . . 8
|
27 | | fvex 6201 |
. . . . . . . 8
|
28 | 26, 27 | coex 7118 |
. . . . . . 7
|
29 | 25, 28 | op1st 7176 |
. . . . . 6
|
30 | 29 | coeq1i 5281 |
. . . . 5
|
31 | | simpll 790 |
. . . . . . 7
|
32 | | simpr1 1067 |
. . . . . . . 8
|
33 | | simplr 792 |
. . . . . . . . 9
|
34 | | simpr2 1068 |
. . . . . . . . 9
|
35 | 19, 20, 2, 10, 21 | dibelval1st1 36439 |
. . . . . . . . 9
|
36 | 31, 33, 34, 35 | syl3anc 1326 |
. . . . . . . 8
|
37 | 2, 10, 3 | tendocl 36055 |
. . . . . . . 8
|
38 | 31, 32, 36, 37 | syl3anc 1326 |
. . . . . . 7
|
39 | | simpr3 1069 |
. . . . . . . 8
|
40 | 19, 20, 2, 10, 21 | dibelval1st1 36439 |
. . . . . . . 8
|
41 | 31, 33, 39, 40 | syl3anc 1326 |
. . . . . . 7
|
42 | 2, 10 | ltrnco 36007 |
. . . . . . 7
|
43 | 31, 38, 41, 42 | syl3anc 1326 |
. . . . . 6
|
44 | | simplll 798 |
. . . . . . . 8
|
45 | | hllat 34650 |
. . . . . . . 8
|
46 | 44, 45 | syl 17 |
. . . . . . 7
|
47 | | eqid 2622 |
. . . . . . . . 9
|
48 | 19, 2, 10, 47 | trlcl 35451 |
. . . . . . . 8
|
49 | 31, 43, 48 | syl2anc 693 |
. . . . . . 7
|
50 | 19, 2, 10, 47 | trlcl 35451 |
. . . . . . . . 9
|
51 | 31, 38, 50 | syl2anc 693 |
. . . . . . . 8
|
52 | 19, 2, 10, 47 | trlcl 35451 |
. . . . . . . . 9
|
53 | 31, 41, 52 | syl2anc 693 |
. . . . . . . 8
|
54 | | eqid 2622 |
. . . . . . . . 9
|
55 | 19, 54 | latjcl 17051 |
. . . . . . . 8
|
56 | 46, 51, 53, 55 | syl3anc 1326 |
. . . . . . 7
|
57 | | simplrl 800 |
. . . . . . 7
|
58 | 20, 54, 2, 10, 47 | trlco 36015 |
. . . . . . . 8
|
59 | 31, 38, 41, 58 | syl3anc 1326 |
. . . . . . 7
|
60 | 19, 2, 10, 47 | trlcl 35451 |
. . . . . . . . . 10
|
61 | 31, 36, 60 | syl2anc 693 |
. . . . . . . . 9
|
62 | 20, 2, 10, 47, 3 | tendotp 36049 |
. . . . . . . . . 10
|
63 | 31, 32, 36, 62 | syl3anc 1326 |
. . . . . . . . 9
|
64 | | eqid 2622 |
. . . . . . . . . . . 12
|
65 | 19, 20, 2, 64, 21 | dibelval1st 36438 |
. . . . . . . . . . 11
|
66 | 31, 33, 34, 65 | syl3anc 1326 |
. . . . . . . . . 10
|
67 | 19, 20, 2, 10, 47, 64 | diatrl 36333 |
. . . . . . . . . 10
|
68 | 31, 33, 66, 67 | syl3anc 1326 |
. . . . . . . . 9
|
69 | 19, 20, 46, 51, 61, 57, 63, 68 | lattrd 17058 |
. . . . . . . 8
|
70 | 19, 20, 2, 64, 21 | dibelval1st 36438 |
. . . . . . . . . 10
|
71 | 31, 33, 39, 70 | syl3anc 1326 |
. . . . . . . . 9
|
72 | 19, 20, 2, 10, 47, 64 | diatrl 36333 |
. . . . . . . . 9
|
73 | 31, 33, 71, 72 | syl3anc 1326 |
. . . . . . . 8
|
74 | 19, 20, 54 | latjle12 17062 |
. . . . . . . . 9
|
75 | 46, 51, 53, 57, 74 | syl13anc 1328 |
. . . . . . . 8
|
76 | 69, 73, 75 | mpbi2and 956 |
. . . . . . 7
|
77 | 19, 20, 46, 49, 56, 57, 59, 76 | lattrd 17058 |
. . . . . 6
|
78 | 19, 20, 2, 10, 47, 64 | diaelval 36322 |
. . . . . . 7
|
79 | 78 | adantr 481 |
. . . . . 6
|
80 | 43, 77, 79 | mpbir2and 957 |
. . . . 5
|
81 | 30, 80 | syl5eqel 2705 |
. . . 4
|
82 | | eqid 2622 |
. . . . . . . . 9
|
83 | | eqid 2622 |
. . . . . . . . 9
Scalar Scalar |
84 | 2, 10, 3, 4, 5, 82,
83 | dvhfplusr 36373 |
. . . . . . . 8
Scalar |
85 | 84 | ad2antrr 762 |
. . . . . . 7
Scalar |
86 | 25, 28 | op2nd 7177 |
. . . . . . . 8
|
87 | | eqid 2622 |
. . . . . . . . . . . 12
|
88 | 19, 20, 2, 10, 87, 21 | dibelval2nd 36441 |
. . . . . . . . . . 11
|
89 | 31, 33, 34, 88 | syl3anc 1326 |
. . . . . . . . . 10
|
90 | 89 | coeq2d 5284 |
. . . . . . . . 9
|
91 | 19, 2, 10, 3, 87 | tendo0mulr 36115 |
. . . . . . . . . 10
|
92 | 31, 32, 91 | syl2anc 693 |
. . . . . . . . 9
|
93 | 90, 92 | eqtrd 2656 |
. . . . . . . 8
|
94 | 86, 93 | syl5eq 2668 |
. . . . . . 7
|
95 | 19, 20, 2, 10, 87, 21 | dibelval2nd 36441 |
. . . . . . . 8
|
96 | 31, 33, 39, 95 | syl3anc 1326 |
. . . . . . 7
|
97 | 85, 94, 96 | oveq123d 6671 |
. . . . . 6
Scalar |
98 | | simpllr 799 |
. . . . . . 7
|
99 | 19, 2, 10, 3, 87 | tendo0cl 36078 |
. . . . . . . 8
|
100 | 99 | ad2antrr 762 |
. . . . . . 7
|
101 | 19, 2, 10, 3, 87, 82 | tendo0pl 36079 |
. . . . . . 7
|
102 | 44, 98, 100, 101 | syl21anc 1325 |
. . . . . 6
|
103 | 97, 102 | eqtrd 2656 |
. . . . 5
Scalar |
104 | | ovex 6678 |
. . . . . 6
Scalar |
105 | 104 | elsn 4192 |
. . . . 5
Scalar Scalar |
106 | 103, 105 | sylibr 224 |
. . . 4
Scalar |
107 | | opelxpi 5148 |
. . . 4
Scalar
Scalar
|
108 | 81, 106, 107 | syl2anc 693 |
. . 3
Scalar
|
109 | 23 | adantr 481 |
. . . . . . 7
|
110 | 109, 34 | sseldd 3604 |
. . . . . 6
|
111 | | eqid 2622 |
. . . . . . 7
|
112 | 2, 10, 3, 4, 111 | dvhvsca 36390 |
. . . . . 6
|
113 | 31, 32, 110, 112 | syl12anc 1324 |
. . . . 5
|
114 | 113 | oveq1d 6665 |
. . . 4
|
115 | 89, 100 | eqeltrd 2701 |
. . . . . . 7
|
116 | 2, 3 | tendococl 36060 |
. . . . . . 7
|
117 | 31, 32, 115, 116 | syl3anc 1326 |
. . . . . 6
|
118 | | opelxpi 5148 |
. . . . . 6
|
119 | 38, 117, 118 | syl2anc 693 |
. . . . 5
|
120 | 109, 39 | sseldd 3604 |
. . . . 5
|
121 | | eqid 2622 |
. . . . . 6
|
122 | 2, 10, 3, 4, 5, 121, 83 | dvhvadd 36381 |
. . . . 5
Scalar |
123 | 31, 119, 120, 122 | syl12anc 1324 |
. . . 4
Scalar |
124 | 114, 123 | eqtrd 2656 |
. . 3
Scalar |
125 | 19, 20, 2, 10, 87, 64, 21 | dibval2 36433 |
. . . 4
|
126 | 125 | adantr 481 |
. . 3
|
127 | 108, 124,
126 | 3eltr4d 2716 |
. 2
|
128 | 1, 9, 14, 15, 16, 18, 23, 24, 127 | islssd 18936 |
1
|