Proof of Theorem 2lplnja
Step | Hyp | Ref
| Expression |
1 | | eqid 2454 |
. 2
         |
2 | | 2lplnja.l |
. 2
     |
3 | | simp11l 1099 |
. . 3
     
       
         
              
  |
4 | | hllat 33371 |
. . 3
   |
5 | 3, 4 | syl 16 |
. 2
     
       
         
              
  |
6 | | simp121 1120 |
. . . . 5
     
       
         
              
  |
7 | | simp122 1121 |
. . . . 5
     
       
         
              
  |
8 | | 2lplnja.j |
. . . . . 6
     |
9 | | 2lplnja.a |
. . . . . 6
     |
10 | 1, 8, 9 | hlatjcl 33374 |
. . . . 5
 
         |
11 | 3, 6, 7, 10 | syl3anc 1219 |
. . . 4
     
       
         
              
        |
12 | | simp123 1122 |
. . . . 5
     
       
         
              
  |
13 | 1, 9 | atbase 33297 |
. . . . 5
       |
14 | 12, 13 | syl 16 |
. . . 4
     
       
         
              
      |
15 | 1, 8 | latjcl 15344 |
. . . 4
  
    
    
          |
16 | 5, 11, 14, 15 | syl3anc 1219 |
. . 3
     
       
         
              
          |
17 | | simp2l1 1087 |
. . . . 5
     
       
         
              
  |
18 | | simp2l2 1088 |
. . . . 5
     
       
         
              
  |
19 | 1, 8, 9 | hlatjcl 33374 |
. . . . 5
 
         |
20 | 3, 17, 18, 19 | syl3anc 1219 |
. . . 4
     
       
         
              
        |
21 | | simp2l3 1089 |
. . . . 5
     
       
         
              
  |
22 | 1, 9 | atbase 33297 |
. . . . 5
       |
23 | 21, 22 | syl 16 |
. . . 4
     
       
         
              
      |
24 | 1, 8 | latjcl 15344 |
. . . 4
  
    
    
          |
25 | 5, 20, 23, 24 | syl3anc 1219 |
. . 3
     
       
         
              
          |
26 | 1, 8 | latjcl 15344 |
. . 3
         
                         |
27 | 5, 16, 25, 26 | syl3anc 1219 |
. 2
     
       
         
              
   
            |
28 | | simp11r 1100 |
. . 3
     
       
         
              
  |
29 | | 2lplnja.v |
. . . 4
     |
30 | 1, 29 | lvolbase 33585 |
. . 3
       |
31 | 28, 30 | syl 16 |
. 2
     
       
         
              
      |
32 | | simp31 1024 |
. . 3
     
       
         
              
   
  |
33 | | simp32 1025 |
. . 3
     
       
         
              
   
  |
34 | 1, 2, 8 | latjle12 15355 |
. . . 4
             
    
           
    
   
     
   |
35 | 5, 16, 25, 31, 34 | syl13anc 1221 |
. . 3
     
       
         
              
          
   
     
   |
36 | 32, 33, 35 | mpbi2and 912 |
. 2
     
       
         
              
   
     
  |
37 | 1, 2, 8 | latlej2 15354 |
. . . . . . . . . 10
  
    
    
  
   |
38 | 5, 20, 23, 37 | syl3anc 1219 |
. . . . . . . . 9
     
       
         
              
  
   |
39 | 1, 2, 5, 23, 25, 31, 38, 33 | lattrd 15351 |
. . . . . . . 8
     
       
         
              
  |
40 | 1, 2, 8 | latjle12 15355 |
. . . . . . . . 9
              
           

   
     |
41 | 5, 16, 23, 31, 40 | syl13anc 1221 |
. . . . . . . 8
     
       
         
              
            
   |
42 | 32, 39, 41 | mpbi2and 912 |
. . . . . . 7
     
       
         
              
   
    |
43 | 42 | ad2antrr 725 |
. . . . . 6
     
 

                 
                     
 
   
    |
44 | 3 | ad2antrr 725 |
. . . . . . 7
     
 

                 
                     
 
  |
45 | 3, 6, 7 | 3jca 1168 |
. . . . . . . . 9
     
       
         
              
    |
46 | 45 | ad2antrr 725 |
. . . . . . . 8
     
 

                 
                     
 
    |
47 | 12, 21 | jca 532 |
. . . . . . . . 9
     
       
         
              

   |
48 | 47 | ad2antrr 725 |
. . . . . . . 8
     
 

                 
                     
 

   |
49 | | simp13l 1103 |
. . . . . . . . 9
     
       
         
              
  |
50 | 49 | ad2antrr 725 |
. . . . . . . 8
     
 

                 
                     
 
  |
51 | | simp13r 1104 |
. . . . . . . . 9
     
       
         
              
    |
52 | 51 | ad2antrr 725 |
. . . . . . . 8
     
 

                 
                     
 
    |
