Step | Hyp | Ref
| Expression |
1 | | mplsubglem.u |
. . 3
   supp
   |
2 | | ssrab2 3500 |
. . 3
  supp

 |
3 | 1, 2 | syl6eqss 3468 |
. 2

  |
4 | | mplsubglem.s |
. . . . 5
 mPwSer   |
5 | | mplsubglem.i |
. . . . 5
   |
6 | | mplsubglem.r |
. . . . 5
   |
7 | | mplsubglem.d |
. . . . 5
          |
8 | | mplsubglem.z |
. . . . 5
     |
9 | | mplsubglem.b |
. . . . 5
     |
10 | 4, 5, 6, 7, 8, 9 | psr0cl 18695 |
. . . 4
     |
11 | | eqid 2471 |
. . . . . . . . 9
         |
12 | 11, 8 | grpidcl 16772 |
. . . . . . . 8
       |
13 | | fconst6g 5785 |
. . . . . . . 8
   
            |
14 | 6, 12, 13 | 3syl 18 |
. . . . . . 7
             |
15 | | eldifi 3544 |
. . . . . . . . 9
  
  |
16 | | fvex 5889 |
. . . . . . . . . . 11
     |
17 | 8, 16 | eqeltri 2545 |
. . . . . . . . . 10
 |
18 | 17 | fvconst2 6136 |
. . . . . . . . 9
        |
19 | 15, 18 | syl 17 |
. . . . . . . 8
  
       |
20 | 19 | adantl 473 |
. . . . . . 7
 

         |
21 | 14, 20 | suppss 6964 |
. . . . . 6
    supp   |
22 | | ss0 3768 |
. . . . . 6
    supp    supp
  |
23 | 21, 22 | syl 17 |
. . . . 5
    supp
  |
24 | | mplsubglem.0 |
. . . . 5

  |
25 | 23, 24 | eqeltrd 2549 |
. . . 4
    supp
  |
26 | 1 | eleq2d 2534 |
. . . . 5
        supp
    |
27 | | oveq1 6315 |
. . . . . . 7
    supp    supp
  |
28 | 27 | eleq1d 2533 |
. . . . . 6
     supp
   supp
   |
29 | 28 | elrab 3184 |
. . . . 5
     supp

      supp
   |
30 | 26, 29 | syl6bb 269 |
. . . 4
          supp
    |
31 | 10, 25, 30 | mpbir2and 936 |
. . 3
     |
32 | | ne0i 3728 |
. . 3
     |
33 | 31, 32 | syl 17 |
. 2
   |
34 | | eqid 2471 |
. . . . . . 7
       |
35 | 6 | ad2antrr 740 |
. . . . . . 7
       |
36 | 1 | eleq2d 2534 |
. . . . . . . . . . 11
    supp     |
37 | | oveq1 6315 |
. . . . . . . . . . . . 13
  supp

supp   |
38 | 37 | eleq1d 2533 |
. . . . . . . . . . . 12
   supp
 supp
   |
39 | 38 | elrab 3184 |
. . . . . . . . . . 11
   supp    supp    |
40 | 36, 39 | syl6bb 269 |
. . . . . . . . . 10
   
supp     |
41 | 40 | biimpa 492 |
. . . . . . . . 9
 
  
supp    |
42 | 41 | simpld 466 |
. . . . . . . 8
 
   |
43 | 42 | adantr 472 |
. . . . . . 7
       |
44 | 1 | adantr 472 |
. . . . . . . . . . 11
 
   supp
   |
45 | 44 | eleq2d 2534 |
. . . . . . . . . 10
 
 
  supp     |
46 | | oveq1 6315 |
. . . . . . . . . . . 12
  supp
 supp
  |
47 | 46 | eleq1d 2533 |
. . . . . . . . . . 11
   supp
 supp
   |
48 | 47 | elrab 3184 |
. . . . . . . . . 10
   supp    supp    |
49 | 45, 48 | syl6bb 269 |
. . . . . . . . 9
 
 

 supp
    |
50 | 49 | biimpa 492 |
. . . . . . . 8
       supp
   |
51 | 50 | simpld 466 |
. . . . . . 7
       |
52 | 4, 9, 34, 35, 43, 51 | psraddcl 18684 |
. . . . . 6
              |
