Step | Hyp | Ref
| Expression |
1 | | dihopelvalcp.b |
. . . 4
     |
2 | | dihopelvalcp.l |
. . . 4
     |
3 | | dihopelvalcp.j |
. . . 4
     |
4 | | dihopelvalcp.m |
. . . 4
     |
5 | | dihopelvalcp.a |
. . . 4
     |
6 | | dihopelvalcp.h |
. . . 4
     |
7 | | dihopelvalcp.i |
. . . 4
         |
8 | | dihopelvalcp.n |
. . . 4
         |
9 | | dihopelvalcp.c |
. . . 4
         |
10 | | dihopelvalcp.u |
. . . 4
         |
11 | | dihopelvalcp.y |
. . . 4
     |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | dihvalcq 34875 |
. . 3
          
   
            
     |
13 | 12 | eleq2d 2534 |
. 2
          
   
                          |
14 | | simp1 1030 |
. . 3
          
   
    |
15 | | simp3l 1058 |
. . . 4
          
   

   |
16 | | dihopelvalcp.v |
. . . . 5
     |
17 | 2, 5, 6, 10, 9, 16 | diclss 34832 |
. . . 4
             |
18 | 14, 15, 17 | syl2anc 673 |
. . 3
          
   
      |
19 | | simp1l 1054 |
. . . . . 6
          
   
  |
20 | | hllat 33000 |
. . . . . 6
   |
21 | 19, 20 | syl 17 |
. . . . 5
          
   
  |
22 | | simp2l 1056 |
. . . . 5
          
   
  |
23 | | simp1r 1055 |
. . . . . 6
          
   
  |
24 | 1, 6 | lhpbase 33634 |
. . . . . 6
   |
25 | 23, 24 | syl 17 |
. . . . 5
          
   
  |
26 | 1, 4 | latmcl 16376 |
. . . . 5
 
     |
27 | 21, 22, 25, 26 | syl3anc 1292 |
. . . 4
          
   
    |
28 | 1, 2, 4 | latmle2 16401 |
. . . . 5
 
     |
29 | 21, 22, 25, 28 | syl3anc 1292 |
. . . 4
          
   
    |
30 | 1, 2, 6, 10, 8, 16 | diblss 34809 |
. . . 4
                   |
31 | 14, 27, 29, 30 | syl12anc 1290 |
. . 3
          
   
        |
32 | | dihopelvalcp.d |
. . . 4
    |
33 | 6, 10, 32, 16, 11 | dvhopellsm 34756 |
. . 3
                                                                         |
34 | 14, 18, 31, 33 | syl3anc 1292 |
. 2
          
   
            
  
                
  
                      |
35 | | dihopelvalcp.p |
. . . . . . . . 9
         |
36 | | dihopelvalcp.t |
. . . . . . . . 9
         |
37 | | dihopelvalcp.e |
. . . . . . . . 9
         |
38 | | dihopelvalcp.g |
. . . . . . . . 9
        |
39 | | vex 3034 |
. . . . . . . . 9
 |
40 | | vex 3034 |
. . . . . . . . 9
 |
41 | 2, 5, 6, 35, 36, 37, 9, 38, 39, 40 | dicopelval2 34820 |
. . . . . . . 8
              
         |
42 | 14, 15, 41 | syl2anc 673 |
. . . . . . 7
          
   
                 |
43 | | dihopelvalcp.r |
. . . . . . . . 9
         |
44 | | dihopelvalcp.z |
. . . . . . . . 9
    |
45 | 1, 2, 6, 36, 43, 44, 8 | dibopelval3 34787 |
. . . . . . . 8
                  
               |
46 | 14, 27, 29, 45 | syl12anc 1290 |
. . . . . . 7
          
   
                
      |
47 | 42, 46 | anbi12d 725 |
. . . . . 6
          
   
        
  
            
               |
48 | 47 | anbi1d 719 |
. . . . 5
          
   
                               
       
            
             |
49 | | simpl1 1033 |
. . . . . . . . . . 11
     
    
                            |
50 | | simprll 780 |
. . . . . . . . . . . 12
     
    
                              |
51 | | simprlr 781 |
. . . . . . . . . . . . 13
     
    
                          |
52 | 2, 5, 6, 35 | lhpocnel2 33655 |
. . . . . . . . . . . . . . 15
 
     |
53 | 49, 52 | syl 17 |
. . . . . . . . . . . . . 14
     
    
                            |
54 | | simpl3l 1085 |
. . . . . . . . . . . . . 14
     
    
                            |
55 | 2, 5, 6, 36, 38 | ltrniotacl 34217 |
. . . . . . . . . . . . . 14
      
 
  |
56 | 49, 53, 54, 55 | syl3anc 1292 |
. . . . . . . . . . . . 13
     
    
                          |
