Step | Hyp | Ref
| Expression |
1 | | tgpconcomp.s |
. . . . 5
   
↾t     |
2 | | ssrab2 3514 |
. . . . . 6
  
↾t   
  |
3 | | sspwuni 4367 |
. . . . . 6
  
 ↾t    
   
↾t   
  |
4 | 2, 3 | mpbi 212 |
. . . . 5
  
 ↾t     |
5 | 1, 4 | eqsstri 3462 |
. . . 4
 |
6 | 5 | a1i 11 |
. . 3
   |
7 | | tgpconcomp.j |
. . . . . 6
     |
8 | | tgpconcomp.x |
. . . . . 6
     |
9 | 7, 8 | tgptopon 21097 |
. . . . 5
 TopOn    |
10 | | tgpgrp 21093 |
. . . . . 6
   |
11 | | tgpconcomp.z |
. . . . . . 7
     |
12 | 8, 11 | grpidcl 16694 |
. . . . . 6
   |
13 | 10, 12 | syl 17 |
. . . . 5

  |
14 | 1 | concompid 20446 |
. . . . 5
  TopOn     |
15 | 9, 13, 14 | syl2anc 667 |
. . . 4

  |
16 | | ne0i 3737 |
. . . 4
  |
17 | 15, 16 | syl 17 |
. . 3
   |
18 | | df-ima 4847 |
. . . . . . . 8
                           |
19 | | resmpt 5154 |
. . . . . . . . . 10
           
             |
20 | 5, 19 | ax-mp 5 |
. . . . . . . . 9
                       |
21 | 20 | rneqi 5061 |
. . . . . . . 8
          
            |
22 | 18, 21 | eqtri 2473 |
. . . . . . 7
                         |
23 | | imassrn 5179 |
. . . . . . . . 9
                         |
24 | 10 | adantr 467 |
. . . . . . . . . . . . 13
     |
25 | 24 | adantr 467 |
. . . . . . . . . . . 12
    
  |
26 | 6 | sselda 3432 |
. . . . . . . . . . . . 13
     |
27 | 26 | adantr 467 |
. . . . . . . . . . . 12
    
  |
28 | | simpr 463 |
. . . . . . . . . . . 12
    
  |
29 | | eqid 2451 |
. . . . . . . . . . . . 13
         |
30 | 8, 29 | grpsubcl 16734 |
. . . . . . . . . . . 12
 
           |
31 | 25, 27, 28, 30 | syl3anc 1268 |
. . . . . . . . . . 11
    
          |
32 | | eqid 2451 |
. . . . . . . . . . 11
                     |
33 | 31, 32 | fmptd 6046 |
. . . . . . . . . 10
                   |
34 | | frn 5735 |
. . . . . . . . . 10
                        
  |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
            
  |
36 | 23, 35 | syl5ss 3443 |
. . . . . . . 8
                   |
37 | 8, 11, 29 | grpsubid 16738 |
. . . . . . . . . . 11
 
          |
38 | 24, 26, 37 | syl2anc 667 |
. . . . . . . . . 10
            |
39 | | simpr 463 |
. . . . . . . . . . 11
     |
40 | | ovex 6318 |
. . . . . . . . . . 11
         |
41 | | eqid 2451 |
. . . . . . . . . . . 12
                     |
42 | | oveq2 6298 |
. . . . . . . . . . . 12
                   |
43 | 41, 42 | elrnmpt1s 5082 |
. . . . . . . . . . 11
                               |
44 | 39, 40, 43 | sylancl 668 |
. . . . . . . . . 10
                       |
45 | 38, 44 | eqeltrrd 2530 |
. . . . . . . . 9
               |
46 | 45, 22 | syl6eleqr 2540 |
. . . . . . . 8
                   |
47 | | eqid 2451 |
. . . . . . . . 9
   |
48 | | eqid 2451 |
. . . . . . . . . . . . . . 15
       |
49 | | eqid 2451 |
. . . . . . . . . . . . . . 15
           |
50 | 8, 48, 49, 29 | grpsubval 16709 |
. . . . . . . . . . . . . 14
 
                           |
51 | 26, 50 | sylan 474 |
. . . . . . . . . . . . 13
    
                          |
52 | 51 | mpteq2dva 4489 |
. . . . . . . . . . . 12
                                 |
53 | 8, 49 | grpinvcl 16711 |
. . . . . . . . . . . . . 14
 
            |
54 | 24, 53 | sylan 474 |
. . . . . . . . . . . . 13
    
           |
55 | 8, 49 | grpinvf 16710 |
. . . . . . . . . . . . . . . 16
            |
56 | 10, 55 | syl 17 |
. . . . . . . . . . . . . . 15
            |