53 | | ovex 6336 |
. . . . . . . 8
        supp
 |
54 | 53 | a1i 11 |
. . . . . . 7
             supp   |
55 | 41 | simprd 470 |
. . . . . . . . . 10
 
  supp
  |
56 | 55 | adantr 472 |
. . . . . . . . 9
      supp
  |
57 | 50 | simprd 470 |
. . . . . . . . 9
      supp
  |
58 | | mplsubglem.a |
. . . . . . . . . . 11
 

      |
59 | 58 | ralrimivva 2814 |
. . . . . . . . . 10
  

   |
60 | 59 | ad2antrr 740 |
. . . . . . . . 9
     

    |
61 | | uneq1 3572 |
. . . . . . . . . . 11
  supp     supp    |
62 | 61 | eleq1d 2533 |
. . . . . . . . . 10
  supp      supp     |
63 | | uneq2 3573 |
. . . . . . . . . . 11
  supp   supp    supp
 supp
   |
64 | 63 | eleq1d 2533 |
. . . . . . . . . 10
  supp    supp
   supp  supp     |
65 | 62, 64 | rspc2va 3148 |
. . . . . . . . 9
    supp
 supp
 

     supp
 supp    |
66 | 56, 57, 60, 65 | syl21anc 1291 |
. . . . . . . 8
       supp  supp    |
67 | | mplsubglem.y |
. . . . . . . . . . . 12
 

    |
68 | 67 | expr 626 |
. . . . . . . . . . 11
 
 
   |
69 | 68 | alrimiv 1781 |
. . . . . . . . . 10
 
       |
70 | 69 | ralrimiva 2809 |
. . . . . . . . 9
        |
71 | 70 | ad2antrr 740 |
. . . . . . . 8
     
      |
72 | | sseq2 3440 |
. . . . . . . . . . 11
   supp  supp
    supp  supp
    |
73 | 72 | imbi1d 324 |
. . . . . . . . . 10
   supp  supp
       supp
 supp      |
74 | 73 | albidv 1775 |
. . . . . . . . 9
   supp  supp
    

     supp  supp 
    |
75 | 74 | rspcv 3132 |
. . . . . . . 8
   supp  supp      
      supp
 supp      |
76 | 66, 71, 75 | sylc 61 |
. . . . . . 7
          supp  supp 
   |
77 | 4, 11, 7, 9, 52 | psrelbas 18680 |
. . . . . . . 8
                      |
78 | | eqid 2471 |
. . . . . . . . . . . 12
       |
79 | 4, 9, 78, 34, 43, 51 | psradd 18683 |
. . . . . . . . . . 11
                      |
80 | 79 | fveq1d 5881 |
. . . . . . . . . 10
                              |
81 | 80 | adantr 472 |
. . . . . . . . 9
   



  supp  supp                             |
82 | | eldifi 3544 |
. . . . . . . . . 10
    supp
 supp     |
83 | 4, 11, 7, 9, 42 | psrelbas 18680 |
. . . . . . . . . . . . 13
 
           |
84 | 83 | adantr 472 |
. . . . . . . . . . . 12
               |
85 | 84 | ffnd 5740 |
. . . . . . . . . . 11
       |
86 | 4, 11, 7, 9, 51 | psrelbas 18680 |
. . . . . . . . . . . 12
               |
87 | 86 | ffnd 5740 |
. . . . . . . . . . 11
       |
88 | | ovex 6336 |
. . . . . . . . . . . . 13
   |
89 | 7, 88 | rabex2 4552 |
. . . . . . . . . . . 12
 |
90 | 89 | a1i 11 |
. . . . . . . . . . 11
       |
91 | | inidm 3632 |
. . . . . . . . . . 11
   |
92 | | eqidd 2472 |
. . . . . . . . . . 11
   


           |
93 | | eqidd 2472 |
. . . . . . . . . . 11
   


           |
94 | 85, 87, 90, 90, 91, 92, 93 | ofval 6559 |
. . . . . . . . . 10
   


                              |
95 | 82, 94 | sylan2 482 |
. . . . . . . . 9
   



  supp  supp                                 |
96 | | ssun1 3588 |
. . . . . . . . . . . . . 14
 supp   supp  supp   |
