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

Theorem pi1xfr 18657
 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 18486 . . . . . . 7 TopOn
32a1i 10 . . . . . 6 TopOn
4 pi1xfr.f . . . . . 6
5 cnf2 17085 . . . . . 6 TopOn TopOn
63, 1, 4, 5syl3anc 1182 . . . . 5
7 0elunit 10846 . . . . 5
8 ffvelrn 5746 . . . . 5
96, 7, 8sylancl 643 . . . 4
10 pi1xfr.p . . . . 5
1110pi1grp 18652 . . . 4 TopOn
121, 9, 11syl2anc 642 . . 3
13 1elunit 10847 . . . . 5
14 ffvelrn 5746 . . . . 5
156, 13, 14sylancl 643 . . . 4
16 pi1xfr.q . . . . 5
1716pi1grp 18652 . . . 4 TopOn
181, 15, 17syl2anc 642 . . 3
1912, 18jca 518 . 2
20 pi1xfr.b . . . 4
21 pi1xfr.g . . . 4
22 pi1xfr.i . . . . . . 7
2322pcorevcl 18627 . . . . . 6
244, 23syl 15 . . . . 5
2524simp1d 967 . . . 4
2624simp2d 968 . . . . 5
2726eqcomd 2363 . . . 4
2824simp3d 969 . . . 4
2910, 16, 20, 21, 1, 4, 25, 27, 28pi1xfrf 18655 . . 3
3020a1i 10 . . . . . . . 8
3110, 1, 9, 30pi1bas2 18643 . . . . . . 7
3231eleq2d 2425 . . . . . 6
3332biimpa 470 . . . . 5
34 eqid 2358 . . . . . 6
35 oveq1 5952 . . . . . . . . 9
3635fveq2d 5612 . . . . . . . 8
37 fveq2 5608 . . . . . . . . 9
3837oveq1d 5960 . . . . . . . 8
3936, 38eqeq12d 2372 . . . . . . 7
4039ralbidv 2639 . . . . . 6
4131eleq2d 2425 . . . . . . . . . 10
4241biimpa 470 . . . . . . . . 9
4342adantlr 695 . . . . . . . 8
44 oveq2 5953 . . . . . . . . . . 11
4544fveq2d 5612 . . . . . . . . . 10
46 fveq2 5608 . . . . . . . . . . 11
4746oveq2d 5961 . . . . . . . . . 10
4845, 47eqeq12d 2372 . . . . . . . . 9
49 phtpcer 18597 . . . . . . . . . . . . . 14
5049a1i 10 . . . . . . . . . . . . 13
5110, 1, 9, 30pi1eluni 18644 . . . . . . . . . . . . . . . . . . . . 21
5251biimpa 470 . . . . . . . . . . . . . . . . . . . 20
5352simp1d 967 . . . . . . . . . . . . . . . . . . 19
54533adant3 975 . . . . . . . . . . . . . . . . . 18
5510, 1, 9, 30pi1eluni 18644 . . . . . . . . . . . . . . . . . . . . 21
5655adantr 451 . . . . . . . . . . . . . . . . . . . 20
5756biimp3a 1281 . . . . . . . . . . . . . . . . . . 19
5857simp1d 967 . . . . . . . . . . . . . . . . . 18
5954, 58pco0 18616 . . . . . . . . . . . . . . . . 17
6052simp2d 968 . . . . . . . . . . . . . . . . . 18
61603adant3 975 . . . . . . . . . . . . . . . . 17
6259, 61eqtrd 2390 . . . . . . . . . . . . . . . 16
6352simp3d 969 . . . . . . . . . . . . . . . . . . . 20
64633adant3 975 . . . . . . . . . . . . . . . . . . 19
6557simp2d 968 . . . . . . . . . . . . . . . . . . 19
6664, 65eqtr4d 2393 . . . . . . . . . . . . . . . . . 18
6754, 58, 66pcocn 18619 . . . . . . . . . . . . . . . . 17
684adantr 451 . . . . . . . . . . . . . . . . . 18
69683adant3 975 . . . . . . . . . . . . . . . . 17
7067, 69pco0 18616 . . . . . . . . . . . . . . . 16
71283ad2ant1 976 . . . . . . . . . . . . . . . 16
7262, 70, 713eqtr4rd 2401 . . . . . . . . . . . . . . 15
73 simp1 955 . . . . . . . . . . . . . . . . 17
7473, 25syl 15 . . . . . . . . . . . . . . . 16
7550, 74erref 6767 . . . . . . . . . . . . . . 15
7657simp3d 969 . . . . . . . . . . . . . . . . 17
77 eqid 2358 . . . . . . . . . . . . . . . . 17
7854, 58, 69, 66, 76, 77pcoass 18626 . . . . . . . . . . . . . . . 16
7958, 69pco0 18616 . . . . . . . . . . . . . . . . . . 19
8066, 79eqtr4d 2393 . . . . . . . . . . . . . . . . . 18
8150, 54erref 6767 . . . . . . . . . . . . . . . . . 18
8269, 74pco1 18617 . . . . . . . . . . . . . . . . . . . . . 22
8365, 79, 713eqtr4rd 2401 . . . . . . . . . . . . . . . . . . . . . 22
8482, 83eqtrd 2390 . . . . . . . . . . . . . . . . . . . . 21
85 eqid 2358 . . . . . . . . . . . . . . . . . . . . . . 23
8622, 85pcorev2 18630 . . . . . . . . . . . . . . . . . . . . . 22
8769, 86syl 15 . . . . . . . . . . . . . . . . . . . . 21
8858, 69, 76pcocn 18619 . . . . . . . . . . . . . . . . . . . . . 22
8950, 88erref 6767 . . . . . . . . . . . . . . . . . . . . 21
9084, 87, 89pcohtpy 18622 . . . . . . . . . . . . . . . . . . . 20
9179, 65eqtrd 2390 . . . . . . . . . . . . . . . . . . . . 21
9285pcopt 18624 . . . . . . . . . . . . . . . . . . . . 21
9388, 91, 92syl2anc 642 . . . . . . . . . . . . . . . . . . . 20
9450, 90, 93ertrd 6763 . . . . . . . . . . . . . . . . . . 19
9573, 26syl 15 . . . . . . . . . . . . . . . . . . . . 21
9695eqcomd 2363 . . . . . . . . . . . . . . . . . . . 20
9769, 74, 88, 96, 83, 77pcoass 18626 . . . . . . . . . . . . . . . . . . 19
9850, 94, 97ertr3d 6765 . . . . . . . . . . . . . . . . . 18
9980, 81, 98pcohtpy 18622 . . . . . . . . . . . . . . . . 17
10074, 88, 83pcocn 18619 . . . . . . . . . . . . . . . . . 18
10174, 88pco0 18616 . . . . . . . . . . . . . . . . . . . 20
102101, 95eqtrd 2390 . . . . . . . . . . . . . . . . . . 19
103102eqcomd 2363 . . . . . . . . . . . . . . . . . 18
10454, 69, 100, 64, 103, 77pcoass 18626 . . . . . . . . . . . . . . . . 17
10550, 99, 104ertr4d 6766 . . . . . . . . . . . . . . . 16
10650, 78, 105ertrd 6763 . . . . . . . . . . . . . . 15
10772, 75, 106pcohtpy 18622 . . . . . . . . . . . . . 14
10853, 68, 63pcocn 18619 . . . . . . . . . . . . . . . 16
1091083adant3 975 . . . . . . . . . . . . . . 15
11053, 68pco0 18616 . . . . . . . . . . . . . . . . 17
11128adantr 451 . . . . . . . . . . . . . . . . 17
11260, 110, 1113eqtr4rd 2401 . . . . . . . . . . . . . . . 16
1131123adant3 975 . . . . . . . . . . . . . . 15
11454, 69pco1 18617 . . . . . . . . . . . . . . . 16
115114, 102eqtr4d 2393 . . . . . . . . . . . . . . 15
11674, 109, 100, 113, 115, 77pcoass 18626 . . . . . . . . . . . . . 14
11750, 107, 116ertr4d 6766 . . . . . . . . . . . . 13
11850, 117erthi 6793 . . . . . . . . . . . 12
1191adantr 451 . . . . . . . . . . . . . 14 TopOn
1201193adant3 975 . . . . . . . . . . . . 13 TopOn
12125adantr 451 . . . . . . . . . . . . . 14
1221213adant3 975 . . . . . . . . . . . . 13
1231113adant3 975 . . . . . . . . . . . . 13
12454, 58pco1 18617 . . . . . . . . . . . . . . 15
125124, 76eqtrd 2390 . . . . . . . . . . . . . 14
12610, 1, 9, 30pi1eluni 18644 . . . . . . . . . . . . . . 15
1271263ad2ant1 976 . . . . . . . . . . . . . 14
12867, 62, 125, 127mpbir3and 1135 . . . . . . . . . . . . 13
12910, 16, 20, 21, 120, 69, 122, 96, 123, 128pi1xfrval 18656 . . . . . . . . . . . 12
130 eqid 2358 . . . . . . . . . . . . 13
13113ad2ant1 976 . . . . . . . . . . . . 13 TopOn
13273, 15syl 15 . . . . . . . . . . . . 13
133 eqid 2358 . . . . . . . . . . . . 13
134121, 108, 112pcocn 18619 . . . . . . . . . . . . . . 15
1351343adant3 975 . . . . . . . . . . . . . 14
136121, 108pco0 18616 . . . . . . . . . . . . . . . 16
13726adantr 451 . . . . . . . . . . . . . . . 16
138136, 137eqtrd 2390 . . . . . . . . . . . . . . 15
1391383adant3 975 . . . . . . . . . . . . . 14
140121, 108pco1 18617 . . . . . . . . . . . . . . . 16
14153, 68pco1 18617 . . . . . . . . . . . . . . . 16
142140, 141eqtrd 2390 . . . . . . . . . . . . . . 15
1431423adant3 975 . . . . . . . . . . . . . 14
144 eqidd 2359 . . . . . . . . . . . . . . 15
14516, 131, 132, 144pi1eluni 18644 . . . . . . . . . . . . . 14
146135, 139, 143, 145mpbir3and 1135 . . . . . . . . . . . . 13
14774, 88pco1 18617 . . . . . . . . . . . . . . 15
14858, 69pco1 18617 . . . . . . . . . . . . . . 15
149147, 148eqtrd 2390 . . . . . . . . . . . . . 14
15016, 131, 132, 144pi1eluni 18644 . . . . . . . . . . . . . 14
151100, 102, 149, 150mpbir3and 1135 . . . . . . . . . . . . 13
15216, 130, 131, 132, 133, 146, 151pi1addval 18650 . . . . . . . . . . . 12
153118, 129, 1523eqtr4d 2400 . . . . . . . . . . 11
15473, 9syl 15 . . . . . . . . . . . . 13
155 eqid 2358 . . . . . . . . . . . . 13
156 simp2 956 . . . . . . . . . . . . 13
157 simp3 957 . . . . . . . . . . . . 13
15810, 20, 131, 154, 155, 156, 157pi1addval 18650 . . . . . . . . . . . 12
159158fveq2d 5612 . . . . . . . . . . 11
16027adantr 451 . . . . . . . . . . . . . 14
161 simpr 447 . . . . . . . . . . . . . 14
16210, 16, 20, 21, 119, 68, 121, 160, 111, 161pi1xfrval 18656 . . . . . . . . . . . . 13
1631623adant3 975 . . . . . . . . . . . 12
16410, 16, 20, 21, 120, 69, 122, 96, 123, 157pi1xfrval 18656 . . . . . . . . . . . 12
165163, 164oveq12d 5963 . . . . . . . . . . 11
166153, 159, 1653eqtr4d 2400 . . . . . . . . . 10
1671663expa 1151 . . . . . . . . 9
16834, 48, 167ectocld 6813 . . . . . . . 8
16943, 168syldan 456 . . . . . . 7
170169ralrimiva 2702 . . . . . 6
17134, 40, 170ectocld 6813 . . . . 5
17233, 171syldan 456 . . . 4
173172ralrimiva 2702 . . 3
17429, 173jca 518 . 2
17520, 130, 155, 133isghm 14782 . 2
17619, 174, 175sylanbrc 645 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934   wceq 1642   wcel 1710  wral 2619  cif 3641  csn 3716  cop 3719  cuni 3908   class class class wbr 4104   cmpt 4158   cxp 4769   crn 4772  wf 5333  cfv 5337  (class class class)co 5945   wer 6744  cec 6745  cqs 6746  cc0 8827  c1 8828   caddc 8830   cmul 8832   cle 8958   cmin 9127   cdiv 9513  c2 9885  c4 9887  cicc 10751  cbs 13245   cplusg 13305  cgrp 14461   cghm 14779  TopOnctopon 16738   ccn 17060  cii 18482   cphtpc 18571  cpco 18602   cpi1 18605 This theorem is referenced by:  pi1xfrcnv  18659  pi1xfrgim  18660 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-rep 4212  ax-sep 4222  ax-nul 4230  ax-pow 4269  ax-pr 4295  ax-un 4594  ax-inf2 7432  ax-cnex 8883  ax-resscn 8884  ax-1cn 8885  ax-icn 8886  ax-addcl 8887  ax-addrcl 8888  ax-mulcl 8889  ax-mulrcl 8890  ax-mulcom 8891  ax-addass 8892  ax-mulass 8893  ax-distr 8894  ax-i2m1 8895  ax-1ne0 8896  ax-1rid 8897  ax-rnegex 8898  ax-rrecex 8899  ax-cnre 8900  ax-pre-lttri 8901  ax-pre-lttrn 8902  ax-pre-ltadd 8903  ax-pre-mulgt0 8904  ax-pre-sup 8905  ax-addf 8906  ax-mulf 8907 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-nel 2524  df-ral 2624  df-rex 2625  df-reu 2626  df-rmo 2627  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3909  df-int 3944  df-iun 3988  df-iin 3989  df-br 4105  df-opab 4159  df-mpt 4160  df-tr 4195  df-eprel 4387  df-id 4391  df-po 4396  df-so 4397  df-fr 4434  df-se 4435  df-we 4436  df-ord 4477  df-on 4478  df-lim 4479  df-suc 4480  df-om 4739  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-res 4783  df-ima 4784  df-iota 5301  df-fun 5339  df-fn 5340  df-f 5341  df-f1 5342  df-fo 5343  df-f1o 5344  df-fv 5345  df-isom 5346  df-ov 5948  df-oprab 5949  df-mpt2 5950  df-of 6165  df-1st 6209  df-2nd 6210  df-riota 6391  df-recs 6475  df-rdg 6510  df-1o 6566  df-2o 6567  df-oadd 6570  df-er 6747  df-ec 6749  df-qs 6753  df-map 6862  df-ixp 6906  df-en 6952  df-dom 6953  df-sdom 6954  df-fin 6955  df-fi 7255  df-sup 7284  df-oi 7315  df-card 7662  df-cda 7884  df-pnf 8959  df-mnf 8960  df-xr 8961  df-ltxr 8962  df-le 8963  df-sub 9129  df-neg 9130  df-div 9514  df-nn 9837  df-2 9894  df-3 9895  df-4 9896  df-5 9897  df-6 9898  df-7 9899  df-8 9900  df-9 9901  df-10 9902  df-n0 10058  df-z 10117  df-dec 10217  df-uz 10323  df-q 10409  df-rp 10447  df-xneg 10544  df-xadd 10545  df-xmul 10546  df-ioo 10752  df-icc 10755  df-fz 10875  df-fzo 10963  df-seq 11139  df-exp 11198  df-hash 11431  df-cj 11680  df-re 11681  df-im 11682  df-sqr 11816  df-abs 11817  df-struct 13247  df-ndx 13248  df-slot 13249  df-base 13250  df-sets 13251  df-ress 13252  df-plusg 13318  df-mulr 13319  df-starv 13320  df-sca 13321  df-vsca 13322  df-tset 13324  df-ple 13325  df-ds 13327  df-unif 13328  df-hom 13329  df-cco 13330  df-rest 13426  df-topn 13427  df-topgen 13443  df-pt 13444  df-prds 13447  df-xrs 13502  df-0g 13503  df-gsum 13504  df-qtop 13509  df-imas 13510  df-divs 13511  df-xps 13512  df-mre 13587  df-mrc 13588  df-acs 13590  df-mnd 14466  df-submnd 14515  df-grp 14588  df-mulg 14591  df-ghm 14780  df-cntz 14892  df-cmn 15190  df-xmet 16475  df-met 16476  df-bl 16477  df-mopn 16478  df-cnfld 16483  df-top 16742  df-bases 16744  df-topon 16745  df-topsp 16746  df-cld 16862  df-cn 17063  df-cnp 17064  df-tx 17363  df-hmeo 17552  df-xms 17987  df-ms 17988  df-tms 17989  df-ii 18484  df-htpy 18572  df-phtpy 18573  df-phtpc 18594  df-pco 18607  df-om1 18608  df-pi1 18610
 Copyright terms: Public domain W3C validator