Step | Hyp | Ref
| Expression |
1 | | subgga.3 |
. . . 4

↾s   |
2 | 1 | subggrp 16820 |
. . 3
 SubGrp 
  |
3 | | subgga.1 |
. . . 4
     |
4 | | fvex 5875 |
. . . 4
     |
5 | 3, 4 | eqeltri 2525 |
. . 3
 |
6 | 2, 5 | jctir 541 |
. 2
 SubGrp 
    |
7 | | subgrcl 16822 |
. . . . . . . 8
 SubGrp 
  |
8 | 7 | adantr 467 |
. . . . . . 7
  SubGrp  
 
  |
9 | 3 | subgss 16818 |
. . . . . . . . 9
 SubGrp 
  |
10 | 9 | sselda 3432 |
. . . . . . . 8
  SubGrp     |
11 | 10 | adantrr 723 |
. . . . . . 7
  SubGrp  
 
  |
12 | | simprr 766 |
. . . . . . 7
  SubGrp  
 
  |
13 | | subgga.2 |
. . . . . . . 8
    |
14 | 3, 13 | grpcl 16679 |
. . . . . . 7
 
     |
15 | 8, 11, 12, 14 | syl3anc 1268 |
. . . . . 6
  SubGrp  
 
    |
16 | 15 | ralrimivva 2809 |
. . . . 5
 SubGrp 


    |
17 | | subgga.4 |
. . . . . 6
 
    |
18 | 17 | fmpt2 6860 |
. . . . 5
 



        |
19 | 16, 18 | sylib 200 |
. . . 4
 SubGrp 
        |
20 | 1 | subgbas 16821 |
. . . . . 6
 SubGrp 
      |
21 | 20 | xpeq1d 4857 |
. . . . 5
 SubGrp 
          |
22 | 21 | feq2d 5715 |
. . . 4
 SubGrp 
      
             |
23 | 19, 22 | mpbid 214 |
. . 3
 SubGrp 
            |
24 | | eqid 2451 |
. . . . . . . 8
         |
25 | 24 | subg0cl 16825 |
. . . . . . 7
 SubGrp 
      |
26 | | oveq12 6299 |
. . . . . . . 8
     
           |
27 | | ovex 6318 |
. . . . . . . 8
       |
28 | 26, 17, 27 | ovmpt2a 6427 |
. . . . . . 7
     
                 |
29 | 25, 28 | sylan 474 |
. . . . . 6
  SubGrp                   |
30 | 1, 24 | subg0 16823 |
. . . . . . . 8
 SubGrp 
          |
31 | 30 | oveq1d 6305 |
. . . . . . 7
 SubGrp 
                  |
32 | 31 | adantr 467 |
. . . . . 6
  SubGrp                     |
33 | 3, 13, 24 | grplid 16696 |
. . . . . . 7
 
         |
34 | 7, 33 | sylan 474 |
. . . . . 6
  SubGrp       
   |
35 | 29, 32, 34 | 3eqtr3d 2493 |
. . . . 5
  SubGrp             |
36 | 7 | ad2antrr 732 |
. . . . . . . . . 10
   SubGrp   
 
  |
37 | 9 | ad2antrr 732 |
. . . . . . . . . . 11
   SubGrp   
 
  |
38 | | simprl 764 |
. . . . . . . . . . 11
   SubGrp   
 
  |
39 | 37, 38 | sseldd 3433 |
. . . . . . . . . 10
   SubGrp   
 
  |
40 | | simprr 766 |
. . . . . . . . . . 11
   SubGrp   
 
  |
41 | 37, 40 | sseldd 3433 |
. . . . . . . . . 10
   SubGrp   
 
  |
42 | | simplr 762 |
. . . . . . . . . 10
   SubGrp   
 
  |
43 | 3, 13 | grpass 16680 |
. . . . . . . . . 10
  
    
  
    |
44 | 36, 39, 41, 42, 43 | syl13anc 1270 |
. . . . . . . . 9
   SubGrp   
 
 
        |
45 | 3, 13 | grpcl 16679 |
. . . . . . . . . . 11
 
     |
46 | 36, 41, 42, 45 | syl3anc 1268 |
. . . . . . . . . 10
   SubGrp   
 
    |
47 | | oveq12 6299 |
. . . . . . . . . . 11
 
           |
48 | | ovex 6318 |
. . . . . . . . . . 11
     |
49 | 47, 17, 48 | ovmpt2a 6427 |
. . . . . . . . . 10
  
              |
50 | 38, 46, 49 | syl2anc 667 |
. . . . . . . . 9
   SubGrp   
 
       
    |
51 | 44, 50 | eqtr4d 2488 |
. . . . . . . 8
   SubGrp   
 
 
          |
52 | 13 | subgcl 16827 |
. . . . . . . . . . 11
  SubGrp 
 
   |
53 | 52 | 3expb 1209 |
. . . . . . . . . 10
  SubGrp  
 
    |
54 | 53 | adantlr 721 |
. . . . . . . . 9
   SubGrp   
 
    |
55 | | oveq12 6299 |
. . . . . . . . . 10
   
         |
56 | | ovex 6318 |
. . . . . . . . . 10
     |
57 | 55, 17, 56 | ovmpt2a 6427 |
. . . . . . . . 9
   
             |
58 | 54, 42, 57 | syl2anc 667 |
. . . . . . . 8
   SubGrp   
 
 
          |
59 | | oveq12 6299 |
. . . . . . . . . . 11
 
       |
60 | | ovex 6318 |
. . . . . . . . . . 11
   |
61 | 59, 17, 60 | ovmpt2a 6427 |
. . . . . . . . . 10
 
         |
62 | 40, 42, 61 | syl2anc 667 |
. . . . . . . . 9
   SubGrp   
 
        |
63 | 62 | oveq2d 6306 |
. . . . . . . 8
   SubGrp   
 
                |
64 | 51, 58, 63 | 3eqtr4d 2495 |
. . . . . . 7
   SubGrp   
 
 
              |
65 | 64 | ralrimivva 2809 |
. . . . . 6
  SubGrp   

 
              |
66 | 1, 13 | ressplusg 15239 |
. . . . . . . . . . . 12
 SubGrp 
     |
67 | 66 | oveqd 6307 |
. . . . . . . . . . 11
 SubGrp 
           |
68 | 67 | oveq1d 6305 |
. . . . . . . . . 10
 SubGrp 
 
                 |
69 | 68 | eqeq1d 2453 |
. . . . . . . . 9
 SubGrp 
              
                      |
70 | 20, 69 | raleqbidv 3001 |
. . . . . . . 8
 SubGrp 
 
             
                            |
71 | 20, 70 | raleqbidv 3001 |
. . . . . . 7
 SubGrp 
 

             
                                  |
72 | 71 | biimpa 487 |
. . . . . 6
  SubGrp  

               
     
                          |
73 | 65, 72 | syldan 473 |
. . . . 5
  SubGrp                                    |
74 | 35, 73 | jca 535 |
. . . 4
  SubGrp                                              |
75 | 74 | ralrimiva 2802 |
. . 3
 SubGrp 

         
                                 |
76 | 23, 75 | jca 535 |
. 2
 SubGrp 
           
                                            |
77 | | eqid 2451 |
. . 3
         |
78 | | eqid 2451 |
. . 3
       |
79 | | eqid 2451 |
. . 3
         |
80 | 77, 78, 79 | isga 16945 |
. 2
                 
                                             |
81 | 6, 76, 80 | sylanbrc 670 |
1
 SubGrp 

   |