Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  tgpconcompeqg Structured version   Visualization version   Unicode version

Theorem tgpconcompeqg 21138
 Description: The connected component containing is the left coset of the identity component containing . (Contributed by Mario Carneiro, 17-Sep-2015.)
Hypotheses
Ref Expression
tgpconcomp.x
tgpconcomp.z
tgpconcomp.j
tgpconcomp.s t
tgpconcompeqg.r ~QG
Assertion
Ref Expression
tgpconcompeqg t
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem tgpconcompeqg
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfec2 7371 . . . . 5
21adantl 468 . . . 4
3 tgpconcomp.s . . . . . . . . 9 t
4 ssrab2 3516 . . . . . . . . . 10 t
5 sspwuni 4370 . . . . . . . . . 10 t t
64, 5mpbi 212 . . . . . . . . 9 t
73, 6eqsstri 3464 . . . . . . . 8
87a1i 11 . . . . . . 7
9 tgpconcomp.x . . . . . . . 8
10 eqid 2453 . . . . . . . 8
11 eqid 2453 . . . . . . . 8
12 tgpconcompeqg.r . . . . . . . 8 ~QG
139, 10, 11, 12eqgval 16878 . . . . . . 7
148, 13syldan 473 . . . . . 6
15 simp2 1010 . . . . . 6
1614, 15syl6bi 232 . . . . 5
1716abssdv 3505 . . . 4
182, 17eqsstrd 3468 . . 3
19 simpr 463 . . . . 5
20 tgpgrp 21105 . . . . . . 7
21 tgpconcomp.z . . . . . . . 8
229, 11, 21, 10grplinv 16724 . . . . . . 7
2320, 22sylan 474 . . . . . 6
24 tgpconcomp.j . . . . . . . . 9
2524, 9tgptopon 21109 . . . . . . . 8 TopOn
2625adantr 467 . . . . . . 7 TopOn
2720adantr 467 . . . . . . . 8
289, 21grpidcl 16706 . . . . . . . 8
2927, 28syl 17 . . . . . . 7
303concompid 20458 . . . . . . 7 TopOn
3126, 29, 30syl2anc 667 . . . . . 6
3223, 31eqeltrd 2531 . . . . 5
339, 10, 11, 12eqgval 16878 . . . . . 6
348, 33syldan 473 . . . . 5
3519, 19, 32, 34mpbir3and 1192 . . . 4
36 elecg 7407 . . . . 5
3719, 19, 36syl2anc 667 . . . 4
3835, 37mpbird 236 . . 3
399, 12, 11eqglact 16880 . . . . . . 7
407, 39mp3an2 1354 . . . . . 6
4120, 40sylan 474 . . . . 5
4241oveq2d 6311 . . . 4 t t
43 eqid 2453 . . . . 5
44 eqid 2453 . . . . . . 7
4544, 9, 11, 24tgplacthmeo 21130 . . . . . 6
46 hmeocn 20787 . . . . . 6
4745, 46syl 17 . . . . 5
48 toponuni 19954 . . . . . . 7 TopOn
4926, 48syl 17 . . . . . 6
507, 49syl5sseq 3482 . . . . 5
513concompcon 20459 . . . . . 6 TopOn t
5226, 29, 51syl2anc 667 . . . . 5 t
5343, 47, 50, 52conima 20452 . . . 4 t
5442, 53eqeltrd 2531 . . 3 t
55 eqid 2453 . . . 4 t t
5655concompss 20460 . . 3 t t
5718, 38, 54, 56syl3anc 1269 . 2 t
58 elpwi 3962 . . . . . 6
5944mptpreima 5331 . . . . . . . . . . . 12
60 ssrab2 3516 . . . . . . . . . . . 12
6159, 60eqsstri 3464 . . . . . . . . . . 11
6261a1i 11 . . . . . . . . . 10 t
6329adantr 467 . . . . . . . . . . 11 t
649, 11, 21grprid 16709 . . . . . . . . . . . . . 14
6520, 64sylan 474 . . . . . . . . . . . . 13
6665adantr 467 . . . . . . . . . . . 12 t
67 simprrl 775 . . . . . . . . . . . 12 t
6866, 67eqeltrd 2531 . . . . . . . . . . 11 t
69 oveq2 6303 . . . . . . . . . . . . 13
7069eleq1d 2515 . . . . . . . . . . . 12
7170, 59elrab2 3200 . . . . . . . . . . 11
7263, 68, 71sylanbrc 671 . . . . . . . . . 10 t
73 hmeocnvcn 20788 . . . . . . . . . . . . 13
7445, 73syl 17 . . . . . . . . . . . 12
7574adantr 467 . . . . . . . . . . 11 t
76 simprl 765 . . . . . . . . . . . 12 t
7749adantr 467 . . . . . . . . . . . 12 t
7876, 77sseqtrd 3470 . . . . . . . . . . 11 t
79 simprrr 776 . . . . . . . . . . 11 t t
8043, 75, 78, 79conima 20452 . . . . . . . . . 10 t t
813concompss 20460 . . . . . . . . . 10 t
8262, 72, 80, 81syl3anc 1269 . . . . . . . . 9 t
83 eqid 2453 . . . . . . . . . . . . . . . 16
8483, 9, 11, 10grplactcnv 16766 . . . . . . . . . . . . . . 15
8520, 84sylan 474 . . . . . . . . . . . . . 14
8685simpld 461 . . . . . . . . . . . . 13
8783, 9grplactfval 16764 . . . . . . . . . . . . . . 15
8887adantl 468 . . . . . . . . . . . . . 14
89 f1oeq1 5810 . . . . . . . . . . . . . 14
9088, 89syl 17 . . . . . . . . . . . . 13
9186, 90mpbid 214 . . . . . . . . . . . 12
9291adantr 467 . . . . . . . . . . 11 t
93 f1ocnv 5831 . . . . . . . . . . 11
94 f1ofun 5821 . . . . . . . . . . 11
9592, 93, 943syl 18 . . . . . . . . . 10 t
96 f1odm 5823 . . . . . . . . . . . 12
9792, 93, 963syl 18 . . . . . . . . . . 11 t
9876, 97sseqtr4d 3471 . . . . . . . . . 10 t
99 funimass3 6003 . . . . . . . . . 10
10095, 98, 99syl2anc 667 . . . . . . . . 9 t
10182, 100mpbid 214 . . . . . . . 8 t
10241adantr 467 . . . . . . . . 9 t
103 imacnvcnv 5303 . . . . . . . . 9
104102, 103syl6eqr 2505 . . . . . . . 8 t
105101, 104sseqtr4d 3471 . . . . . . 7 t
106105expr 620 . . . . . 6 t
10758, 106sylan2 477 . . . . 5 t
108107ralrimiva 2804 . . . 4 t
109 eleq2 2520 . . . . . 6
110 oveq2 6303 . . . . . . 7 t t
111110eleq1d 2515 . . . . . 6 t t
112109, 111anbi12d 718 . . . . 5 t t
113112ralrab 3202 . . . 4 t t
114108, 113sylibr 216 . . 3 t
115 unissb 4232 . . 3 t t
116114, 115sylibr 216 . 2 t
11757, 116eqssd 3451 1 t
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   w3a 986   wceq 1446   wcel 1889  cab 2439  wral 2739  crab 2743   wss 3406  cpw 3953  cuni 4201   class class class wbr 4405   cmpt 4464  ccnv 4836   cdm 4837  cima 4840   wfun 5579  wf1o 5584  cfv 5585  (class class class)co 6295  cec 7366  cbs 15133   cplusg 15202   ↾t crest 15331  ctopn 15332  c0g 15350  cgrp 16681  cminusg 16682   ~QG cqg 16825  TopOnctopon 19930   ccn 20252  ccon 20438  chmeo 20780  ctgp 21098 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-rep 4518  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-reu 2746  df-rmo 2747  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-uni 4202  df-int 4238  df-iun 4283  df-br 4406  df-opab 4465  df-mpt 4466  df-tr 4501  df-eprel 4748  df-id 4752  df-po 4758  df-so 4759  df-fr 4796  df-we 4798  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-pred 5383  df-ord 5429  df-on 5430  df-lim 5431  df-suc 5432  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-riota 6257  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6698  df-1st 6798  df-2nd 6799  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-oadd 7191  df-er 7368  df-ec 7370  df-map 7479  df-en 7575  df-fin 7578  df-fi 7930  df-rest 15333  df-0g 15352  df-topgen 15354  df-plusf 16499  df-mgm 16500  df-sgrp 16539  df-mnd 16549  df-grp 16685  df-minusg 16686  df-eqg 16828  df-top 19933  df-bases 19934  df-topon 19935  df-topsp 19936  df-cld 20046  df-cn 20255  df-cnp 20256  df-con 20439  df-tx 20589  df-hmeo 20782  df-tmd 21099  df-tgp 21100 This theorem is referenced by:  tgpconcomp  21139
 Copyright terms: Public domain W3C validator