57 | 56 | adantr 467 |
. . . . . . . . . . . . . 14
              |
58 | 57 | feqmptd 5918 |
. . . . . . . . . . . . 13
                     |
59 | | eqidd 2452 |
. . . . . . . . . . . . 13
                       |
60 | | oveq2 6298 |
. . . . . . . . . . . . 13
                                   |
61 | 54, 58, 59, 60 | fmptco 6056 |
. . . . . . . . . . . 12
                                       |
62 | 52, 61 | eqtr4d 2488 |
. . . . . . . . . . 11
                               |
63 | 7, 49 | grpinvhmeo 21101 |
. . . . . . . . . . . . 13
            |
64 | 63 | adantr 467 |
. . . . . . . . . . . 12
              |
65 | | eqid 2451 |
. . . . . . . . . . . . . 14
                   |
66 | 65, 8, 48, 7 | tgplacthmeo 21118 |
. . . . . . . . . . . . 13
                  |
67 | 26, 66 | syldan 473 |
. . . . . . . . . . . 12
                  |
68 | | hmeoco 20787 |
. . . . . . . . . . . 12
           
                                   |
69 | 64, 67, 68 | syl2anc 667 |
. . . . . . . . . . 11
                         |
70 | 62, 69 | eqeltrd 2529 |
. . . . . . . . . 10
                   |
71 | | hmeocn 20775 |
. . . . . . . . . 10
              

             |
72 | 70, 71 | syl 17 |
. . . . . . . . 9
                 |
73 | | toponuni 19942 |
. . . . . . . . . . . 12
 TopOn 
   |
74 | 9, 73 | syl 17 |
. . . . . . . . . . 11
    |
75 | 74 | adantr 467 |
. . . . . . . . . 10
      |
76 | 5, 75 | syl5sseq 3480 |
. . . . . . . . 9
      |
77 | 1 | concompcon 20447 |
. . . . . . . . . . 11
  TopOn    ↾t    |
78 | 9, 13, 77 | syl2anc 667 |
. . . . . . . . . 10
  ↾t    |
79 | 78 | adantr 467 |
. . . . . . . . 9
    ↾t    |
80 | 47, 72, 76, 79 | conima 20440 |
. . . . . . . 8
    ↾t                  |
81 | 1 | concompss 20448 |
. . . . . . . 8
                              
↾t                                 |
82 | 36, 46, 80, 81 | syl3anc 1268 |
. . . . . . 7
                   |
83 | 22, 82 | syl5eqssr 3477 |
. . . . . 6
            
  |
84 | | ovex 6318 |
. . . . . . . 8
         |
85 | 84, 41 | fnmpti 5706 |
. . . . . . 7
           |
86 | | df-f 5586 |
. . . . . . 7
              
                    
   |
87 | 85, 86 | mpbiran 929 |
. . . . . 6
              
            |
88 | 83, 87 | sylibr 216 |
. . . . 5
                   |
89 | 41 | fmpt 6043 |
. . . . 5
 
                        |
90 | 88, 89 | sylibr 216 |
. . . 4
   
          |
91 | 90 | ralrimiva 2802 |
. . 3
  
          |
92 | 8, 29 | issubg4 16836 |
. . . 4
 
SubGrp   

            |
93 | 10, 92 | syl 17 |
. . 3
  SubGrp  


            |
94 | 6, 17, 91, 93 | mpbir3and 1191 |
. 2
 SubGrp    |
95 | 10 | adantr 467 |
. . . . . . . . . 10
   

  
        |
96 | | eqid 2451 |
. . . . . . . . . . 11
oppg  oppg   |
97 | 96, 49 | oppginv 17010 |
. . . . . . . . . 10
          oppg     |
98 | 95, 97 | syl 17 |
. . . . . . . . 9
   

  
               oppg     |
99 | 98 | fveq1d 5867 |
. . . . . . . 8
   

  
                             oppg                 |
100 | | simprll 772 |
. . . . . . . . 9
   

  
        |
101 | 8, 49 | grpinvinv 16721 |
. . . . . . . . 9
 
                     |
102 | 95, 100, 101 | syl2anc 667 |
. . . . . . . 8
   

  
                          |
103 | 99, 102 | eqtr3d 2487 |
. . . . . . 7
   

  
           oppg                 |
104 | 103 | oveq1d 6305 |
. . . . . 6
   

  
            oppg                  oppg         oppg       |
105 | | eqid 2451 |
. . . . . . 7
  oppg     oppg    |
106 | 48, 96, 105 | oppgplus 17000 |
. . . . . 6
    oppg             |
107 | 104, 106 | syl6eq 2501 |
. . . . 5
   

  
            oppg                  oppg              |
