Step | Hyp | Ref
| Expression |
1 | | eqidd 2452 |
. . 3
 Scalar  Scalar    |
2 | | eqidd 2452 |
. . 3
    Scalar      Scalar     |
3 | | lbsext.v |
. . . 4
     |
4 | 3 | a1i 11 |
. . 3
       |
5 | | eqidd 2452 |
. . 3
         |
6 | | eqidd 2452 |
. . 3
           |
7 | | lbsext.p |
. . . 4
     |
8 | 7 | a1i 11 |
. . 3
       |
9 | | lbsext.t |
. . . 4
          |
10 | | lbsext.w |
. . . . . . . . 9
   |
11 | | lveclmod 18329 |
. . . . . . . . 9

  |
12 | 10, 11 | syl 17 |
. . . . . . . 8
   |
13 | 12 | adantr 467 |
. . . . . . 7
 
   |
14 | | lbsext.a |
. . . . . . . . . . 11

  |
15 | | lbsext.s |
. . . . . . . . . . . 12
 
 
   
       |
16 | | ssrab2 3514 |
. . . . . . . . . . . 12
                |
17 | 15, 16 | eqsstri 3462 |
. . . . . . . . . . 11
  |
18 | 14, 17 | syl6ss 3444 |
. . . . . . . . . 10

   |
19 | 18 | sselda 3432 |
. . . . . . . . 9
 
    |
20 | 19 | elpwid 3961 |
. . . . . . . 8
 
   |
21 | 20 | ssdifssd 3571 |
. . . . . . 7
 
 
     |
22 | | lbsext.n |
. . . . . . . 8
     |
23 | 3, 22 | lspssv 18206 |
. . . . . . 7
  
   
          |
24 | 13, 21, 23 | syl2anc 667 |
. . . . . 6
 
        
  |
25 | 24 | ralrimiva 2802 |
. . . . 5
            |
26 | | iunss 4319 |
. . . . 5
 
       

          |
27 | 25, 26 | sylibr 216 |
. . . 4
            |
28 | 9, 27 | syl5eqss 3476 |
. . 3

  |
29 | 9 | a1i 11 |
. . . 4
 
          |
30 | | lbsext.z |
. . . . . 6
   |
31 | 3, 7, 22 | lspcl 18199 |
. . . . . . . . 9
  
   
          |
32 | 13, 21, 31 | syl2anc 667 |
. . . . . . . 8
 
           |
33 | 7 | lssn0 18164 |
. . . . . . . 8
            
      |
34 | 32, 33 | syl 17 |
. . . . . . 7
 
           |
35 | 34 | ralrimiva 2802 |
. . . . . 6
            |
36 | | r19.2z 3858 |
. . . . . 6
  
         
          |
37 | 30, 35, 36 | syl2anc 667 |
. . . . 5
            |
38 | | iunn0 4338 |
. . . . 5
         
    
      |
39 | 37, 38 | sylib 200 |
. . . 4
            |
40 | 29, 39 | eqnetrd 2691 |
. . 3
   |
41 | 9 | eleq2i 2521 |
. . . . . . . . 9

           |
42 | | eliun 4283 |
. . . . . . . . 9
     
   

          |
43 | | difeq1 3544 |
. . . . . . . . . . . 12
 
         |
44 | 43 | fveq2d 5869 |
. . . . . . . . . . 11
                   |
45 | 44 | eleq2d 2514 |
. . . . . . . . . 10
                     |
46 | 45 | cbvrexv 3020 |
. . . . . . . . 9
     
   

          |
47 | 41, 42, 46 | 3bitri 275 |
. . . . . . . 8


          |
48 | 9 | eleq2i 2521 |
. . . . . . . . 9

           |
49 | | eliun 4283 |
. . . . . . . . 9
     
   

          |
50 | | difeq1 3544 |
. . . . . . . . . . . 12
 
         |
51 | 50 | fveq2d 5869 |
. . . . . . . . . . 11
                   |
52 | 51 | eleq2d 2514 |
. . . . . . . . . 10
         
           |
53 | 52 | cbvrexv 3020 |
. . . . . . . . 9
     
   

          |
54 | 48, 49, 53 | 3bitri 275 |
. . . . . . . 8


          |
55 | 47, 54 | anbi12i 703 |
. . . . . . 7
 
  
                    |
56 | | reeanv 2958 |
. . . . . . 7
  
            
               
   
       |
57 | 55, 56 | bitr4i 256 |
. . . . . 6
 
  
            
       |
58 | | simp1l 1032 |
. . . . . . . . . . . . 13
      Scalar                  
     
  |
59 | | lbsext.r |
. . . . . . . . . . . . 13
 [ ]
  |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . 12
      Scalar                  
     
[ ]   |
61 | | simp2 1009 |
. . . . . . . . . . . 12
      Scalar                  
     

   |
62 | | sorpssun 6578 |
. . . . . . . . . . . 12
 [ ] 
 
    |
63 | 60, 61, 62 | syl2anc 667 |
. . . . . . . . . . 11
      Scalar                  
     
    |
64 | 58, 12 | syl 17 |
. . . . . . . . . . . . 13
      Scalar                  
     
  |
65 | | elssuni 4227 |
. . . . . . . . . . . . . . . 16
        |
66 | 63, 65 | syl 17 |
. . . . . . . . . . . . . . 15
      Scalar                  
     
     |
67 | | sspwuni 4367 |
. . . . . . . . . . . . . . . . 17
 
   |
68 | 18, 67 | sylib 200 |
. . . . . . . . . . . . . . . 16
    |
69 | 58, 68 | syl 17 |
. . . . . . . . . . . . . . 15
      Scalar                  
     
   |
70 | 66, 69 | sstrd 3442 |
. . . . . . . . . . . . . 14
      Scalar                  
     
    |
