Step | Hyp | Ref
| Expression |
1 | | dfec2 7371 |
. . . . 5
       |
2 | 1 | adantl 468 |
. . . 4
         |
3 | | tgpconcomp.s |
. . . . . . . . 9
   
↾t     |
4 | | ssrab2 3516 |
. . . . . . . . . 10
  
↾t   
  |
5 | | sspwuni 4370 |
. . . . . . . . . 10
  
 ↾t    
   
↾t   
  |
6 | 4, 5 | mpbi 212 |
. . . . . . . . 9
  
 ↾t     |
7 | 3, 6 | eqsstri 3464 |
. . . . . . . 8
 |
8 | 7 | a1i 11 |
. . . . . . 7
     |
9 | | tgpconcomp.x |
. . . . . . . 8
     |
10 | | eqid 2453 |
. . . . . . . 8
           |
11 | | eqid 2453 |
. . . . . . . 8
       |
12 | | tgpconcompeqg.r |
. . . . . . . 8

~QG   |
13 | 9, 10, 11, 12 | eqgval 16878 |
. . . . . . 7
   

                    |
14 | 8, 13 | syldan 473 |
. . . . . 6
   

                    |
15 | | simp2 1010 |
. . . . . 6
 
                
  |
16 | 14, 15 | syl6bi 232 |
. . . . 5
       |
17 | 16 | abssdv 3505 |
. . . 4
       |
18 | 2, 17 | eqsstrd 3468 |
. . 3
    
  |
19 | | simpr 463 |
. . . . 5
     |
20 | | tgpgrp 21105 |
. . . . . . 7
   |
21 | | tgpconcomp.z |
. . . . . . . 8
     |
22 | 9, 11, 21, 10 | grplinv 16724 |
. . . . . . 7
 
                  |
23 | 20, 22 | sylan 474 |
. . . . . 6
                    |
24 | | tgpconcomp.j |
. . . . . . . . 9
     |
25 | 24, 9 | tgptopon 21109 |
. . . . . . . 8
 TopOn    |
26 | 25 | adantr 467 |
. . . . . . 7
   TopOn    |
27 | 20 | adantr 467 |
. . . . . . . 8
     |
28 | 9, 21 | grpidcl 16706 |
. . . . . . . 8
   |
29 | 27, 28 | syl 17 |
. . . . . . 7
     |
30 | 3 | concompid 20458 |
. . . . . . 7
  TopOn     |
31 | 26, 29, 30 | syl2anc 667 |
. . . . . 6
     |
32 | 23, 31 | eqeltrd 2531 |
. . . . 5
                     |
33 | 9, 10, 11, 12 | eqgval 16878 |
. . . . . 6
   

                    |
34 | 8, 33 | syldan 473 |
. . . . 5
   

                    |
35 | 19, 19, 32, 34 | mpbir3and 1192 |
. . . 4
     |
36 | | elecg 7407 |
. . . . 5
 
   
   |
37 | 19, 19, 36 | syl2anc 667 |
. . . 4
   
 
   |
38 | 35, 37 | mpbird 236 |
. . 3
      |
39 | 9, 12, 11 | eqglact 16880 |
. . . . . . 7
                    |
40 | 7, 39 | mp3an2 1354 |
. . . . . 6
 
                  |
41 | 20, 40 | sylan 474 |
. . . . 5
                    |
42 | 41 | oveq2d 6311 |
. . . 4
    ↾t    ↾t                 |
43 | | eqid 2453 |
. . . . 5
   |
44 | | eqid 2453 |
. . . . . . 7
                   |
45 | 44, 9, 11, 24 | tgplacthmeo 21130 |
. . . . . 6
                  |
46 | | hmeocn 20787 |
. . . . . 6
             

            |
47 | 45, 46 | syl 17 |
. . . . 5
                |
48 | | toponuni 19954 |
. . . . . . 7
 TopOn 
   |
49 | 26, 48 | syl 17 |
. . . . . 6
      |
50 | 7, 49 | syl5sseq 3482 |
. . . . 5
      |
51 | 3 | concompcon 20459 |
. . . . . 6
  TopOn    ↾t    |
52 | 26, 29, 51 | syl2anc 667 |
. . . . 5
    ↾t    |
53 | 43, 47, 50, 52 | conima 20452 |
. . . 4
    ↾t                 |
54 | 42, 53 | eqeltrd 2531 |
. . 3
    ↾t     |
55 | | eqid 2453 |
. . . 4
     ↾t   
    
↾t     |
56 | 55 | concompss 20460 |
. . 3
      
↾t  
       
↾t      |
57 | 18, 38, 54, 56 | syl3anc 1269 |
. 2
    
    
↾t      |
58 | | elpwi 3962 |
. . . . . 6
 
  |
59 | 44 | mptpreima 5331 |
. . . . . . . . . . . 12
                        |
60 | | ssrab2 3516 |
. . . . . . . . . . . 12
          |
61 | 59, 60 | eqsstri 3464 |
. . . . . . . . . . 11
               |
62 | 61 | a1i 11 |
. . . . . . . . . 10
       ↾t                     |
