Metamath Proof Explorer

Theorem pi1cof

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

Ref Expression
Hypotheses pi1co.p ⊢ 𝑃 = ( 𝐽 π1 𝐴 )
pi1co.q ⊢ 𝑄 = ( 𝐾 π1 𝐵 )
pi1co.v ⊢ 𝑉 = ( Base ‘ 𝑃 )
pi1co.g ⊢ 𝐺 = ran ( 𝑔 ∈ ∪ 𝑉 ↦ ⟨ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ∘ 𝑔 ) ] ( ≃ph ‘ 𝐾 ) ⟩ )
pi1co.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
pi1co.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
pi1co.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
pi1co.b ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 𝐵 )
Assertion pi1cof ( 𝜑 → 𝐺 : 𝑉 ⟶ ( Base ‘ 𝑄 ) )

Proof

Step Hyp Ref Expression
1 pi1co.p ⊢ 𝑃 = ( 𝐽 π1 𝐴 )
2 pi1co.q ⊢ 𝑄 = ( 𝐾 π1 𝐵 )
3 pi1co.v ⊢ 𝑉 = ( Base ‘ 𝑃 )
4 pi1co.g ⊢ 𝐺 = ran ( 𝑔 ∈ ∪ 𝑉 ↦ ⟨ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ∘ 𝑔 ) ] ( ≃ph ‘ 𝐾 ) ⟩ )
5 pi1co.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
6 pi1co.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
7 pi1co.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
8 pi1co.b ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 𝐵 )
9 fvex ⊢ ( ≃ph ‘ 𝐽 ) ∈ V
10 ecexg ⊢ ( ( ≃ph ‘ 𝐽 ) ∈ V → [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ∈ V )
11 9 10 mp1i ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝑉 ) → [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ∈ V )
12 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
13 cntop2 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
14 6 13 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
15 toptopon2 ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
16 14 15 sylib ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝑉 ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
18 cnf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 : 𝑋 ⟶ ∪ 𝐾 )
19 5 16 6 18 syl3anc ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ∪ 𝐾 )
20 19 7 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ∪ 𝐾 )
21 8 20 eqeltrrd ⊢ ( 𝜑 → 𝐵 ∈ ∪ 𝐾 )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝑉 ) → 𝐵 ∈ ∪ 𝐾 )
23 3 a1i ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑃 ) )
24 1 5 7 23 pi1eluni ⊢ ( 𝜑 → ( 𝑔 ∈ ∪ 𝑉 ↔ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( 𝑔 ‘ 0 ) = 𝐴 ∧ ( 𝑔 ‘ 1 ) = 𝐴 ) ) )
25 24 biimpa ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝑉 ) → ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( 𝑔 ‘ 0 ) = 𝐴 ∧ ( 𝑔 ‘ 1 ) = 𝐴 ) )
26 25 simp1d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝑉 ) → 𝑔 ∈ ( II Cn 𝐽 ) )
27 6 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝑉 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
28 cnco ⊢ ( ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐹 ∘ 𝑔 ) ∈ ( II Cn 𝐾 ) )
29 26 27 28 syl2anc ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝑉 ) → ( 𝐹 ∘ 𝑔 ) ∈ ( II Cn 𝐾 ) )
30 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
31 cnf2 ⊢ ( ( II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑔 ∈ ( II Cn 𝐽 ) ) → 𝑔 : ( 0 [,] 1 ) ⟶ 𝑋 )
32 30 5 26 31 mp3an2ani ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝑉 ) → 𝑔 : ( 0 [,] 1 ) ⟶ 𝑋 )
33 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
34 fvco3 ⊢ ( ( 𝑔 : ( 0 [,] 1 ) ⟶ 𝑋 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ 𝑔 ) ‘ 0 ) = ( 𝐹 ‘ ( 𝑔 ‘ 0 ) ) )
35 32 33 34 sylancl ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝑉 ) → ( ( 𝐹 ∘ 𝑔 ) ‘ 0 ) = ( 𝐹 ‘ ( 𝑔 ‘ 0 ) ) )
36 25 simp2d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝑉 ) → ( 𝑔 ‘ 0 ) = 𝐴 )
37 36 fveq2d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝑉 ) → ( 𝐹 ‘ ( 𝑔 ‘ 0 ) ) = ( 𝐹 ‘ 𝐴 ) )
38 8 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝑉 ) → ( 𝐹 ‘ 𝐴 ) = 𝐵 )
39 35 37 38 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝑉 ) → ( ( 𝐹 ∘ 𝑔 ) ‘ 0 ) = 𝐵 )
40 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
41 fvco3 ⊢ ( ( 𝑔 : ( 0 [,] 1 ) ⟶ 𝑋 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ 𝑔 ) ‘ 1 ) = ( 𝐹 ‘ ( 𝑔 ‘ 1 ) ) )
42 32 40 41 sylancl ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝑉 ) → ( ( 𝐹 ∘ 𝑔 ) ‘ 1 ) = ( 𝐹 ‘ ( 𝑔 ‘ 1 ) ) )
43 25 simp3d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝑉 ) → ( 𝑔 ‘ 1 ) = 𝐴 )
44 43 fveq2d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝑉 ) → ( 𝐹 ‘ ( 𝑔 ‘ 1 ) ) = ( 𝐹 ‘ 𝐴 ) )
45 42 44 38 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝑉 ) → ( ( 𝐹 ∘ 𝑔 ) ‘ 1 ) = 𝐵 )
46 2 12 17 22 29 39 45 elpi1i ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝑉 ) → [ ( 𝐹 ∘ 𝑔 ) ] ( ≃ph ‘ 𝐾 ) ∈ ( Base ‘ 𝑄 ) )
47 eceq1 ⊢ ( 𝑔 = ℎ → [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) )
48 coeq2 ⊢ ( 𝑔 = ℎ → ( 𝐹 ∘ 𝑔 ) = ( 𝐹 ∘ ℎ ) )
49 48 eceq1d ⊢ ( 𝑔 = ℎ → [ ( 𝐹 ∘ 𝑔 ) ] ( ≃ph ‘ 𝐾 ) = [ ( 𝐹 ∘ ℎ ) ] ( ≃ph ‘ 𝐾 ) )
50 phtpcer ⊢ ( ≃ph ‘ 𝐾 ) Er ( II Cn 𝐾 )
51 50 a1i ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → ( ≃ph ‘ 𝐾 ) Er ( II Cn 𝐾 ) )
52 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) )
53 phtpcer ⊢ ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 )
54 53 a1i ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 ) )
55 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → 𝑔 ∈ ∪ 𝑉 )
56 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → ( 𝑔 ∈ ∪ 𝑉 ↔ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( 𝑔 ‘ 0 ) = 𝐴 ∧ ( 𝑔 ‘ 1 ) = 𝐴 ) ) )
57 55 56 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( 𝑔 ‘ 0 ) = 𝐴 ∧ ( 𝑔 ‘ 1 ) = 𝐴 ) )
58 57 simp1d ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → 𝑔 ∈ ( II Cn 𝐽 ) )
59 54 58 erth ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → ( 𝑔 ( ≃ph ‘ 𝐽 ) ℎ ↔ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) )
60 52 59 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → 𝑔 ( ≃ph ‘ 𝐽 ) ℎ )
61 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
62 60 61 phtpcco2 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → ( 𝐹 ∘ 𝑔 ) ( ≃ph ‘ 𝐾 ) ( 𝐹 ∘ ℎ ) )
63 51 62 erthi ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) → [ ( 𝐹 ∘ 𝑔 ) ] ( ≃ph ‘ 𝐾 ) = [ ( 𝐹 ∘ ℎ ) ] ( ≃ph ‘ 𝐾 ) )
64 4 11 46 47 49 63 fliftfund ⊢ ( 𝜑 → Fun 𝐺 )
65 4 11 46 fliftf ⊢ ( 𝜑 → ( Fun 𝐺 ↔ 𝐺 : ran ( 𝑔 ∈ ∪ 𝑉 ↦ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ) ⟶ ( Base ‘ 𝑄 ) ) )
66 64 65 mpbid ⊢ ( 𝜑 → 𝐺 : ran ( 𝑔 ∈ ∪ 𝑉 ↦ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ) ⟶ ( Base ‘ 𝑄 ) )
67 1 5 7 23 pi1bas2 ⊢ ( 𝜑 → 𝑉 = ( ∪ 𝑉 / ( ≃ph ‘ 𝐽 ) ) )
68 df-qs ⊢ ( ∪ 𝑉 / ( ≃ph ‘ 𝐽 ) ) = { 𝑠 ∣ ∃ 𝑔 ∈ ∪ 𝑉 𝑠 = [ 𝑔 ] ( ≃ph ‘ 𝐽 ) }
69 eqid ⊢ ( 𝑔 ∈ ∪ 𝑉 ↦ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ) = ( 𝑔 ∈ ∪ 𝑉 ↦ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) )
70 69 rnmpt ⊢ ran ( 𝑔 ∈ ∪ 𝑉 ↦ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ) = { 𝑠 ∣ ∃ 𝑔 ∈ ∪ 𝑉 𝑠 = [ 𝑔 ] ( ≃ph ‘ 𝐽 ) }
71 68 70 eqtr4i ⊢ ( ∪ 𝑉 / ( ≃ph ‘ 𝐽 ) ) = ran ( 𝑔 ∈ ∪ 𝑉 ↦ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) )
72 67 71 eqtrdi ⊢ ( 𝜑 → 𝑉 = ran ( 𝑔 ∈ ∪ 𝑉 ↦ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ) )
73 72 feq2d ⊢ ( 𝜑 → ( 𝐺 : 𝑉 ⟶ ( Base ‘ 𝑄 ) ↔ 𝐺 : ran ( 𝑔 ∈ ∪ 𝑉 ↦ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ) ⟶ ( Base ‘ 𝑄 ) ) )
74 66 73 mpbird ⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ ( Base ‘ 𝑄 ) )