57 | 6, 36, 37 | tendocl 34405 |
. . . . . . . . . . . . 13
   

      |
58 | 49, 51, 56, 57 | syl3anc 1292 |
. . . . . . . . . . . 12
     
    
                              |
59 | 50, 58 | eqeltrd 2549 |
. . . . . . . . . . 11
     
    
                          |
60 | | simprll 780 |
. . . . . . . . . . . 12
       
             |
61 | 60 | adantl 473 |
. . . . . . . . . . 11
     
    
                          |
62 | | simprrr 783 |
. . . . . . . . . . . 12
     
    
                          |
63 | 1, 6, 36, 37, 44 | tendo0cl 34428 |
. . . . . . . . . . . . 13
 
   |
64 | 49, 63 | syl 17 |
. . . . . . . . . . . 12
     
    
                          |
65 | 62, 64 | eqeltrd 2549 |
. . . . . . . . . . 11
     
    
                          |
66 | | eqid 2471 |
. . . . . . . . . . . 12
Scalar  Scalar   |
67 | | eqid 2471 |
. . . . . . . . . . . 12
  Scalar     Scalar    |
68 | 6, 36, 37, 10, 66, 32, 67 | dvhopvadd 34732 |
. . . . . . . . . . 11
      
 
                Scalar        |
69 | 49, 59, 51, 61, 65, 68 | syl122anc 1301 |
. . . . . . . . . 10
     
    
                                        Scalar        |
70 | | dihopelvalcp.o |
. . . . . . . . . . . . . 14
 
              |
71 | 6, 36, 37, 10, 66, 70, 67 | dvhfplusr 34723 |
. . . . . . . . . . . . 13
 
   Scalar     |
72 | 49, 71 | syl 17 |
. . . . . . . . . . . 12
     
    
                          Scalar     |
73 | 72 | oveqd 6325 |
. . . . . . . . . . 11
     
    
                            Scalar           |
74 | 73 | opeq2d 4165 |
. . . . . . . . . 10
     
    
                                Scalar     
           |
75 | 69, 74 | eqtrd 2505 |
. . . . . . . . 9
     
    
                                           |
76 | 75 | eqeq2d 2481 |
. . . . . . . 8
     
    
                                                   |
77 | | dihopelvalcp.f |
. . . . . . . . . 10
 |
78 | | dihopelvalcp.s |
. . . . . . . . . 10
 |
79 | 77, 78 | opth 4676 |
. . . . . . . . 9
  
            
       |
80 | 62 | oveq2d 6324 |
. . . . . . . . . . . 12
     
    
                                  |
81 | 1, 6, 36, 37, 44, 70 | tendo0plr 34430 |
. . . . . . . . . . . . 13
    
      |
82 | 49, 51, 81 | syl2anc 673 |
. . . . . . . . . . . 12
     
    
                              |
83 | 80, 82 | eqtrd 2505 |
. . . . . . . . . . 11
     
    
                              |
84 | 83 | eqeq2d 2481 |
. . . . . . . . . 10
     
    
                            
   |
85 | 84 | anbi2d 718 |
. . . . . . . . 9
     
    
                                
       |
86 | 79, 85 | syl5bb 265 |
. . . . . . . 8
     
    
                                    
       |
87 | 76, 86 | bitrd 261 |
. . . . . . 7
     
    
                                      
    |
88 | 87 | pm5.32da 653 |
. . . . . 6
          
   
       
             
         
       
           
       |
89 | | simplll 776 |
. . . . . . . . . . 11
       
            
          |
90 | 89 | adantl 473 |
. . . . . . . . . 10
     
    
           
       
    
    
      |
91 | | simprrr 783 |
. . . . . . . . . . 11
     
    
           
       
    
    
  |
92 | 91 | fveq1d 5881 |
. . . . . . . . . 10
     
    
           
       
    
               |
93 | 90, 92 | eqtr4d 2508 |
. . . . . . . . 9
     
    
           
       
    
    
      |
94 | 91 | eqcomd 2477 |
. . . . . . . . 9
     
    
           
       
    
       |
95 | | coass 5361 |
. . . . . . . . . . 11
                           |
96 | | simpl1 1033 |
. . . . . . . . . . . . . . 15
     
    
           
       
    
         |
97 | | simpllr 777 |
. . . . . . . . . . . . . . . . . 18
       
            
      |
98 | 97 | adantl 473 |
. . . . . . . . . . . . . . . . 17
     
    
           
       
    
       |
99 | 91, 98 | eqeltrd 2549 |
. . . . . . . . . . . . . . . 16
     
    
           
       
    
    
  |
100 | 56 | adantrr 731 |
. . . . . . . . . . . . . . . 16
     
    
           
       
    
    
  |
101 | 6, 36, 37 | tendocl 34405 |
. . . . . . . . . . . . . . . 16
   

      |