53 | | simp33 1026 |
. . . . . . . . . 10
     
       
         
              
          |
54 | 53 | ad2antrr 725 |
. . . . . . . . 9
     
 

                 
                     
 
          |
55 | | simplr 754 |
. . . . . . . . . . . . . . . 16
     
 

                 
                     
 
  
   |
56 | | simpr 461 |
. . . . . . . . . . . . . . . 16
     
 

                 
                     
 
  
   |
57 | 1, 9 | atbase 33297 |
. . . . . . . . . . . . . . . . . . 19
       |
58 | 17, 57 | syl 16 |
. . . . . . . . . . . . . . . . . 18
     
       
         
              
      |
59 | 1, 9 | atbase 33297 |
. . . . . . . . . . . . . . . . . . 19
       |
60 | 18, 59 | syl 16 |
. . . . . . . . . . . . . . . . . 18
     
       
         
              
      |
61 | 1, 2, 8 | latjle12 15355 |
. . . . . . . . . . . . . . . . . 18
  
   
      
           

              |
62 | 5, 58, 60, 16, 61 | syl13anc 1221 |
. . . . . . . . . . . . . . . . 17
     
       
         
              
        
   
       |
63 | 62 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
     
 

                 
                     
 
        
   
       |
64 | 55, 56, 63 | mpbi2and 912 |
. . . . . . . . . . . . . . 15
     
 

                 
                     
 
        |
65 | 64 | adantr 465 |
. . . . . . . . . . . . . 14
                           
                     
 
  
 
        |
66 | | simpr 461 |
. . . . . . . . . . . . . 14
                           
                     
 
  
 
  
   |
67 | 1, 2, 8 | latjle12 15355 |
. . . . . . . . . . . . . . . 16
            
                                  |
68 | 5, 20, 23, 16, 67 | syl13anc 1221 |
. . . . . . . . . . . . . . 15
     
       
         
              
          
     
       |
69 | 68 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
                           
                     
 
  
 
          
     
       |
70 | 65, 66, 69 | mpbi2and 912 |
. . . . . . . . . . . . 13
                           
                     
 
  
 
   
      |
71 | | simp2l 1014 |
. . . . . . . . . . . . . . 15
     
       
         
              

   |
72 | | simp12 1019 |
. . . . . . . . . . . . . . 15
     
       
         
              

   |
73 | | simp2rr 1058 |
. . . . . . . . . . . . . . 15
     
       
         
              
    |
74 | | simp2rl 1057 |
. . . . . . . . . . . . . . 15
     
       
         
              
  |
75 | 2, 8, 9 | 3at 33497 |
. . . . . . . . . . . . . . 15
   


  
                        |
76 | 3, 71, 72, 73, 74, 75 | syl32anc 1227 |
. . . . . . . . . . . . . 14
     
       
         
              
   
                |
77 | 76 | ad3antrrr 729 |
. . . . . . . . . . . . 13
                           
                     
 
  
 
   
                |
78 | 70, 77 | mpbid 210 |
. . . . . . . . . . . 12
                           
                     
 
  
 
          |
79 | 78 | eqcomd 2462 |
. . . . . . . . . . 11
                           
                     
 
  
 
          |
80 | 79 | ex 434 |
. . . . . . . . . 10
     
 

                 
                     
 
                |
81 | 80 | necon3ad 2662 |
. . . . . . . . 9
     
 

                 
                     
 
   
    
  
    |
82 | 54, 81 | mpd 15 |
. . . . . . . 8
     
 

                 
                     
 
      |
83 | 2, 8, 9, 29 | lvoli2 33588 |
. . . . . . . 8
  
 

  
              |
84 | 46, 48, 50, 52, 82, 83 | syl113anc 1231 |
. . . . . . 7
     
 

                 
                     
 
   
    |
85 | 28 | ad2antrr 725 |
. . . . . . 7
     
 

                 
                     
 
  |
86 | 2, 29 | lvolcmp 33624 |
. . . . . . 7
                         |
87 | 44, 84, 85, 86 | syl3anc 1219 |
. . . . . 6
     
 

                 
                     
 
                |
88 | 43, 87 | mpbid 210 |
. . . . 5
     
 

                 
                     
 
   
    |
89 | 1, 2, 8 | latjlej2 15359 |
. . . . . . . 8
  
           
             
                    |
90 | 5, 23, 25, 16, 89 | syl13anc 1221 |
. . . . . . 7
     
       
         
              
          
   
         |
91 | 38, 90 | mpd 15 |
. . . . . 6
     
       
         
              
   
     
        |
92 | 91 | ad2antrr 725 |
. . . . 5
     
 

                 
                     
 
   
     
        |
93 | 88, 92 | eqbrtrrd 4425 |
. . . 4
     
 

                 
                     
 
            |