97 | | sscon 3556 |
. . . . . . . . . . . . . 14
  supp
  supp
 supp     supp  supp
 
  supp    |
98 | 96, 97 | ax-mp 5 |
. . . . . . . . . . . . 13
   supp  supp
 
  supp   |
99 | 98 | sseli 3414 |
. . . . . . . . . . . 12
    supp
 supp     supp    |
100 | | ssid 3437 |
. . . . . . . . . . . . . . 15
 supp  supp
 |
101 | 100 | a1i 11 |
. . . . . . . . . . . . . 14
 
  supp

supp   |
102 | 89 | a1i 11 |
. . . . . . . . . . . . . 14
 
   |
103 | 17 | a1i 11 |
. . . . . . . . . . . . . 14
 
   |
104 | 83, 101, 102, 103 | suppssr 6965 |
. . . . . . . . . . . . 13
      supp
 
     |
105 | 104 | adantlr 729 |
. . . . . . . . . . . 12
   



 supp
 
     |
106 | 99, 105 | sylan2 482 |
. . . . . . . . . . 11
   



  supp  supp         |
107 | | ssun2 3589 |
. . . . . . . . . . . . . 14
 supp   supp  supp   |
108 | | sscon 3556 |
. . . . . . . . . . . . . 14
  supp
  supp
 supp     supp  supp
 
  supp    |
109 | 107, 108 | ax-mp 5 |
. . . . . . . . . . . . 13
   supp  supp
 
  supp   |
110 | 109 | sseli 3414 |
. . . . . . . . . . . 12
    supp
 supp     supp    |
111 | | ssid 3437 |
. . . . . . . . . . . . . 14
 supp  supp
 |
112 | 111 | a1i 11 |
. . . . . . . . . . . . 13
      supp
 supp
  |
113 | 17 | a1i 11 |
. . . . . . . . . . . . 13
       |
114 | 86, 112, 90, 113 | suppssr 6965 |
. . . . . . . . . . . 12
   



 supp
 
     |
115 | 110, 114 | sylan2 482 |
. . . . . . . . . . 11
   



  supp  supp         |
116 | 106, 115 | oveq12d 6326 |
. . . . . . . . . 10
   



  supp  supp                        |
117 | 11, 78, 8 | grplid 16774 |
. . . . . . . . . . . . 13
           |
118 | 12, 117 | mpdan 681 |
. . . . . . . . . . . 12
     |
119 | 35, 118 | syl 17 |
. . . . . . . . . . 11
         |
120 | 119 | adantr 472 |
. . . . . . . . . 10
   



  supp  supp        |
121 | 116, 120 | eqtrd 2505 |
. . . . . . . . 9
   



  supp  supp                    |
122 | 81, 95, 121 | 3eqtrd 2509 |
. . . . . . . 8
   



  supp  supp                |
123 | 77, 122 | suppss 6964 |
. . . . . . 7
             supp   supp  supp    |
124 | | sseq1 3439 |
. . . . . . . . 9
         supp    supp
 supp 
        supp   supp  supp
    |
125 | | eleq1 2537 |
. . . . . . . . 9
         supp          supp
   |
126 | 124, 125 | imbi12d 327 |
. . . . . . . 8
         supp     supp  supp
           supp   supp  supp
         supp     |
127 | 126 | spcgv 3120 |
. . . . . . 7
         supp    
  supp
 supp

          supp   supp
 supp          supp     |
128 | 54, 76, 123, 127 | syl3c 62 |
. . . . . 6
             supp   |
129 | 1 | ad2antrr 740 |
. . . . . . . 8
       supp
   |
130 | 129 | eleq2d 2534 |
. . . . . . 7
            
  
      supp     |
131 | | oveq1 6315 |
. . . . . . . . 9
         supp
        supp   |
132 | 131 | eleq1d 2533 |
. . . . . . . 8
          supp
        supp
   |
133 | 132 | elrab 3184 |
. . . . . . 7
          supp
                 supp    |
134 | 130, 133 | syl6bb 269 |
. . . . . 6
            
                supp
    |
135 | 52, 128, 134 | mpbir2and 936 |
. . . . 5
              |
136 | 135 | ralrimiva 2809 |
. . . 4
 
 
  
      |
