Step | Hyp | Ref
| Expression |
1 | | gaset 16959 |
. . 3
    |
2 | | gasubg.1 |
. . . 4

↾s   |
3 | 2 | subggrp 16832 |
. . 3
 SubGrp 
  |
4 | 1, 3 | anim12ci 571 |
. 2

  SubGrp  
    |
5 | | eqid 2453 |
. . . . . . 7
         |
6 | 5 | gaf 16961 |
. . . . . 6
             |
7 | 6 | adantr 467 |
. . . . 5

  SubGrp  
           |
8 | | simpr 463 |
. . . . . . 7

  SubGrp  
SubGrp    |
9 | 5 | subgss 16830 |
. . . . . . 7
 SubGrp 
      |
10 | 8, 9 | syl 17 |
. . . . . 6

  SubGrp  
      |
11 | | xpss1 4946 |
. . . . . 6
    
          |
12 | 10, 11 | syl 17 |
. . . . 5

  SubGrp  
          |
13 | 7, 12 | fssresd 5755 |
. . . 4

  SubGrp  
           |
14 | 2 | subgbas 16833 |
. . . . . . 7
 SubGrp 
      |
15 | 8, 14 | syl 17 |
. . . . . 6

  SubGrp  
      |
16 | 15 | xpeq1d 4860 |
. . . . 5

  SubGrp  
          |
17 | 16 | feq2d 5720 |
. . . 4

  SubGrp  
         
                |
18 | 13, 17 | mpbid 214 |
. . 3

  SubGrp  
               |
19 | 8 | adantr 467 |
. . . . . . . 8
 
 
SubGrp    SubGrp    |
20 | | eqid 2453 |
. . . . . . . . 9
         |
21 | 20 | subg0cl 16837 |
. . . . . . . 8
 SubGrp 
      |
22 | 19, 21 | syl 17 |
. . . . . . 7
 
 
SubGrp          |
23 | | simpr 463 |
. . . . . . 7
 
 
SubGrp      |
24 | | ovres 6441 |
. . . . . . 7
     
                    |
25 | 22, 23, 24 | syl2anc 667 |
. . . . . 6
 
 
SubGrp                       |
26 | 2, 20 | subg0 16835 |
. . . . . . . 8
 SubGrp 
          |
27 | 19, 26 | syl 17 |
. . . . . . 7
 
 
SubGrp              |
28 | 27 | oveq1d 6310 |
. . . . . 6
 
 
SubGrp                            |
29 | 20 | gagrpid 16960 |
. . . . . . 7

           |
30 | 29 | adantlr 722 |
. . . . . 6
 
 
SubGrp            |
31 | 25, 28, 30 | 3eqtr3d 2495 |
. . . . 5
 
 
SubGrp                 |
32 | | eqimss2 3487 |
. . . . . . . . . . 11
    
      |
33 | 15, 32 | syl 17 |
. . . . . . . . . 10

  SubGrp  
      |
34 | 33 | adantr 467 |
. . . . . . . . 9
 
 
SubGrp          |
35 | 34 | sselda 3434 |
. . . . . . . 8
    
SubGrp           |
36 | 34 | sselda 3434 |
. . . . . . . 8
    
SubGrp           |
37 | 35, 36 | anim12dan 849 |
. . . . . . 7
    
SubGrp               
   |
38 | | simprl 765 |
. . . . . . . . . 10
    
SubGrp    
 
  |
39 | 7 | ad2antrr 733 |
. . . . . . . . . . 11
    
SubGrp    
 
           |
40 | 9 | ad3antlr 738 |
. . . . . . . . . . . 12
    
SubGrp    
 
      |
41 | | simprr 767 |
. . . . . . . . . . . 12
    
SubGrp    
 
  |
42 | 40, 41 | sseldd 3435 |
. . . . . . . . . . 11
    
SubGrp    
 
      |
43 | 23 | adantr 467 |
. . . . . . . . . . 11
    
SubGrp    
 
  |
44 | 39, 42, 43 | fovrnd 6446 |
. . . . . . . . . 10
    
SubGrp    
 
    |
45 | | ovres 6441 |
. . . . . . . . . 10
                    |
46 | 38, 44, 45 | syl2anc 667 |
. . . . . . . . 9
    
SubGrp    
 
      
        |
47 | | ovres 6441 |
. . . . . . . . . . 11
 
            |
48 | 41, 43, 47 | syl2anc 667 |
. . . . . . . . . 10
    
SubGrp    
 
           |
49 | 48 | oveq2d 6311 |
. . . . . . . . 9
    
SubGrp    
 
                         |
50 | | simplll 769 |
. . . . . . . . . 10
    
SubGrp    
 
    |
51 | 40, 38 | sseldd 3435 |
. . . . . . . . . 10
    
SubGrp    
 
      |
52 | | eqid 2453 |
. . . . . . . . . . 11
       |
53 | 5, 52 | gaass 16963 |
. . . . . . . . . 10

          
            
    |
54 | 50, 51, 42, 43, 53 | syl13anc 1271 |
. . . . . . . . 9
    
SubGrp    
 
               |
55 | 46, 49, 54 | 3eqtr4d 2497 |
. . . . . . . 8
    
SubGrp    
 
                         |
56 | 52 | subgcl 16839 |
. . . . . . . . . . 11
  SubGrp 
          |
57 | 56 | 3expb 1210 |
. . . . . . . . . 10
  SubGrp  
 
  
      |
58 | 19, 57 | sylan 474 |
. . . . . . . . 9
    
SubGrp    
 
  
      |
59 | | ovres 6441 |
. . . . . . . . 9
                  
                |
60 | 58, 43, 59 | syl2anc 667 |
. . . . . . . 8
    
SubGrp    
 
                         |
61 | 2, 52 | ressplusg 15251 |
. . . . . . . . . . 11
 SubGrp 
        |
62 | 61 | ad3antlr 738 |
. . . . . . . . . 10
    
SubGrp    
 
        |
63 | 62 | oveqd 6312 |
. . . . . . . . 9
    
SubGrp    
 
  
             |
64 | 63 | oveq1d 6310 |
. . . . . . . 8
    
SubGrp    
 
                              |
65 | 55, 60, 64 | 3eqtr2rd 2494 |
. . . . . . 7
    
SubGrp    
 
               
              |
66 | 37, 65 | syldan 473 |
. . . . . 6
    
SubGrp                                             |
67 | 66 | ralrimivva 2811 |
. . . . 5
 
 
SubGrp                               
              |
68 | 31, 67 | jca 535 |
. . . 4
 
 
SubGrp                
                          
               |
69 | 68 | ralrimiva 2804 |
. . 3

  SubGrp  

                                       
               |
70 | 18, 69 | jca 535 |
. 2

  SubGrp  
              
                                       
                |
71 | | eqid 2453 |
. . 3
         |
72 | | eqid 2453 |
. . 3
       |
73 | | eqid 2453 |
. . 3
         |
74 | 71, 72, 73 | isga 16957 |
. 2
       

              
                                       
                 |
75 | 4, 70, 74 | sylanbrc 671 |
1

  SubGrp  
       |