102 | 96, 99, 100, 101 | syl3anc 1292 |
. . . . . . . . . . . . . . 15
     
    
           
       
    
           |
103 | 1, 6, 36 | ltrn1o 33760 |
. . . . . . . . . . . . . . 15
        
          |
104 | 96, 102, 103 | syl2anc 673 |
. . . . . . . . . . . . . 14
     
    
           
       
    
               |
105 | | f1ococnv1 5856 |
. . . . . . . . . . . . . 14
        
              |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . 13
     
    
           
       
    
               
   |
107 | 106 | coeq1d 5001 |
. . . . . . . . . . . 12
     
    
           
       
    
                       |
108 | 60 | ad2antrl 742 |
. . . . . . . . . . . . . 14
     
    
           
       
    
       |
109 | 1, 6, 36 | ltrn1o 33760 |
. . . . . . . . . . . . . 14
    
      |
110 | 96, 108, 109 | syl2anc 673 |
. . . . . . . . . . . . 13
     
    
           
       
    
           |
111 | | f1of 5828 |
. . . . . . . . . . . . 13
    
      |
112 | | fcoi2 5770 |
. . . . . . . . . . . . 13
          |
113 | 110, 111,
112 | 3syl 18 |
. . . . . . . . . . . 12
     
    
           
       
    
          |
114 | 107, 113 | eqtr2d 2506 |
. . . . . . . . . . 11
     
    
           
       
    
                    |
115 | | simprrl 782 |
. . . . . . . . . . . . . 14
     
    
           
       
    
    
    |
116 | 93 | coeq1d 5001 |
. . . . . . . . . . . . . 14
     
    
           
       
    
               |
117 | 115, 116 | eqtrd 2505 |
. . . . . . . . . . . . 13
     
    
           
       
    
    
        |
118 | 117 | coeq1d 5001 |
. . . . . . . . . . . 12
     
    
           
       
    
                           |
119 | 6, 36 | ltrncnv 33782 |
. . . . . . . . . . . . . 14
        
       |
120 | 96, 102, 119 | syl2anc 673 |
. . . . . . . . . . . . 13
     
    
           
       
    
            |
121 | 6, 36 | ltrnco 34357 |
. . . . . . . . . . . . . 14
       

        |
122 | 96, 102, 108, 121 | syl3anc 1292 |
. . . . . . . . . . . . 13
     
    
           
       
    
             |
123 | 6, 36 | ltrncom 34376 |
. . . . . . . . . . . . 13
                                            |
124 | 96, 120, 122, 123 | syl3anc 1292 |
. . . . . . . . . . . 12
     
    
           
       
    
                                 |
125 | 118, 124 | eqtr4d 2508 |
. . . . . . . . . . 11
     
    
           
       
    
                           |
126 | 95, 114, 125 | 3eqtr4a 2531 |
. . . . . . . . . 10
     
    
           
       
    
              |
127 | | simplrr 779 |
. . . . . . . . . . 11
       
            
      |
128 | 127 | adantl 473 |
. . . . . . . . . 10
     
    
           
       
    
    
  |
129 | 126, 128 | jca 541 |
. . . . . . . . 9
     
    
           
       
    
                |
130 | 93, 94, 129 | jca31 543 |
. . . . . . . 8
     
    
           
       
    
          
             |
131 | 130 | ex 441 |
. . . . . . 7
          
   
       
            
                  
     |
132 | 131 | pm4.71rd 647 |
. . . . . 6
          
   
       
            
   
               
 
       
           
        |
133 | 88, 132 | bitrd 261 |
. . . . 5
          
   
       
             
         
               
 
       
           
        |
134 | | simprrl 782 |
. . . . . . . . . 10
      
    
                                          
    
    |
135 | | simpll1 1069 |
. . . . . . . . . . 11
      
    
                                          
         |
136 | 89 | adantl 473 |
. . . . . . . . . . . 12
      
    
                                          
    
      |
137 | 97 | adantl 473 |
. . . . . . . . . . . . 13
      
    
                                          
       |
138 | 135, 52 | syl 17 |
. . . . . . . . . . . . . 14
      
    
                                          
         |
139 | | simpl3l 1085 |
. . . . . . . . . . . . . . 15
     
    
                           |
140 | 139 | adantr 472 |
. . . . . . . . . . . . . 14
      
    
                                          
         |
141 | 135, 138,
140, 55 | syl3anc 1292 |
. . . . . . . . . . . . 13
      
    
                                          
    
  |
142 | 135, 137,
141, 57 | syl3anc 1292 |
. . . . . . . . . . . 12
      
    
                                          
           |
143 | 136, 142 | eqeltrd 2549 |
. . . . . . . . . . 11
      
    
                                          
    
  |
