Proof of Theorem cdlemk5u
Step | Hyp | Ref
| Expression |
1 | | cdlemk1.b |
. 2
     |
2 | | cdlemk1.l |
. 2
     |
3 | | simp11l 1125 |
. . 3
    
  


                                
          
  |
4 | | hllat 32974 |
. . 3
   |
5 | 3, 4 | syl 17 |
. 2
    
  


                                
          
  |
6 | | simp22l 1133 |
. . . 4
    
  


                                
          
  |
7 | | simp1 1014 |
. . . . 5
    
  


                                
             
   |
8 | | simp211 1152 |
. . . . . 6
    
  


                                
          
  |
9 | | simp22 1048 |
. . . . . 6
    
  


                                
               |
10 | | simp23 1049 |
. . . . . 6
    
  


                                
                     |
11 | 8, 9, 10 | 3jca 1194 |
. . . . 5
    
  


                                
                         |
12 | | simp3l1 1119 |
. . . . . 6
    
  


                                
              |
13 | | simp3l2 1120 |
. . . . . 6
    
  


                                
              |
14 | | simp3r1 1122 |
. . . . . 6
    
  


                                
                     |
15 | 12, 13, 14 | 3jca 1194 |
. . . . 5
    
  


                                
                         |
16 | | cdlemk1.j |
. . . . . . 7
     |
17 | | cdlemk1.m |
. . . . . . 7
     |
18 | | cdlemk1.a |
. . . . . . 7
     |
19 | | cdlemk1.h |
. . . . . . 7
     |
20 | | cdlemk1.t |
. . . . . . 7
         |
21 | | cdlemk1.r |
. . . . . . 7
         |
22 | | cdlemk1.s |
. . . . . . 7
                               |
23 | | cdlemk1.o |
. . . . . . 7
     |
24 | 1, 2, 16, 17, 18, 19, 20, 21, 22, 23 | cdlemkoatnle 34463 |
. . . . . 6
    
 

                                   |
25 | 24 | simpld 465 |
. . . . 5
    
 

                             |
26 | 7, 11, 15, 25 | syl3anc 1276 |
. . . 4
    
  


                                
                 |
27 | 1, 16, 18 | hlatjcl 32977 |
. . . 4
 
             |
28 | 3, 6, 26, 27 | syl3anc 1276 |
. . 3
    
  


                                
                   |
29 | | simp11 1044 |
. . . . 5
    
  


                                
               |
30 | | simp212 1153 |
. . . . 5
    
  


                                
          
  |
31 | 2, 18, 19, 20 | ltrnat 33750 |
. . . . 5
   

      |
32 | 29, 30, 6, 31 | syl3anc 1276 |
. . . 4
    
  


                                
                 |
33 | | simp13 1046 |
. . . . 5
    
  


                                
          
  |
34 | | simp3r2 1123 |
. . . . 5
    
  


                                
                     |
35 | 18, 19, 20, 21 | trlcocnvat 34336 |
. . . . 5
                        |
36 | 29, 30, 33, 34, 35 | syl121anc 1281 |
. . . 4
    
  


                                
              
     |
37 | 1, 16, 18 | hlatjcl 32977 |
. . . 4
                  
          |
38 | 3, 32, 36, 37 | syl3anc 1276 |
. . 3
    
  


                                
                          |
39 | 1, 17 | latmcl 16347 |
. . 3
  
         
               
        
       |
40 | 5, 28, 38, 39 | syl3anc 1276 |
. 2
    
  


                                
                 
        
       |
41 | 2, 18, 19, 20 | ltrnat 33750 |
. . . . 5
   

      |
42 | 29, 33, 6, 41 | syl3anc 1276 |
. . . 4
    
  


                                
                 |
43 | 1, 18, 19, 20, 21 | trlnidat 33784 |
. . . . 5
   
        |
44 | 29, 33, 13, 43 | syl3anc 1276 |
. . . 4
    
  


                                
                 |
45 | 1, 16, 18 | hlatjcl 32977 |
. . . 4
               
       |
46 | 3, 42, 44, 45 | syl3anc 1276 |
. . 3
    
  


                                
                       |
47 | 1, 16, 18 | hlatjcl 32977 |
. . . 4
                  
          |
48 | 3, 42, 36, 47 | syl3anc 1276 |
. . 3
    
  


                                
                          |
49 | 1, 17 | latmcl 16347 |
. . 3
                                    
        
       |
50 | 5, 46, 48, 49 | syl3anc 1276 |
. 2
    
  


                                
                     
        
       |
51 | | simp213 1154 |
. . . 4
    
  


                                
          
  |
52 | 2, 18, 19, 20 | ltrnat 33750 |
. . . 4
   

      |
53 | 29, 51, 6, 52 | syl3anc 1276 |
. . 3
    
  


                                
                 |
54 | | simp3r3 1124 |
. . . 4
    
  


                                
                     |
55 | 18, 19, 20, 21 | trlcocnvat 34336 |
. . . 4
                        |
56 | 29, 51, 33, 54, 55 | syl121anc 1281 |
. . 3
    
  


                                
              
     |
57 | 1, 16, 18 | hlatjcl 32977 |
. . 3
                  
          |
58 | 3, 53, 56, 57 | syl3anc 1276 |
. 2
    
  


                                
                          |
59 | 1, 2, 16, 17, 18, 19, 20, 21, 22, 23 | cdlemk1u 34471 |
. . . . 5
    
 

                            
            |
60 | 7, 11, 15, 59 | syl3anc 1276 |
. . . 4
    
  


                                
                             |
61 | 1, 2, 17 | latmlem1 16376 |
. . . . 5
                                                  
                    
     
                      |
62 | 5, 28, 46, 38, 61 | syl13anc 1278 |
. . . 4
    
  


                                
                 
                
        
               
        
        |
63 | 60, 62 | mpd 15 |
. . 3
    
  


                                
                 
        
               
        
       |
64 | | simp11r 1126 |
. . . . 5
    
  


                                
          
  |
65 | 1, 2, 16, 18, 19, 20, 21 | cdlemk2 34444 |
. . . . 5
      
 
        
                   |
66 | 3, 64, 33, 30, 9, 65 | syl221anc 1287 |
. . . 4
    
  


                                
                                       |
67 | 66 | oveq2d 6331 |
. . 3
    
  


                                
                     
        
                                |
68 | 63, 67 | breqtrd 4441 |
. 2
    
  


                                
                 
        
               
        
       |
69 | | simp3l3 1121 |
. . . 4
    
  


                                
              |
70 | 13, 69 | jca 539 |
. . 3
    
  


                                
                 |
71 | 1, 2, 16, 18, 19, 20, 21, 17 | cdlemk5a 34447 |
. . 3
               
      
     
                  
        
      |
72 | 3, 64, 33, 30, 51, 34, 70, 9, 71 | syl233anc 1305 |
. 2
    
  


                                
                     
        
                    |
73 | 1, 2, 5, 40, 50, 58, 68, 72 | lattrd 16353 |
1
    
  


                                
                 
        
                    |