108 | 8, 49 | grpinvcl 16711 |
. . . . . . . . . 10
 
            |
109 | 95, 100, 108 | syl2anc 667 |
. . . . . . . . 9
   

  
                 |
110 | | simprlr 773 |
. . . . . . . . 9
   

  
        |
111 | 102 | oveq1d 6305 |
. . . . . . . . . 10
   

  
                                        |
112 | | simprr 766 |
. . . . . . . . . 10
   

  
               |
113 | 111, 112 | eqeltrd 2529 |
. . . . . . . . 9
   

  
                                 |
114 | | eqid 2451 |
. . . . . . . . . . 11
 ~QG   ~QG   |
115 | 8, 49, 48, 114 | eqgval 16866 |
. . . . . . . . . 10
               ~QG  
         
                             |
116 | 95, 5, 115 | sylancl 668 |
. . . . . . . . 9
   

  
                  ~QG            
                             |
117 | 109, 110,
113, 116 | mpbir3and 1191 |
. . . . . . . 8
   

  
                 ~QG     |
118 | 8, 11, 7, 1, 114 | tgpconcompeqg 21126 |
. . . . . . . . . . . 12
                       ![] ]](rbrack.gif)  ~QG               
↾t      |
119 | 109, 118 | syldan 473 |
. . . . . . . . . . 11
   

  
                 ![] ]](rbrack.gif)  ~QG              
 ↾t      |
120 | 96 | oppgtgp 21113 |
. . . . . . . . . . . . 13
 oppg    |
121 | 120 | adantr 467 |
. . . . . . . . . . . 12
   

  
      oppg    |
122 | 96, 8 | oppgbas 17002 |
. . . . . . . . . . . . 13
   oppg    |
123 | 96, 11 | oppgid 17007 |
. . . . . . . . . . . . 13
   oppg    |
124 | 96, 7 | oppgtopn 17004 |
. . . . . . . . . . . . 13
   oppg    |
125 | | eqid 2451 |
. . . . . . . . . . . . 13
 oppg 
~QG   oppg  ~QG   |
126 | 122, 123,
124, 1, 125 | tgpconcompeqg 21126 |
. . . . . . . . . . . 12
  oppg                       ![] ]](rbrack.gif)  oppg 
~QG   

          
↾t      |
127 | 121, 109,
126 | syl2anc 667 |
. . . . . . . . . . 11
   

  
                 ![] ]](rbrack.gif)  oppg 
~QG   

          
↾t      |
128 | 119, 127 | eqtr4d 2488 |
. . . . . . . . . 10
   

  
                 ![] ]](rbrack.gif)  ~QG             ![] ]](rbrack.gif)  oppg 
~QG    |
129 | 128 | eleq2d 2514 |
. . . . . . . . 9
   

  
                  ![] ]](rbrack.gif)  ~QG             ![] ]](rbrack.gif)  oppg 
~QG     |
130 | | vex 3048 |
. . . . . . . . . 10
 |
131 | | fvex 5875 |
. . . . . . . . . 10
          |
132 | 130, 131 | elec 7403 |
. . . . . . . . 9
            ![] ]](rbrack.gif)  ~QG             ~QG     |
133 | 130, 131 | elec 7403 |
. . . . . . . . 9
            ![] ]](rbrack.gif)  oppg  ~QG 
           oppg  ~QG     |
134 | 129, 132,
133 | 3bitr3g 291 |
. . . . . . . 8
   

  
                  ~QG              oppg  ~QG      |
135 | 117, 134 | mpbid 214 |
. . . . . . 7
   

  
                 oppg  ~QG     |
136 | | eqid 2451 |
. . . . . . . . 9
    oppg       oppg    |
137 | 122, 136,
105, 125 | eqgval 16866 |
. . . . . . . 8
  oppg  
            oppg  ~QG  
         
      oppg                  oppg         |
138 | 121, 5, 137 | sylancl 668 |
. . . . . . 7
   

  
                  oppg  ~QG  
         
      oppg                  oppg         |
139 | 135, 138 | mpbid 214 |
. . . . . 6
   

  
               
      oppg                  oppg        |
140 | 139 | simp3d 1022 |
. . . . 5
   

  
            oppg                  oppg       |
141 | 107, 140 | eqeltrrd 2530 |
. . . 4
   

  
               |
142 | 141 | expr 620 |
. . 3
  
 
       
  
       |
143 | 142 | ralrimivva 2809 |
. 2
  
                  |
144 | 8, 48 | isnsg2 16847 |
. 2
 NrmSGrp   SubGrp   
                   |
145 | 94, 143, 144 | sylanbrc 670 |
1
 NrmSGrp    |