Step | Hyp | Ref
| Expression |
1 | | isgrp2d.3 |
. . 3
         |
2 | | isgrp2d.2 |
. . . . . . . . . 10
   |
3 | 2 | adantr 472 |
. . . . . . . . 9
 
   |
4 | | isgrp2d.6 |
. . . . . . . . . . . 12
 

  
      |
5 | 4 | anass1rs 824 |
. . . . . . . . . . 11
     
      |
6 | | eqcom 2478 |
. . . . . . . . . . . 12
    
      |
7 | 6 | rexbii 2881 |
. . . . . . . . . . 11
     

      |
8 | 5, 7 | sylib 201 |
. . . . . . . . . 10
     
      |
9 | 8 | ralrimiva 2809 |
. . . . . . . . 9
 
 

      |
10 | | r19.2z 3849 |
. . . . . . . . 9
  

     

      |
11 | 3, 9, 10 | syl2anc 673 |
. . . . . . . 8
 
 

      |
12 | 11 | ralrimiva 2809 |
. . . . . . 7
  

      |
13 | | foov 6462 |
. . . . . . 7
      
        

       |
14 | 1, 12, 13 | sylanbrc 677 |
. . . . . 6
         |
15 | | forn 5809 |
. . . . . 6
         |
16 | 14, 15 | syl 17 |
. . . . 5
   |
17 | 16 | sqxpeqd 4865 |
. . . 4
       |
18 | 17, 16 | feq23d 5734 |
. . 3
       
         |
19 | 1, 18 | mpbird 240 |
. 2
      
  |
20 | | isgrp2d.4 |
. . . 4
 

                    |
21 | 20 | ralrimivvva 2815 |
. . 3
  

                  |
22 | 16 | raleqdv 2979 |
. . . . 5
                                        |
23 | 16, 22 | raleqbidv 2987 |
. . . 4
                       
                   |
24 | 16, 23 | raleqbidv 2987 |
. . 3
                         

                   |
25 | 21, 24 | mpbird 240 |
. 2
                         |
26 | | n0 3732 |
. . . . 5
    |
27 | 2, 26 | sylib 201 |
. . . 4
    |
28 | | simpr 468 |
. . . . . . 7
 
   |
29 | 28, 28 | jca 541 |
. . . . . 6
 
 
   |
30 | | isgrp2d.5 |
. . . . . . . 8
 

  
      |
31 | 30 | ralrimivva 2814 |
. . . . . . 7
  

      |
32 | 31 | adantr 472 |
. . . . . 6
 
 


      |
33 | | oveq2 6316 |
. . . . . . . . 9
           |
34 | 33 | eqeq1d 2473 |
. . . . . . . 8
     
       |
35 | 34 | rexbidv 2892 |
. . . . . . 7
  
   

       |
36 | | eqeq2 2482 |
. . . . . . . . 9
     
       |
37 | 36 | rexbidv 2892 |
. . . . . . . 8
  
   

       |
38 | | oveq1 6315 |
. . . . . . . . . 10
           |
39 | 38 | eqeq1d 2473 |
. . . . . . . . 9
     
       |
40 | 39 | cbvrexv 3006 |
. . . . . . . 8
     

      |
41 | 37, 40 | syl6bb 269 |
. . . . . . 7
  
   

       |
42 | 35, 41 | rspc2v 3147 |
. . . . . 6
 
                 |
43 | 29, 32, 42 | sylc 61 |
. . . . 5
 
 
      |
44 | 4 | ralrimivva 2814 |
. . . . . . . . . . . . 13
  

      |
45 | | oveq1 6315 |
. . . . . . . . . . . . . . . . 17
           |
46 | 45 | eqeq1d 2473 |
. . . . . . . . . . . . . . . 16
     
       |
47 | 46 | rexbidv 2892 |
. . . . . . . . . . . . . . 15
  
   

       |
48 | 47 | ralbidv 2829 |
. . . . . . . . . . . . . 14
  

   


       |
49 | 48 | rspccva 3135 |
. . . . . . . . . . . . 13
   

   
  
      |
50 | 44, 49 | sylan 479 |
. . . . . . . . . . . 12
 
 

      |
51 | | eqeq2 2482 |
. . . . . . . . . . . . . . 15
     
       |
52 | 51 | rexbidv 2892 |
. . . . . . . . . . . . . 14
  
   

       |
53 | | oveq2 6316 |
. . . . . . . . . . . . . . . 16
           |
54 | 53 | eqeq1d 2473 |
. . . . . . . . . . . . . . 15
     
       |
55 | 54 | cbvrexv 3006 |
. . . . . . . . . . . . . 14
     

      |
56 | 52, 55 | syl6bb 269 |
. . . . . . . . . . . . 13
  
   

       |
57 | 56 | rspccva 3135 |
. . . . . . . . . . . 12
   
   
        |
58 | 50, 57 | sylan 479 |
. . . . . . . . . . 11
     
      |
59 | 58 | ad2ant2r 761 |
. . . . . . . . . 10
   



             |
60 | 21 | ad3antrrr 744 |
. . . . . . . . . . . . . . . 16
   


       


                  |
