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

Theorem pi1xfr 22078
 Description: Given a path and its inverse between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015.)
Hypotheses
Ref Expression
pi1xfr.p
pi1xfr.q
pi1xfr.b
pi1xfr.g
pi1xfr.j TopOn
pi1xfr.f
pi1xfr.i
Assertion
Ref Expression
pi1xfr
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,)

Proof of Theorem pi1xfr
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pi1xfr.j . . . 4 TopOn
2 iitopon 21903 . . . . . . 7 TopOn
32a1i 11 . . . . . 6 TopOn
4 pi1xfr.f . . . . . 6
5 cnf2 20257 . . . . . 6 TopOn TopOn
63, 1, 4, 5syl3anc 1265 . . . . 5
7 0elunit 11752 . . . . 5
8 ffvelrn 6033 . . . . 5
96, 7, 8sylancl 667 . . . 4
10 pi1xfr.p . . . . 5
1110pi1grp 22073 . . . 4 TopOn
121, 9, 11syl2anc 666 . . 3
13 1elunit 11753 . . . . 5
14 ffvelrn 6033 . . . . 5
156, 13, 14sylancl 667 . . . 4
16 pi1xfr.q . . . . 5
1716pi1grp 22073 . . . 4 TopOn
181, 15, 17syl2anc 666 . . 3
1912, 18jca 535 . 2
20 pi1xfr.b . . . 4
21 pi1xfr.g . . . 4
22 pi1xfr.i . . . . . . 7
2322pcorevcl 22048 . . . . . 6
244, 23syl 17 . . . . 5
2524simp1d 1018 . . . 4
2624simp2d 1019 . . . . 5
2726eqcomd 2431 . . . 4
2824simp3d 1020 . . . 4
2910, 16, 20, 21, 1, 4, 25, 27, 28pi1xfrf 22076 . . 3
3020a1i 11 . . . . . . . 8
3110, 1, 9, 30pi1bas2 22064 . . . . . . 7
3231eleq2d 2493 . . . . . 6
3332biimpa 487 . . . . 5
34 eqid 2423 . . . . . 6
35 oveq1 6310 . . . . . . . . 9
3635fveq2d 5883 . . . . . . . 8
37 fveq2 5879 . . . . . . . . 9
3837oveq1d 6318 . . . . . . . 8
3936, 38eqeq12d 2445 . . . . . . 7
4039ralbidv 2865 . . . . . 6
4131eleq2d 2493 . . . . . . . . . 10
4241biimpa 487 . . . . . . . . 9
4342adantlr 720 . . . . . . . 8
44 oveq2 6311 . . . . . . . . . . 11
4544fveq2d 5883 . . . . . . . . . 10
46 fveq2 5879 . . . . . . . . . . 11
4746oveq2d 6319 . . . . . . . . . 10
4845, 47eqeq12d 2445 . . . . . . . . 9
49 phtpcer 22018 . . . . . . . . . . . . . 14
5049a1i 11 . . . . . . . . . . . . 13
5110, 1, 9, 30pi1eluni 22065 . . . . . . . . . . . . . . . . . . . . 21
5251biimpa 487 . . . . . . . . . . . . . . . . . . . 20
5352simp1d 1018 . . . . . . . . . . . . . . . . . . 19
54533adant3 1026 . . . . . . . . . . . . . . . . . 18
5510, 1, 9, 30pi1eluni 22065 . . . . . . . . . . . . . . . . . . . . 21
5655adantr 467 . . . . . . . . . . . . . . . . . . . 20
5756biimp3a 1365 . . . . . . . . . . . . . . . . . . 19
5857simp1d 1018 . . . . . . . . . . . . . . . . . 18
5954, 58pco0 22037 . . . . . . . . . . . . . . . . 17
6052simp2d 1019 . . . . . . . . . . . . . . . . . 18
61603adant3 1026 . . . . . . . . . . . . . . . . 17
6259, 61eqtrd 2464 . . . . . . . . . . . . . . . 16
6352simp3d 1020 . . . . . . . . . . . . . . . . . . . 20
64633adant3 1026 . . . . . . . . . . . . . . . . . . 19
6557simp2d 1019 . . . . . . . . . . . . . . . . . . 19
6664, 65eqtr4d 2467 . . . . . . . . . . . . . . . . . 18
6754, 58, 66pcocn 22040 . . . . . . . . . . . . . . . . 17
6843ad2ant1 1027 . . . . . . . . . . . . . . . . 17
6967, 68pco0 22037 . . . . . . . . . . . . . . . 16
70283ad2ant1 1027 . . . . . . . . . . . . . . . 16
7162, 69, 703eqtr4rd 2475 . . . . . . . . . . . . . . 15
72253ad2ant1 1027 . . . . . . . . . . . . . . . 16
7350, 72erref 7389 . . . . . . . . . . . . . . 15
7457simp3d 1020 . . . . . . . . . . . . . . . . 17
75 eqid 2423 . . . . . . . . . . . . . . . . 17
7654, 58, 68, 66, 74, 75pcoass 22047 . . . . . . . . . . . . . . . 16
7758, 68pco0 22037 . . . . . . . . . . . . . . . . . . 19
7866, 77eqtr4d 2467 . . . . . . . . . . . . . . . . . 18
7950, 54erref 7389 . . . . . . . . . . . . . . . . . 18
8068, 72pco1 22038 . . . . . . . . . . . . . . . . . . . . . 22
8165, 77, 703eqtr4rd 2475 . . . . . . . . . . . . . . . . . . . . . 22
8280, 81eqtrd 2464 . . . . . . . . . . . . . . . . . . . . 21
83 eqid 2423 . . . . . . . . . . . . . . . . . . . . . . 23
8422, 83pcorev2 22051 . . . . . . . . . . . . . . . . . . . . . 22
8568, 84syl 17 . . . . . . . . . . . . . . . . . . . . 21
8658, 68, 74pcocn 22040 . . . . . . . . . . . . . . . . . . . . . 22
8750, 86erref 7389 . . . . . . . . . . . . . . . . . . . . 21
8882, 85, 87pcohtpy 22043 . . . . . . . . . . . . . . . . . . . 20
8977, 65eqtrd 2464 . . . . . . . . . . . . . . . . . . . . 21
9083pcopt 22045 . . . . . . . . . . . . . . . . . . . . 21
9186, 89, 90syl2anc 666 . . . . . . . . . . . . . . . . . . . 20
9250, 88, 91ertrd 7385 . . . . . . . . . . . . . . . . . . 19
93263ad2ant1 1027 . . . . . . . . . . . . . . . . . . . . 21
9493eqcomd 2431 . . . . . . . . . . . . . . . . . . . 20
9568, 72, 86, 94, 81, 75pcoass 22047 . . . . . . . . . . . . . . . . . . 19
9650, 92, 95ertr3d 7387 . . . . . . . . . . . . . . . . . 18
9778, 79, 96pcohtpy 22043 . . . . . . . . . . . . . . . . 17
9872, 86, 81pcocn 22040 . . . . . . . . . . . . . . . . . 18
9972, 86pco0 22037 . . . . . . . . . . . . . . . . . . . 20
10099, 93eqtrd 2464 . . . . . . . . . . . . . . . . . . 19
101100eqcomd 2431 . . . . . . . . . . . . . . . . . 18
10254, 68, 98, 64, 101, 75pcoass 22047 . . . . . . . . . . . . . . . . 17
10350, 97, 102ertr4d 7388 . . . . . . . . . . . . . . . 16
10450, 76, 103ertrd 7385 . . . . . . . . . . . . . . 15
10571, 73, 104pcohtpy 22043 . . . . . . . . . . . . . 14
1064adantr 467 . . . . . . . . . . . . . . . . 17
10753, 106, 63pcocn 22040 . . . . . . . . . . . . . . . 16
1081073adant3 1026 . . . . . . . . . . . . . . 15
10953, 106pco0 22037 . . . . . . . . . . . . . . . . 17
11028adantr 467 . . . . . . . . . . . . . . . . 17
11160, 109, 1103eqtr4rd 2475 . . . . . . . . . . . . . . . 16
1121113adant3 1026 . . . . . . . . . . . . . . 15
11354, 68pco1 22038 . . . . . . . . . . . . . . . 16
114113, 100eqtr4d 2467 . . . . . . . . . . . . . . 15
11572, 108, 98, 112, 114, 75pcoass 22047 . . . . . . . . . . . . . 14
11650, 105, 115ertr4d 7388 . . . . . . . . . . . . 13
11750, 116erthi 7416 . . . . . . . . . . . 12
11813ad2ant1 1027 . . . . . . . . . . . . 13 TopOn
11954, 58pco1 22038 . . . . . . . . . . . . . . 15
120119, 74eqtrd 2464 . . . . . . . . . . . . . 14
12110, 1, 9, 30pi1eluni 22065 . . . . . . . . . . . . . . 15
1221213ad2ant1 1027 . . . . . . . . . . . . . 14
12367, 62, 120, 122mpbir3and 1189 . . . . . . . . . . . . 13
12410, 16, 20, 21, 118, 68, 72, 94, 70, 123pi1xfrval 22077 . . . . . . . . . . . 12
125 eqid 2423 . . . . . . . . . . . . 13
126153ad2ant1 1027 . . . . . . . . . . . . 13
127 eqid 2423 . . . . . . . . . . . . 13
12825adantr 467 . . . . . . . . . . . . . . . 16
129128, 107, 111pcocn 22040 . . . . . . . . . . . . . . 15
1301293adant3 1026 . . . . . . . . . . . . . 14
131128, 107pco0 22037 . . . . . . . . . . . . . . . 16
13226adantr 467 . . . . . . . . . . . . . . . 16
133131, 132eqtrd 2464 . . . . . . . . . . . . . . 15
1341333adant3 1026 . . . . . . . . . . . . . 14
135128, 107pco1 22038 . . . . . . . . . . . . . . . 16
13653, 106pco1 22038 . . . . . . . . . . . . . . . 16
137135, 136eqtrd 2464 . . . . . . . . . . . . . . 15
1381373adant3 1026 . . . . . . . . . . . . . 14
139 eqidd 2424 . . . . . . . . . . . . . . 15
14016, 118, 126, 139pi1eluni 22065 . . . . . . . . . . . . . 14
141130, 134, 138, 140mpbir3and 1189 . . . . . . . . . . . . 13
14272, 86pco1 22038 . . . . . . . . . . . . . . 15
14358, 68pco1 22038 . . . . . . . . . . . . . . 15
144142, 143eqtrd 2464 . . . . . . . . . . . . . 14
14516, 118, 126, 139pi1eluni 22065 . . . . . . . . . . . . . 14
14698, 100, 144, 145mpbir3and 1189 . . . . . . . . . . . . 13
14716, 125, 118, 126, 127, 141, 146pi1addval 22071 . . . . . . . . . . . 12
148117, 124, 1473eqtr4d 2474 . . . . . . . . . . 11
14993ad2ant1 1027 . . . . . . . . . . . . 13
150 eqid 2423 . . . . . . . . . . . . 13
151 simp2 1007 . . . . . . . . . . . . 13
152 simp3 1008 . . . . . . . . . . . . 13
15310, 20, 118, 149, 150, 151, 152pi1addval 22071 . . . . . . . . . . . 12
154153fveq2d 5883 . . . . . . . . . . 11
1551adantr 467 . . . . . . . . . . . . . 14 TopOn
15627adantr 467 . . . . . . . . . . . . . 14
157 simpr 463 . . . . . . . . . . . . . 14
15810, 16, 20, 21, 155, 106, 128, 156, 110, 157pi1xfrval 22077 . . . . . . . . . . . . 13
1591583adant3 1026 . . . . . . . . . . . 12
16010, 16, 20, 21, 118, 68, 72, 94, 70, 152pi1xfrval 22077 . . . . . . . . . . . 12
161159, 160oveq12d 6321 . . . . . . . . . . 11
162148, 154, 1613eqtr4d 2474 . . . . . . . . . 10
1631623expa 1206 . . . . . . . . 9
16434, 48, 163ectocld 7436 . . . . . . . 8
16543, 164syldan 473 . . . . . . 7
166165ralrimiva 2840 . . . . . 6
16734, 40, 166ectocld 7436 . . . . 5
16833, 167syldan 473 . . . 4
169168ralrimiva 2840 . . 3
17029, 169jca 535 . 2
17120, 125, 150, 127isghm 16876 . 2
17219, 170, 171sylanbrc 669 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   w3a 983   wceq 1438   wcel 1869  wral 2776  cif 3910  csn 3997  cop 4003  cuni 4217   class class class wbr 4421   cmpt 4480   cxp 4849   crn 4852  wf 5595  cfv 5599  (class class class)co 6303   wer 7366  cec 7367  cqs 7368  cc0 9541  c1 9542   caddc 9544   cmul 9546   cle 9678   cmin 9862   cdiv 10271  c2 10661  c4 10663  cicc 11640  cbs 15114   cplusg 15183  cgrp 16662   cghm 16873  TopOnctopon 19910   ccn 20232  cii 21899   cphtpc 21992  cpco 22023   cpi1 22026 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4534  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595  ax-inf2 8150  ax-cnex 9597  ax-resscn 9598  ax-1cn 9599  ax-icn 9600  ax-addcl 9601  ax-addrcl 9602  ax-mulcl 9603  ax-mulrcl 9604  ax-mulcom 9605  ax-addass 9606  ax-mulass 9607  ax-distr 9608  ax-i2m1 9609  ax-1ne0 9610  ax-1rid 9611  ax-rnegex 9612  ax-rrecex 9613  ax-cnre 9614  ax-pre-lttri 9615  ax-pre-lttrn 9616  ax-pre-ltadd 9617  ax-pre-mulgt0 9618  ax-pre-sup 9619  ax-addf 9620  ax-mulf 9621 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-int 4254  df-iun 4299  df-iin 4300  df-br 4422  df-opab 4481  df-mpt 4482  df-tr 4517  df-eprel 4762  df-id 4766  df-po 4772  df-so 4773  df-fr 4810  df-se 4811  df-we 4812  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-pred 5397  df-ord 5443  df-on 5444  df-lim 5445  df-suc 5446  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-isom 5608  df-riota 6265  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-of 6543  df-om 6705  df-1st 6805  df-2nd 6806  df-supp 6924  df-wrecs 7034  df-recs 7096  df-rdg 7134  df-1o 7188  df-2o 7189  df-oadd 7192  df-er 7369  df-ec 7371  df-qs 7375  df-map 7480  df-ixp 7529  df-en 7576  df-dom 7577  df-sdom 7578  df-fin 7579  df-fsupp 7888  df-fi 7929  df-sup 7960  df-inf 7961  df-oi 8029  df-card 8376  df-cda 8600  df-pnf 9679  df-mnf 9680  df-xr 9681  df-ltxr 9682  df-le 9683  df-sub 9864  df-neg 9865  df-div 10272  df-nn 10612  df-2 10670  df-3 10671  df-4 10672  df-5 10673  df-6 10674  df-7 10675  df-8 10676  df-9 10677  df-10 10678  df-n0 10872  df-z 10940  df-dec 11054  df-uz 11162  df-q 11267  df-rp 11305  df-xneg 11411  df-xadd 11412  df-xmul 11413  df-ioo 11641  df-icc 11644  df-fz 11787  df-fzo 11918  df-seq 12215  df-exp 12274  df-hash 12517  df-cj 13156  df-re 13157  df-im 13158  df-sqrt 13292  df-abs 13293  df-struct 15116  df-ndx 15117  df-slot 15118  df-base 15119  df-sets 15120  df-ress 15121  df-plusg 15196  df-mulr 15197  df-starv 15198  df-sca 15199  df-vsca 15200  df-ip 15201  df-tset 15202  df-ple 15203  df-ds 15205  df-unif 15206  df-hom 15207  df-cco 15208  df-rest 15314  df-topn 15315  df-0g 15333  df-gsum 15334  df-topgen 15335  df-pt 15336  df-prds 15339  df-xrs 15393  df-qtop 15399  df-imas 15400  df-qus 15402  df-xps 15403  df-mre 15485  df-mrc 15486  df-acs 15488  df-mgm 16481  df-sgrp 16520  df-mnd 16530  df-submnd 16576  df-grp 16666  df-mulg 16669  df-ghm 16874  df-cntz 16964  df-cmn 17425  df-psmet 18955  df-xmet 18956  df-met 18957  df-bl 18958  df-mopn 18959  df-cnfld 18964  df-top 19913  df-bases 19914  df-topon 19915  df-topsp 19916  df-cld 20026  df-cn 20235  df-cnp 20236  df-tx 20569  df-hmeo 20762  df-xms 21327  df-ms 21328  df-tms 21329  df-ii 21901  df-htpy 21993  df-phtpy 21994  df-phtpc 22015  df-pco 22028  df-om1 22029  df-pi1 22031 This theorem is referenced by:  pi1xfrcnv  22080  pi1xfrgim  22081
 Copyright terms: Public domain W3C validator