71 | 70 | ssdifssd 3571 |
. . . . . . . . . . . . 13
      Scalar                  
     
     
  |
72 | 3, 7, 22 | lspcl 18199 |
. . . . . . . . . . . . 13
    
   
            |
73 | 64, 71, 72 | syl2anc 667 |
. . . . . . . . . . . 12
      Scalar                  
     
            |
74 | | simp1r 1033 |
. . . . . . . . . . . 12
      Scalar                  
     
   Scalar     |
75 | | ssun1 3597 |
. . . . . . . . . . . . . . 15

  |
76 | | ssdif 3568 |
. . . . . . . . . . . . . . 15
   
     
     |
77 | 75, 76 | mp1i 13 |
. . . . . . . . . . . . . 14
      Scalar                  
     
            |
78 | 3, 22 | lspss 18207 |
. . . . . . . . . . . . . 14
    
                 
                |
79 | 64, 71, 77, 78 | syl3anc 1268 |
. . . . . . . . . . . . 13
      Scalar                  
     
                    |
80 | | simp3l 1036 |
. . . . . . . . . . . . 13
      Scalar                  
     
          |
81 | 79, 80 | sseldd 3433 |
. . . . . . . . . . . 12
      Scalar                  
     
            |
82 | | ssun2 3598 |
. . . . . . . . . . . . . . 15

  |
83 | | ssdif 3568 |
. . . . . . . . . . . . . . 15
   
     
     |
84 | 82, 83 | mp1i 13 |
. . . . . . . . . . . . . 14
      Scalar                  
     
            |
85 | 3, 22 | lspss 18207 |
. . . . . . . . . . . . . 14
    
                 
                |
86 | 64, 71, 84, 85 | syl3anc 1268 |
. . . . . . . . . . . . 13
      Scalar                  
     
                    |
87 | | simp3r 1037 |
. . . . . . . . . . . . 13
      Scalar                  
     
          |
88 | 86, 87 | sseldd 3433 |
. . . . . . . . . . . 12
      Scalar                  
     
            |
89 | | eqid 2451 |
. . . . . . . . . . . . 13
Scalar  Scalar   |
90 | | eqid 2451 |
. . . . . . . . . . . . 13
   Scalar      Scalar    |
91 | | eqid 2451 |
. . . . . . . . . . . . 13
       |
92 | | eqid 2451 |
. . . . . . . . . . . . 13
         |
93 | 89, 90, 91, 92, 7 | lsscl 18166 |
. . . . . . . . . . . 12
       
        Scalar  
                                                 |
94 | 73, 74, 81, 88, 93 | syl13anc 1270 |
. . . . . . . . . . 11
      Scalar                  
     
                    
      |
95 | | difeq1 3544 |
. . . . . . . . . . . . . 14
   
     
     |
96 | 95 | fveq2d 5869 |
. . . . . . . . . . . . 13
                       |
97 | 96 | eleq2d 2514 |
. . . . . . . . . . . 12
                      
   
                    
       |
98 | 97 | rspcev 3150 |
. . . . . . . . . . 11
                             

                  
      |
99 | 63, 94, 98 | syl2anc 667 |
. . . . . . . . . 10
      Scalar                  
     

                  
      |
100 | | eliun 4283 |
. . . . . . . . . 10
                        

                  
      |
101 | 99, 100 | sylibr 216 |
. . . . . . . . 9
      Scalar                  
     
                          |
102 | 101, 9 | syl6eleqr 2540 |
. . . . . . . 8
      Scalar                  
     
                 |
103 | 102 | 3expia 1210 |
. . . . . . 7
      Scalar            
   
        
                  |
104 | 103 | rexlimdvva 2886 |
. . . . . 6
 
   Scalar           
   
        
                  |
105 | 57, 104 | syl5bi 221 |
. . . . 5
 
   Scalar                         |
106 | 105 | exp4b 612 |
. . . 4
     Scalar                         |
107 | 106 | 3imp2 1224 |
. . 3
 
    Scalar  
 
                 |
108 | 1, 2, 4, 5, 6, 8, 28, 40, 107 | islssd 18159 |
. 2
   |
109 | | eldifi 3555 |
. . . . . . 7
         |
110 | 109 | adantl 468 |
. . . . . 6
 
         |
111 | | eldifn 3556 |
. . . . . . . . . 10
     
    |
112 | 111 | ad2antlr 733 |
. . . . . . . . 9
         
    |
113 | | eldif 3414 |
. . . . . . . . . 10
           |
114 | 3, 22 | lspssid 18208 |
. . . . . . . . . . . . 13
  
   
       
      |
115 | 13, 21, 114 | syl2anc 667 |
. . . . . . . . . . . 12
 
 
             |
116 | 115 | adantlr 721 |
. . . . . . . . . . 11
          
             |
117 | 116 | sseld 3431 |
. . . . . . . . . 10
              
           |
118 | 113, 117 | syl5bir 222 |
. . . . . . . . 9
                          |
119 | 112, 118 | mpan2d 680 |
. . . . . . . 8
                      |
120 | 119 | reximdva 2862 |
. . . . . . 7
 
       

           |
121 | | eluni2 4202 |
. . . . . . 7
 

  |
122 | | eliun 4283 |
. . . . . . 7
     
   

          |
123 | 120, 121,
122 | 3imtr4g 274 |
. . . . . 6
 
                    |
124 | 110, 123 | mpd 15 |
. . . . 5
 
      
          |
125 | 124 | ex 436 |
. . . 4
       
           |
126 | 125 | ssrdv 3438 |
. . 3
                 |
127 | 126, 9 | syl6sseqr 3479 |
. 2
        |
128 | 108, 127 | jca 535 |
1
          |