Step | Hyp | Ref
| Expression |
1 | | simpll 527 |
. . . . . . . . . . . . 13
           |
2 | | simprl 529 |
. . . . . . . . . . . . . 14
           |
3 | | simplr 528 |
. . . . . . . . . . . . . . 15
        
  |
4 | | simprrl 539 |
. . . . . . . . . . . . . . 15
           |
5 | 3, 4 | sseldd 3168 |
. . . . . . . . . . . . . 14
           |
6 | | lsspropd.s1 |
. . . . . . . . . . . . . . . 16
 

            |
7 | 6 | ralrimivva 2569 |
. . . . . . . . . . . . . . 15
  
          |
8 | 7 | ad2antrr 488 |
. . . . . . . . . . . . . 14
         

          |
9 | | ovrspc2v 5914 |
. . . . . . . . . . . . . 14
  



                   |
10 | 2, 5, 8, 9 | syl21anc 1247 |
. . . . . . . . . . . . 13
                   |
11 | | lsspropd.w |
. . . . . . . . . . . . . . 15

  |
12 | 11 | ad2antrr 488 |
. . . . . . . . . . . . . 14
           |
13 | | simprrr 540 |
. . . . . . . . . . . . . . 15
           |
14 | 3, 13 | sseldd 3168 |
. . . . . . . . . . . . . 14
           |
15 | 12, 14 | sseldd 3168 |
. . . . . . . . . . . . 13
           |
16 | | lsspropd.p |
. . . . . . . . . . . . . 14
 

                  |
17 | 16 | oveqrspc2v 5915 |
. . . . . . . . . . . . 13
 
                                           |
18 | 1, 10, 15, 17 | syl12anc 1246 |
. . . . . . . . . . . 12
                                         |
19 | | lsspropd.s2 |
. . . . . . . . . . . . . . 15
 

                    |
20 | 19 | oveqrspc2v 5915 |
. . . . . . . . . . . . . 14
 

                    |
21 | 1, 2, 5, 20 | syl12anc 1246 |
. . . . . . . . . . . . 13
                           |
22 | 21 | oveq1d 5903 |
. . . . . . . . . . . 12
                                         |
23 | 18, 22 | eqtrd 2220 |
. . . . . . . . . . 11
                                         |
24 | 23 | eleq1d 2256 |
. . . . . . . . . 10
                                           |
25 | 24 | anassrs 400 |
. . . . . . . . 9
    
                   
                  |
26 | 25 | 2ralbidva 2509 |
. . . . . . . 8
      

              


                  |
27 | 26 | ralbidva 2483 |
. . . . . . 7
 
  


              



                  |
28 | 27 | anbi2d 464 |
. . . . . 6
 
    


               
 
 

                   |
29 | 28 | pm5.32da 452 |
. . . . 5
      

                
                          |
30 | | 3anass 983 |
. . . . 5
 
                        

                   |
31 | | 3anass 983 |
. . . . 5
 
                        

                   |
32 | 29, 30, 31 | 3bitr4g 223 |
. . . 4
    


               
   

                   |
33 | | lsspropd.b1 |
. . . . . 6
       |
34 | 33 | sseq2d 3197 |
. . . . 5
         |
35 | | lsspropd.p1 |
. . . . . 6
    Scalar     |
36 | 35 | raleqdv 2689 |
. . . . 5
                    
   Scalar    

                  |
37 | 34, 36 | 3anbi13d 1324 |
. . . 4
    


               
    
     Scalar                         |
38 | | lsspropd.b2 |
. . . . . 6
       |
39 | 38 | sseq2d 3197 |
. . . . 5
         |
40 | | lsspropd.p2 |
. . . . . 6
    Scalar     |
41 | 40 | raleqdv 2689 |
. . . . 5
                    
   Scalar    

                  |
42 | 39, 41 | 3anbi13d 1324 |
. . . 4
    


               
    
     Scalar                         |
43 | 32, 37, 42 | 3bitr3d 218 |
. . 3
            Scalar    

               
    
     Scalar                         |
44 | | lsppropd.v1 |
. . . 4
   |
45 | | eqid 2187 |
. . . . 5
Scalar  Scalar   |
46 | | eqid 2187 |
. . . . 5
   Scalar      Scalar    |
47 | | eqid 2187 |
. . . . 5
         |
48 | | eqid 2187 |
. . . . 5
       |
49 | | eqid 2187 |
. . . . 5
         |
50 | | eqid 2187 |
. . . . 5
         |
51 | 45, 46, 47, 48, 49, 50 | islssmg 13511 |
. . . 4
     
    
     Scalar                         |
52 | 44, 51 | syl 14 |
. . 3
     
    
     Scalar                         |
53 | | lsppropd.v2 |
. . . 4
   |
54 | | eqid 2187 |
. . . . 5
Scalar  Scalar   |
55 | | eqid 2187 |
. . . . 5
   Scalar      Scalar    |
56 | | eqid 2187 |
. . . . 5
         |
57 | | eqid 2187 |
. . . . 5
       |
58 | | eqid 2187 |
. . . . 5
         |
59 | | eqid 2187 |
. . . . 5
         |
60 | 54, 55, 56, 57, 58, 59 | islssmg 13511 |
. . . 4
     
    
     Scalar                         |
61 | 53, 60 | syl 14 |
. . 3
     
    
     Scalar                         |
62 | 43, 52, 61 | 3bitr4d 220 |
. 2
     
       |
63 | 62 | eqrdv 2185 |
1
           |