61 | | simplr 770 |
. . . . . . . . . . . . . . . . 17
   


      
  |
62 | | simpllr 777 |
. . . . . . . . . . . . . . . . 17
   


      
  |
63 | | simprr 774 |
. . . . . . . . . . . . . . . . 17
   


         |
64 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . 20
           |
65 | 64 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . 19
                   |
66 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . 19
                   |
67 | 65, 66 | eqeq12d 2486 |
. . . . . . . . . . . . . . . . . 18
                 
                   |
68 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . . 20
           |
69 | 68 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . 19
                   |
70 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . 20
           |
71 | 70 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . 19
                   |
72 | 69, 71 | eqeq12d 2486 |
. . . . . . . . . . . . . . . . . 18
                 
                   |
73 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . 19
                   |
74 | 53 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . 19
                   |
75 | 73, 74 | eqeq12d 2486 |
. . . . . . . . . . . . . . . . . 18
                 
                   |
76 | 67, 72, 75 | rspc3v 3150 |
. . . . . . . . . . . . . . . . 17
 
                                        |
77 | 61, 62, 63, 76 | syl3anc 1292 |
. . . . . . . . . . . . . . . 16
   


                                              |
78 | 60, 77 | mpd 15 |
. . . . . . . . . . . . . . 15
   


                         |
79 | | simprl 772 |
. . . . . . . . . . . . . . . 16
   


             |
80 | 79 | oveq1d 6323 |
. . . . . . . . . . . . . . 15
   


                     |
81 | 78, 80 | eqtr3d 2507 |
. . . . . . . . . . . . . 14
   


                     |
82 | 81 | anassrs 660 |
. . . . . . . . . . . . 13
      
                    |
83 | | oveq2 6316 |
. . . . . . . . . . . . . 14
                   |
84 | | id 22 |
. . . . . . . . . . . . . 14
           |
85 | 83, 84 | eqeq12d 2486 |
. . . . . . . . . . . . 13
                 
       |
86 | 82, 85 | syl5ibcom 228 |
. . . . . . . . . . . 12
      
                  |
87 | 86 | rexlimdva 2871 |
. . . . . . . . . . 11
   


      
           |
88 | 87 | adantrl 730 |
. . . . . . . . . 10
   



       
   
       |
89 | 59, 88 | mpd 15 |
. . . . . . . . 9
   



            |
90 | | simplr 770 |
. . . . . . . . . . . . 13
       |
91 | 30 | anassrs 660 |
. . . . . . . . . . . . . . 15
     
      |
92 | 91 | ralrimiva 2809 |
. . . . . . . . . . . . . 14
 
 

      |
93 | 92 | adantlr 729 |
. . . . . . . . . . . . 13
     

      |
94 | | eqeq2 2482 |
. . . . . . . . . . . . . . 15
     
       |
95 | 94 | rexbidv 2892 |
. . . . . . . . . . . . . 14
  
   

       |
96 | 95 | rspcv 3132 |
. . . . . . . . . . . . 13
  

    
       |
97 | 90, 93, 96 | sylc 61 |
. . . . . . . . . . . 12
     
      |
98 | | oveq1 6315 |
. . . . . . . . . . . . . 14
           |
99 | 98 | eqeq1d 2473 |
. . . . . . . . . . . . 13
     
       |
100 | 99 | cbvrexv 3006 |
. . . . . . . . . . . 12
     

      |
101 | 97, 100 | sylib 201 |
. . . . . . . . . . 11
     
      |
102 | 101 | adantllr 733 |
. . . . . . . . . 10
   


 
      |
103 | 102 | adantrr 731 |
. . . . . . . . 9
   



             |
104 | 89, 103 | jca 541 |
. . . . . . . 8
   



           
       |
105 | 104 | expr 626 |
. . . . . . 7
   


                    |
106 | 105 | ralrimdva 2812 |
. . . . . 6
          
              |
107 | 106 | reximdva 2858 |
. . . . 5
 
  
    

              |
108 | 43, 107 | mpd 15 |
. . . 4
 
 

     
       |
109 | 27, 108 | exlimddv 1789 |
. . 3
  
             |
110 | 16 | rexeqdv 2980 |
. . . . . 6
                |
111 | 110 | anbi2d 718 |
. . . . 5
             
     
        |
112 | 16, 111 | raleqbidv 2987 |
. . . 4
         
     

     
        |
113 | 16, 112 | rexeqbidv 2988 |
. . 3
           
     


     
        |
114 | 109, 113 | mpbird 240 |
. 2
                   |
115 | | isgrp2d.1 |
. . . . 5
   |
116 | | xpexg 6612 |
. . . . 5
 
     |
117 | 115, 115,
116 | syl2anc 673 |
. . . 4
     |
118 | | fex 6155 |
. . . 4
             |
119 | 1, 117, 118 | syl2anc 673 |
. . 3
   |
120 | | eqid 2471 |
. . . 4
 |
121 | 120 | isgrpo 26005 |
. . 3
 
      
                               
          |
122 | 119, 121 | syl 17 |
. 2
        
                               
          |
123 | 19, 25, 114, 122 | mpbir3and 1213 |
1
   |