Metamath Proof Explorer

Theorem pi1xfrf

Description: Functionality of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 23-Dec-2016)

Ref Expression
Hypotheses pi1xfr.p ⊢ 𝑃 = ( 𝐽 π1 ( 𝐹 ‘ 0 ) )
pi1xfr.q ⊢ 𝑄 = ( 𝐽 π1 ( 𝐹 ‘ 1 ) )
pi1xfr.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
pi1xfr.g ⊢ 𝐺 = ran ( 𝑔 ∈ ∪ 𝐵 ↦ ⟨ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ )
pi1xfr.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
pi1xfr.f ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
pi1xfrval.i ⊢ ( 𝜑 → 𝐼 ∈ ( II Cn 𝐽 ) )
pi1xfrval.1 ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐼 ‘ 0 ) )
pi1xfrval.2 ⊢ ( 𝜑 → ( 𝐼 ‘ 1 ) = ( 𝐹 ‘ 0 ) )
Assertion pi1xfrf ( 𝜑 → 𝐺 : 𝐵 ⟶ ( Base ‘ 𝑄 ) )

Proof

Step Hyp Ref Expression
1 pi1xfr.p ⊢ 𝑃 = ( 𝐽 π1 ( 𝐹 ‘ 0 ) )
2 pi1xfr.q ⊢ 𝑄 = ( 𝐽 π1 ( 𝐹 ‘ 1 ) )
3 pi1xfr.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
4 pi1xfr.g ⊢ 𝐺 = ran ( 𝑔 ∈ ∪ 𝐵 ↦ ⟨ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ )
5 pi1xfr.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
6 pi1xfr.f ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
7 pi1xfrval.i ⊢ ( 𝜑 → 𝐼 ∈ ( II Cn 𝐽 ) )
8 pi1xfrval.1 ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐼 ‘ 0 ) )
9 pi1xfrval.2 ⊢ ( 𝜑 → ( 𝐼 ‘ 1 ) = ( 𝐹 ‘ 0 ) )
10 5 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
11 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
12 cnf2 ⊢ ( ( II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( II Cn 𝐽 ) ) → 𝐹 : ( 0 [,] 1 ) ⟶ 𝑋 )
13 11 5 6 12 mp3an2i ⊢ ( 𝜑 → 𝐹 : ( 0 [,] 1 ) ⟶ 𝑋 )
14 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
15 ffvelcdm ⊢ ( ( 𝐹 : ( 0 [,] 1 ) ⟶ 𝑋 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ 0 ) ∈ 𝑋 )
16 13 14 15 sylancl ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) ∈ 𝑋 )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝐹 ‘ 0 ) ∈ 𝑋 )
18 3 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑃 ) )
19 1 5 16 18 pi1eluni ⊢ ( 𝜑 → ( 𝑔 ∈ ∪ 𝐵 ↔ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( 𝑔 ‘ 0 ) = ( 𝐹 ‘ 0 ) ∧ ( 𝑔 ‘ 1 ) = ( 𝐹 ‘ 0 ) ) ) )
20 19 biimpa ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( 𝑔 ‘ 0 ) = ( 𝐹 ‘ 0 ) ∧ ( 𝑔 ‘ 1 ) = ( 𝐹 ‘ 0 ) ) )
21 20 simp1d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → 𝑔 ∈ ( II Cn 𝐽 ) )
22 20 simp2d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝑔 ‘ 0 ) = ( 𝐹 ‘ 0 ) )
23 20 simp3d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝑔 ‘ 1 ) = ( 𝐹 ‘ 0 ) )
24 1 3 10 17 21 22 23 elpi1i ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ∈ 𝐵 )
25 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
26 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
27 ffvelcdm ⊢ ( ( 𝐹 : ( 0 [,] 1 ) ⟶ 𝑋 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ 1 ) ∈ 𝑋 )
28 13 26 27 sylancl ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) ∈ 𝑋 )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝐹 ‘ 1 ) ∈ 𝑋 )
30 7 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → 𝐼 ∈ ( II Cn 𝐽 ) )
31 6 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → 𝐹 ∈ ( II Cn 𝐽 ) )
32 21 31 23 pcocn ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ∈ ( II Cn 𝐽 ) )
33 21 31 pco0 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ‘ 0 ) = ( 𝑔 ‘ 0 ) )
34 9 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝐼 ‘ 1 ) = ( 𝐹 ‘ 0 ) )
35 22 33 34 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝐼 ‘ 1 ) = ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ‘ 0 ) )
36 30 32 35 pcocn ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ∈ ( II Cn 𝐽 ) )
37 30 32 pco0 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ‘ 0 ) = ( 𝐼 ‘ 0 ) )
38 8 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝐹 ‘ 1 ) = ( 𝐼 ‘ 0 ) )
39 37 38 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ‘ 0 ) = ( 𝐹 ‘ 1 ) )
40 30 32 pco1 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ‘ 1 ) = ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ‘ 1 ) )
41 21 31 pco1 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ‘ 1 ) = ( 𝐹 ‘ 1 ) )
42 40 41 eqtrd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ‘ 1 ) = ( 𝐹 ‘ 1 ) )
43 2 25 10 29 36 39 42 elpi1i ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) ∈ ( Base ‘ 𝑄 ) )
44 eceq1 ⊢ ( 𝑔 = ℎ → [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) )
45 oveq1 ⊢ ( 𝑔 = ℎ → ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) = ( ℎ ( *𝑝 ‘ 𝐽 ) 𝐹 ) )
46 45 oveq2d ⊢ ( 𝑔 = ℎ → ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) = ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) )
47 46 eceq1d ⊢ ( 𝑔 = ℎ → [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) = [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) )
48 phtpcer ⊢ ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 )
49 48 a1i ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 ) )
50 22 3ad2antr1 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → ( 𝑔 ‘ 0 ) = ( 𝐹 ‘ 0 ) )
51 21 3ad2antr1 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → 𝑔 ∈ ( II Cn 𝐽 ) )
52 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → 𝐹 ∈ ( II Cn 𝐽 ) )
53 51 52 pco0 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ‘ 0 ) = ( 𝑔 ‘ 0 ) )
54 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → ( 𝐼 ‘ 1 ) = ( 𝐹 ‘ 0 ) )
55 50 53 54 3eqtr4rd ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → ( 𝐼 ‘ 1 ) = ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ‘ 0 ) )
56 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → 𝐼 ∈ ( II Cn 𝐽 ) )
57 49 56 erref ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → 𝐼 ( ≃ph ‘ 𝐽 ) 𝐼 )
58 23 3ad2antr1 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → ( 𝑔 ‘ 1 ) = ( 𝐹 ‘ 0 ) )
59 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) )
60 49 51 erth ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → ( 𝑔 ( ≃ph ‘ 𝐽 ) ℎ ↔ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) )
61 59 60 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → 𝑔 ( ≃ph ‘ 𝐽 ) ℎ )
62 49 52 erref ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → 𝐹 ( ≃ph ‘ 𝐽 ) 𝐹 )
63 58 61 62 pcohtpy ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ( ≃ph ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝐹 ) )
64 55 57 63 pcohtpy ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ( ≃ph ‘ 𝐽 ) ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) )
65 49 64 erthi ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) = [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) )
66 4 24 43 44 47 65 fliftfund ⊢ ( 𝜑 → Fun 𝐺 )
67 4 24 43 fliftf ⊢ ( 𝜑 → ( Fun 𝐺 ↔ 𝐺 : ran ( 𝑔 ∈ ∪ 𝐵 ↦ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ) ⟶ ( Base ‘ 𝑄 ) ) )
68 66 67 mpbid ⊢ ( 𝜑 → 𝐺 : ran ( 𝑔 ∈ ∪ 𝐵 ↦ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ) ⟶ ( Base ‘ 𝑄 ) )
69 1 5 16 18 pi1bas2 ⊢ ( 𝜑 → 𝐵 = ( ∪ 𝐵 / ( ≃ph ‘ 𝐽 ) ) )
70 df-qs ⊢ ( ∪ 𝐵 / ( ≃ph ‘ 𝐽 ) ) = { 𝑠 ∣ ∃ 𝑔 ∈ ∪ 𝐵 𝑠 = [ 𝑔 ] ( ≃ph ‘ 𝐽 ) }
71 eqid ⊢ ( 𝑔 ∈ ∪ 𝐵 ↦ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ) = ( 𝑔 ∈ ∪ 𝐵 ↦ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) )
72 71 rnmpt ⊢ ran ( 𝑔 ∈ ∪ 𝐵 ↦ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ) = { 𝑠 ∣ ∃ 𝑔 ∈ ∪ 𝐵 𝑠 = [ 𝑔 ] ( ≃ph ‘ 𝐽 ) }
73 70 72 eqtr4i ⊢ ( ∪ 𝐵 / ( ≃ph ‘ 𝐽 ) ) = ran ( 𝑔 ∈ ∪ 𝐵 ↦ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) )
74 69 73 eqtrdi ⊢ ( 𝜑 → 𝐵 = ran ( 𝑔 ∈ ∪ 𝐵 ↦ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ) )
75 74 feq2d ⊢ ( 𝜑 → ( 𝐺 : 𝐵 ⟶ ( Base ‘ 𝑄 ) ↔ 𝐺 : ran ( 𝑔 ∈ ∪ 𝐵 ↦ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ) ⟶ ( Base ‘ 𝑄 ) ) )
76 68 75 mpbird ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ ( Base ‘ 𝑄 ) )