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

Theorem pcophtb 21821
 Description: The path homotopy equivalence relation on two paths with the same start and end point can be written in terms of the loop formed by concatenating with the inverse of . Thus, all the homotopy information in is available if we restrict our attention to closed loops, as in the definition of the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015.)
Hypotheses
Ref Expression
pcophtb.h
pcophtb.p
pcophtb.f
pcophtb.g
pcophtb.0
pcophtb.1
Assertion
Ref Expression
pcophtb
Distinct variable groups:   ,   ,
Allowed substitution hints:   ()   ()   ()   ()

Proof of Theorem pcophtb
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 phtpcer 21787 . . . 4
21a1i 11 . . 3
3 pcophtb.1 . . . . . . . 8
4 pcophtb.g . . . . . . . . . 10
5 pcophtb.h . . . . . . . . . . 11
65pcorevcl 21817 . . . . . . . . . 10
74, 6syl 17 . . . . . . . . 9
87simp2d 1010 . . . . . . . 8
93, 8eqtr4d 2446 . . . . . . 7
107simp1d 1009 . . . . . . . 8
1110, 4pco0 21806 . . . . . . 7
129, 11eqtr4d 2446 . . . . . 6
1312adantr 463 . . . . 5
14 pcophtb.f . . . . . . 7
1514adantr 463 . . . . . 6
162, 15erref 7368 . . . . 5
17 eqid 2402 . . . . . . . 8
185, 17pcorev 21819 . . . . . . 7
194, 18syl 17 . . . . . 6
2019adantr 463 . . . . 5
2113, 16, 20pcohtpy 21812 . . . 4
223adantr 463 . . . . 5
2317pcopt2 21815 . . . . 5
2415, 22, 23syl2anc 659 . . . 4
252, 21, 24ertrd 7364 . . 3
2610adantr 463 . . . . . 6
274adantr 463 . . . . . 6
289adantr 463 . . . . . 6
297simp3d 1011 . . . . . . 7
3029adantr 463 . . . . . 6
31 eqid 2402 . . . . . 6
3215, 26, 27, 28, 30, 31pcoass 21816 . . . . 5
3314, 10pco1 21807 . . . . . . . 8
3433, 29eqtrd 2443 . . . . . . 7
3534adantr 463 . . . . . 6
36 simpr 459 . . . . . 6
372, 27erref 7368 . . . . . 6
3835, 36, 37pcohtpy 21812 . . . . 5
392, 32, 38ertr3d 7366 . . . 4
40 pcophtb.0 . . . . . . 7
4140adantr 463 . . . . . 6
4241eqcomd 2410 . . . . 5
43 pcophtb.p . . . . . 6
4443pcopt 21814 . . . . 5
4527, 42, 44syl2anc 659 . . . 4
462, 39, 45ertrd 7364 . . 3
472, 25, 46ertr3d 7366 . 2
481a1i 11 . . 3
499adantr 463 . . . 4
50 simpr 459 . . . 4
5110adantr 463 . . . . 5
5248, 51erref 7368 . . . 4
5349, 50, 52pcohtpy 21812 . . 3
54 eqid 2402 . . . . . . 7
555, 54pcorev2 21820 . . . . . 6
564, 55syl 17 . . . . 5
5740sneqd 3984 . . . . . . 7
5857xpeq2d 4847 . . . . . 6
5943, 58syl5eq 2455 . . . . 5
6056, 59breqtrrd 4421 . . . 4