144 | 60 | ad2antrl 742 |
. . . . . . . . . . 11
      
    
                                          
       |
145 | 6, 36 | ltrnco 34357 |
. . . . . . . . . . 11
   

    |
146 | 135, 143,
144, 145 | syl3anc 1292 |
. . . . . . . . . 10
      
    
                                          
         |
147 | 134, 146 | eqeltrd 2549 |
. . . . . . . . 9
      
    
                                          
    
  |
148 | | simpl1l 1081 |
. . . . . . . . . . . 12
     
    
                      
  |
149 | 148 | adantr 472 |
. . . . . . . . . . 11
      
    
                                          
    
  |
150 | 149, 20 | syl 17 |
. . . . . . . . . 10
      
    
                                          
    
  |
151 | 1, 6, 36, 43 | trlcl 33801 |
. . . . . . . . . . 11
    
      |
152 | 135, 144,
151 | syl2anc 673 |
. . . . . . . . . 10
      
    
                                          
           |
153 | | simpl2l 1083 |
. . . . . . . . . . . 12
     
    
                      
  |
154 | 153 | adantr 472 |
. . . . . . . . . . 11
      
    
                                          
    
  |
155 | | simpl1r 1082 |
. . . . . . . . . . . . 13
     
    
                      
  |
156 | 155 | adantr 472 |
. . . . . . . . . . . 12
      
    
                                          
    
  |
157 | 156, 24 | syl 17 |
. . . . . . . . . . 11
      
    
                                          
    
  |
158 | 150, 154,
157, 26 | syl3anc 1292 |
. . . . . . . . . 10
      
    
                                          
         |
159 | | simprlr 781 |
. . . . . . . . . . 11
       
                   |
160 | 159 | ad2antrl 742 |
. . . . . . . . . 10
      
    
                                          
             |
161 | 1, 2, 4 | latmle1 16400 |
. . . . . . . . . . 11
 
     |
162 | 150, 154,
157, 161 | syl3anc 1292 |
. . . . . . . . . 10
      
    
                                          
         |
163 | 1, 2, 150, 152, 158, 154, 160, 162 | lattrd 16382 |
. . . . . . . . 9
      
    
                                          
           |
164 | 147, 137,
163 | jca31 543 |
. . . . . . . 8
      
    
                                          
               |
165 | | simprll 780 |
. . . . . . . . . . . 12
     
    
                      
      |
166 | 165 | adantr 472 |
. . . . . . . . . . 11
      
    
                               
      |
167 | | simprlr 781 |
. . . . . . . . . . . . 13
     
    
                         |
168 | 167 | adantr 472 |
. . . . . . . . . . . 12
      
    
                                  |
169 | 168 | fveq1d 5881 |
. . . . . . . . . . 11
      
    
                                          |
170 | 166, 169 | eqtr4d 2508 |
. . . . . . . . . 10
      
    
                               
      |
171 | | simprlr 781 |
. . . . . . . . . 10
      
    
                                  |
172 | 170, 171 | jca 541 |
. . . . . . . . 9
      
    
                                        |
173 | | simprrl 782 |
. . . . . . . . . . . 12
     
    
                                |
174 | 173 | adantr 472 |
. . . . . . . . . . 11
      
    
                                         |
175 | | simpll1 1069 |
. . . . . . . . . . . 12
      
    
                                    |
176 | | simprll 780 |
. . . . . . . . . . . 12
      
    
                               
  |
177 | 168, 171 | eqeltrrd 2550 |
. . . . . . . . . . . . . 14
      
    
                               
  |
178 | 175, 52 | syl 17 |
. . . . . . . . . . . . . . 15
      
    
                                    |
179 | 139 | adantr 472 |
. . . . . . . . . . . . . . 15
      
    
                                    |
180 | 175, 178,
179, 55 | syl3anc 1292 |
. . . . . . . . . . . . . 14
      
    
                               
  |
181 | 175, 177,
180, 101 | syl3anc 1292 |
. . . . . . . . . . . . 13
      
    
                                      |
182 | 175, 181,
119 | syl2anc 673 |
. . . . . . . . . . . 12
      
    
                                       |
183 | 6, 36 | ltrnco 34357 |
. . . . . . . . . . . 12
         
         |
184 | 175, 176,
182, 183 | syl3anc 1292 |
. . . . . . . . . . 11
      
    
                                         |
185 | 174, 184 | eqeltrd 2549 |
. . . . . . . . . 10
      
    
                                  |
186 | | simprr 774 |
. . . . . . . . . . 11
      
    
                                      |
187 | 2, 6, 36, 43 | trlle 33821 |
. . . . . . . . . . . 12
    
      |
188 | 175, 185,
187 | syl2anc 673 |
. . . . . . . . . . 11
      
    
                                      |
189 | 148 | adantr 472 |
. . . . . . . . . . . . 13
      |