137 | 4, 5, 6 | psrgrp 18699 |
. . . . . 6
   |
138 | | eqid 2471 |
. . . . . . 7
           |
139 | 9, 138 | grpinvcl 16789 |
. . . . . 6
 
            |
140 | 137, 42, 139 | syl2an2r 849 |
. . . . 5
 
            |
141 | | ovex 6336 |
. . . . . . 7
          supp
 |
142 | 141 | a1i 11 |
. . . . . 6
 
           supp
  |
143 | 70 | adantr 472 |
. . . . . . 7
 
 
      |
144 | | sseq2 3440 |
. . . . . . . . . 10
  supp 
 supp    |
145 | 144 | imbi1d 324 |
. . . . . . . . 9
  supp   
  supp     |
146 | 145 | albidv 1775 |
. . . . . . . 8
  supp         
supp     |
147 | 146 | rspcv 3132 |
. . . . . . 7
  supp
 
        supp     |
148 | 55, 143, 147 | sylc 61 |
. . . . . 6
 
     supp
   |
149 | 4, 11, 7, 9, 140 | psrelbas 18680 |
. . . . . . 7
 
                    |
150 | 5 | adantr 472 |
. . . . . . . . . . 11
 
   |
151 | 6 | adantr 472 |
. . . . . . . . . . 11
 
   |
152 | | eqid 2471 |
. . . . . . . . . . 11
           |
153 | 4, 150, 151, 7, 152, 9, 138, 42 | psrneg 18701 |
. . . . . . . . . 10
 
                   |
154 | 153 | adantr 472 |
. . . . . . . . 9
      supp
 
                  |
155 | 154 | fveq1d 5881 |
. . . . . . . 8
      supp
 
                          |
156 | | eldifi 3544 |
. . . . . . . . 9
   supp 
  |
157 | | fvco3 5957 |
. . . . . . . . 9
                                     |
158 | 83, 156, 157 | syl2an 485 |
. . . . . . . 8
      supp
 
                          |
159 | 104 | fveq2d 5883 |
. . . . . . . . 9
      supp
 
                      |
160 | 8, 152 | grpinvid 16795 |
. . . . . . . . . . 11
       
 |
161 | 151, 160 | syl 17 |
. . . . . . . . . 10
 
       
 |
162 | 161 | adantr 472 |
. . . . . . . . 9
      supp
 
        |
163 | 159, 162 | eqtrd 2505 |
. . . . . . . 8
      supp
 
              |
164 | 155, 158,
163 | 3eqtrd 2509 |
. . . . . . 7
      supp
 
              |
165 | 149, 164 | suppss 6964 |
. . . . . 6
 
           supp

supp   |
166 | | sseq1 3439 |
. . . . . . . 8
           supp
  supp           supp  supp    |
167 | | eleq1 2537 |
. . . . . . . 8
           supp

          supp
   |
168 | 166, 167 | imbi12d 327 |
. . . . . . 7
           supp
 
 supp

           supp

supp           supp
    |
169 | 168 | spcgv 3120 |
. . . . . 6
           supp
     supp
            supp
 supp           supp
    |
170 | 142, 148,
165, 169 | syl3c 62 |
. . . . 5
 
           supp
  |
171 | 44 | eleq2d 2534 |
. . . . . 6
 
          
           supp
    |
172 | | oveq1 6315 |
. . . . . . . 8
           supp           supp   |
173 | 172 | eleq1d 2533 |
. . . . . . 7
            supp
          supp
   |
174 | 173 | elrab 3184 |
. . . . . 6
            supp

         
          supp
   |
175 | 171, 174 | syl6bb 269 |
. . . . 5
 
          
                    supp
    |
176 | 140, 170,
175 | mpbir2and 936 |
. . . 4
 
            |
177 | 136, 176 | jca 541 |
. . 3
 
  
                   |
178 | 177 | ralrimiva 2809 |
. 2
                       |
179 | 9, 34, 138 | issubg2 16910 |
. . 3
 
SubGrp   
 
                     |
180 | 137, 179 | syl 17 |
. 2
  SubGrp 
   
  
                  |
181 | 3, 33, 178, 180 | mpbir3and 1213 |
1
 SubGrp    |