Proof of Theorem dalem24
Step | Hyp | Ref
| Expression |
1 | | dalem23.g |
. . . . 5
  
    |
2 | 1 | oveq1i 6285 |
. . . 4
           |
3 | | dalem.ph |
. . . . . . . 8
         
 
  
    
 
   
 
 
               |
4 | 3 | dalemkehl 33189 |
. . . . . . 7
   |
5 | | hlol 32928 |
. . . . . . 7
   |
6 | 4, 5 | syl 17 |
. . . . . 6
   |
7 | 6 | 3ad2ant1 1030 |
. . . . 5
 

  |
8 | 4 | 3ad2ant1 1030 |
. . . . . 6
 

  |
9 | | dalem.ps |
. . . . . . . 8
  

       |
10 | 9 | dalemccea 33249 |
. . . . . . 7

  |
11 | 10 | 3ad2ant3 1032 |
. . . . . 6
 
   |
12 | 3 | dalempea 33192 |
. . . . . . 7
   |
13 | 12 | 3ad2ant1 1030 |
. . . . . 6
 

  |
14 | | eqid 2451 |
. . . . . . 7
         |
15 | | dalem.j |
. . . . . . 7
     |
16 | | dalem.a |
. . . . . . 7
     |
17 | 14, 15, 16 | hlatjcl 32933 |
. . . . . 6
 
         |
18 | 8, 11, 13, 17 | syl3anc 1271 |
. . . . 5
 
         |
19 | 9 | dalemddea 33250 |
. . . . . . 7

  |
20 | 19 | 3ad2ant3 1032 |
. . . . . 6
 
   |
21 | 3 | dalemsea 33195 |
. . . . . . 7
   |
22 | 21 | 3ad2ant1 1030 |
. . . . . 6
 

  |
23 | 14, 15, 16 | hlatjcl 32933 |
. . . . . 6
 
         |
24 | 8, 20, 22, 23 | syl3anc 1271 |
. . . . 5
 
         |
25 | | dalem23.o |
. . . . . . 7
     |
26 | 3, 25 | dalemyeb 33215 |
. . . . . 6
       |
27 | 26 | 3ad2ant1 1030 |
. . . . 5
 

      |
28 | | dalem23.m |
. . . . . 6
     |
29 | 14, 28 | latmmdir 32802 |
. . . . 5
         
    
         
       
   
    |
30 | 7, 18, 24, 27, 29 | syl13anc 1273 |
. . . 4
 
            
   
    |
31 | 2, 30 | syl5eq 2497 |
. . 3
 
      
   
    |
32 | 15, 16 | hlatjcom 32934 |
. . . . . . 7
 
       |
33 | 8, 11, 13, 32 | syl3anc 1271 |
. . . . . 6
 
       |
34 | 33 | oveq1d 6290 |
. . . . 5
 
   
       |
35 | | dalem.l |
. . . . . . . 8
     |
36 | | dalem23.y |
. . . . . . . 8
     |
37 | 3, 35, 15, 16, 25, 36 | dalemply 33220 |
. . . . . . 7

  |
38 | 37 | 3ad2ant1 1030 |
. . . . . 6
 
   |
39 | 9 | dalem-ccly 33251 |
. . . . . . 7
   |
40 | 39 | 3ad2ant3 1032 |
. . . . . 6
 

  |
41 | 14, 35, 15, 28, 16 | 2atjm 33011 |
. . . . . 6
  
              |
42 | 8, 13, 11, 27, 38, 40, 41 | syl132anc 1289 |
. . . . 5
 
       |
43 | 34, 42 | eqtrd 2485 |
. . . 4
 
   
   |
44 | 15, 16 | hlatjcom 32934 |
. . . . . . 7
 
       |
45 | 8, 20, 22, 44 | syl3anc 1271 |
. . . . . 6
 
       |
46 | 45 | oveq1d 6290 |
. . . . 5
 
   
       |
47 | | dalem23.z |
. . . . . . . 8
     |
48 | 3, 35, 15, 16, 47 | dalemsly 33221 |
. . . . . . 7
 
   |
49 | 48 | 3adant3 1029 |
. . . . . 6
 
   |
50 | 9 | dalem-ddly 33252 |
. . . . . . 7
   |
51 | 50 | 3ad2ant3 1032 |
. . . . . 6
 

  |
52 | 14, 35, 15, 28, 16 | 2atjm 33011 |
. . . . . 6
  
              |
53 | 8, 22, 20, 27, 49, 51, 52 | syl132anc 1289 |
. . . . 5
 
       |
54 | 46, 53 | eqtrd 2485 |
. . . 4
 
   
   |
55 | 43, 54 | oveq12d 6293 |
. . 3
 
     
 
       |
56 | 3, 35, 15, 16, 25, 36 | dalempnes 33217 |
. . . . 5
   |
57 | | hlatl 32927 |
. . . . . . 7
   |
58 | 4, 57 | syl 17 |
. . . . . 6
   |
59 | | eqid 2451 |
. . . . . . 7
         |
60 | 28, 59, 16 | atnem0 32885 |
. . . . . 6
 
 
         |
61 | 58, 12, 21, 60 | syl3anc 1271 |
. . . . 5
  
        |
62 | 56, 61 | mpbid 215 |
. . . 4
         |
63 | 62 | 3ad2ant1 1030 |
. . 3
 
         |
64 | 31, 55, 63 | 3eqtrd 2489 |
. 2
 
         |
65 | 58 | 3ad2ant1 1030 |
. . 3
 

  |
66 | 3, 35, 15, 16, 9, 28, 25, 36, 47, 1 | dalem23 33262 |
. . 3
 

  |
67 | 14, 35, 28, 59, 16 | atnle 32884 |
. . 3
 
     
         |
68 | 65, 66, 27, 67 | syl3anc 1271 |
. 2
 
           |
69 | 64, 68 | mpbird 240 |
1
 

  |