63 | 29 | adantr 467 |
. . . . . . . . . . 11
       ↾t       |
64 | 9, 11, 21 | grprid 16709 |
. . . . . . . . . . . . . 14
 
        |
65 | 20, 64 | sylan 474 |
. . . . . . . . . . . . 13
          |
66 | 65 | adantr 467 |
. . . . . . . . . . . 12
       ↾t            |
67 | | simprrl 775 |
. . . . . . . . . . . 12
       ↾t       |
68 | 66, 67 | eqeltrd 2531 |
. . . . . . . . . . 11
       ↾t            |
69 | | oveq2 6303 |
. . . . . . . . . . . . 13
               |
70 | 69 | eleq1d 2515 |
. . . . . . . . . . . 12
        
  
     |
71 | 70, 59 | elrab2 3200 |
. . . . . . . . . . 11
             
        |
72 | 63, 68, 71 | sylanbrc 671 |
. . . . . . . . . 10
       ↾t                     |
73 | | hmeocnvcn 20788 |
. . . . . . . . . . . . 13
             
              |
74 | 45, 73 | syl 17 |
. . . . . . . . . . . 12
                 |
75 | 74 | adantr 467 |
. . . . . . . . . . 11
       ↾t                   |
76 | | simprl 765 |
. . . . . . . . . . . 12
       ↾t       |
77 | 49 | adantr 467 |
. . . . . . . . . . . 12
       ↾t        |
78 | 76, 77 | sseqtrd 3470 |
. . . . . . . . . . 11
       ↾t        |
79 | | simprrr 776 |
. . . . . . . . . . 11
       ↾t      ↾t    |
80 | 43, 75, 78, 79 | conima 20452 |
. . . . . . . . . 10
       ↾t      ↾t                  |
81 | 3 | concompss 20460 |
. . . . . . . . . 10
                               ↾t                                 |
82 | 62, 72, 80, 81 | syl3anc 1269 |
. . . . . . . . 9
       ↾t                     |
83 | | eqid 2453 |
. . . . . . . . . . . . . . . 16
                       |
84 | 83, 9, 11, 10 | grplactcnv 16766 |
. . . . . . . . . . . . . . 15
 
                                                                |
85 | 20, 84 | sylan 474 |
. . . . . . . . . . . . . 14
                                                                  |
86 | 85 | simpld 461 |
. . . . . . . . . . . . 13
                        |
87 | 83, 9 | grplactfval 16764 |
. . . . . . . . . . . . . . 15
                           |
88 | 87 | adantl 468 |
. . . . . . . . . . . . . 14
                             |
89 | | f1oeq1 5810 |
. . . . . . . . . . . . . 14
                                                             |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . 13
                                       |
91 | 86, 90 | mpbid 214 |
. . . . . . . . . . . 12
                  |
92 | 91 | adantr 467 |
. . . . . . . . . . 11
       ↾t                    |
93 | | f1ocnv 5831 |
. . . . . . . . . . 11
             
                |
94 | | f1ofun 5821 |
. . . . . . . . . . 11
                           |
95 | 92, 93, 94 | 3syl 18 |
. . . . . . . . . 10
       ↾t                 |
96 | | f1odm 5823 |
. . . . . . . . . . . 12
                           |
97 | 92, 93, 96 | 3syl 18 |
. . . . . . . . . . 11
       ↾t                 |
98 | 76, 97 | sseqtr4d 3471 |
. . . . . . . . . 10
       ↾t                 |
99 | | funimass3 6003 |
. . . . . . . . . 10
                                     
                  |
100 | 95, 98, 99 | syl2anc 667 |
. . . . . . . . 9
       ↾t                   
                  |
101 | 82, 100 | mpbid 214 |
. . . . . . . 8
       ↾t                      |
102 | 41 | adantr 467 |
. . . . . . . . 9
       ↾t                      |
103 | | imacnvcnv 5303 |
. . . . . . . . 9
                             |
104 | 102, 103 | syl6eqr 2505 |
. . . . . . . 8
       ↾t                        |
105 | 101, 104 | sseqtr4d 3471 |
. . . . . . 7
       ↾t        |
106 | 105 | expr 620 |
. . . . . 6
    
 

↾t       |
107 | 58, 106 | sylan2 477 |
. . . . 5
         ↾t  
    |
108 | 107 | ralrimiva 2804 |
. . . 4
       
↾t       |
109 | | eleq2 2520 |
. . . . . 6
 
   |
110 | | oveq2 6303 |
. . . . . . 7
  ↾t   ↾t    |
111 | 110 | eleq1d 2515 |
. . . . . 6
  
↾t   ↾t     |
112 | 109, 111 | anbi12d 718 |
. . . . 5
   
↾t     ↾t      |
113 | 112 | ralrab 3202 |
. . . 4
 
   
↾t            ↾t       |
114 | 108, 113 | sylibr 216 |
. . 3
     

 ↾t        |
115 | | unissb 4232 |
. . 3
  


 ↾t   
       ↾t        |
116 | 114, 115 | sylibr 216 |
. 2
        ↾t       |
117 | 57, 116 | eqssd 3451 |
1
          ↾t      |