94 | 1, 8, 9 | hlatjcl 33374 |
. . . . . . . . . . . 12
 
         |
95 | 3, 17, 21, 94 | syl3anc 1219 |
. . . . . . . . . . 11
     
       
         
              
        |
96 | 1, 2, 8 | latlej2 15354 |
. . . . . . . . . . 11
  
    
    
  
   |
97 | 5, 95, 60, 96 | syl3anc 1219 |
. . . . . . . . . 10
     
       
         
              
  
   |
98 | 8, 9 | hlatj32 33379 |
. . . . . . . . . . 11
  
    
       |
99 | 3, 17, 18, 21, 98 | syl13anc 1221 |
. . . . . . . . . 10
     
       
         
              
          |
100 | 97, 99 | breqtrrd 4429 |
. . . . . . . . 9
     
       
         
              
  
   |
101 | 1, 2, 5, 60, 25, 31, 100, 33 | lattrd 15351 |
. . . . . . . 8
     
       
         
              
  |
102 | 1, 2, 8 | latjle12 15355 |
. . . . . . . . 9
              
           

   
     |
103 | 5, 16, 60, 31, 102 | syl13anc 1221 |
. . . . . . . 8
     
       
         
              
            
   |
104 | 32, 101, 103 | mpbi2and 912 |
. . . . . . 7
     
       
         
              
   
    |
105 | 104 | ad2antrr 725 |
. . . . . 6
     
 

                 
                       
   
    |
106 | 3 | ad2antrr 725 |
. . . . . . 7
     
 

                 
                       
  |
107 | 45 | ad2antrr 725 |
. . . . . . . 8
     
 

                 
                       
    |
108 | 12, 18 | jca 532 |
. . . . . . . . 9
     
       
         
              

   |
109 | 108 | ad2antrr 725 |
. . . . . . . 8
     
 

                 
                       

   |
110 | 49 | ad2antrr 725 |
. . . . . . . 8
     
 

                 
                       
  |
111 | 51 | ad2antrr 725 |
. . . . . . . 8
     
 

                 
                       
    |
112 | | simpr 461 |
. . . . . . . 8
     
 

                 
                       
      |
113 | 2, 8, 9, 29 | lvoli2 33588 |
. . . . . . . 8
  
 

  
              |
114 | 107, 109,
110, 111, 112, 113 | syl113anc 1231 |
. . . . . . 7
     
 

                 
                       
   
    |
115 | 28 | ad2antrr 725 |
. . . . . . 7
     
 

                 
                       
  |
116 | 2, 29 | lvolcmp 33624 |
. . . . . . 7
                         |
117 | 106, 114,
115, 116 | syl3anc 1219 |
. . . . . 6
     
 

                 
                       
                |
118 | 105, 117 | mpbid 210 |
. . . . 5
     
 

                 
                       
   
    |
119 | 1, 2, 8 | latjlej2 15359 |
. . . . . . . 8
  
           
             
                    |
120 | 5, 60, 25, 16, 119 | syl13anc 1221 |
. . . . . . 7
     
       
         
              
          
   
         |
121 | 100, 120 | mpd 15 |
. . . . . 6
     
       
         
              
   
     
        |
122 | 121 | ad2antrr 725 |
. . . . 5
     
 

                 
                       
   
     
        |
123 | 118, 122 | eqbrtrrd 4425 |
. . . 4
     
 

                 
                       
            |
124 | 93, 123 | pm2.61dan 789 |
. . 3
      
       
         
                 
 
            |
125 | 1, 8, 9 | hlatjcl 33374 |
. . . . . . . . . . 11
 
         |
126 | 3, 18, 21, 125 | syl3anc 1219 |
. . . . . . . . . 10
     
       
         
              
        |
127 | 1, 2, 8 | latlej1 15353 |
. . . . . . . . . 10
 
                 |
128 | 5, 58, 126, 127 | syl3anc 1219 |
. . . . . . . . 9
     
       
         
              
      |
129 | 1, 8 | latjass 15388 |
. . . . . . . . . 10
  
   
               
    |
130 | 5, 58, 60, 23, 129 | syl13anc 1221 |
. . . . . . . . 9
     
       
         
              
          |
131 | 128, 130 | breqtrrd 4429 |
. . . . . . . 8
     
       
         
              
  
   |
132 | 1, 2, 5, 58, 25, 31, 131, 33 | lattrd 15351 |
. . . . . . 7
     
       
         
              
  |
133 | 1, 2, 8 | latjle12 15355 |
. . . . . . . 8
              
           

   
     |
134 | 5, 16, 58, 31, 133 | syl13anc 1221 |
. . . . . . 7
     
       
         
              
            
   |
135 | 32, 132, 134 | mpbi2and 912 |
. . . . . 6
     
       
         
              
   
    |
136 | 135 | adantr 465 |
. . . . 5
      
       
         
      |