Metamath Proof Explorer

Theorem pi1xfrval

Description: The value of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 12-Feb-2015) (Revised by Mario Carneiro, 23-Dec-2016)

Ref Expression
Hypotheses pi1xfr.p ⊢ P = J π 1 F ⁡ 0
pi1xfr.q ⊢ Q = J π 1 F ⁡ 1
pi1xfr.b ⊢ B = Base P
pi1xfr.g ⊢ G = ran ⁡ g ∈ ⋃ B ⟼ g ≃ ph ⁡ J I * 𝑝 ⁡ J g * 𝑝 ⁡ J F ≃ ph ⁡ J
pi1xfr.j ⊢ φ → J ∈ TopOn ⁡ X
pi1xfr.f ⊢ φ → F ∈ II Cn J
pi1xfrval.i ⊢ φ → I ∈ II Cn J
pi1xfrval.1 ⊢ φ → F ⁡ 1 = I ⁡ 0
pi1xfrval.2 ⊢ φ → I ⁡ 1 = F ⁡ 0
pi1xfrval.a ⊢ φ → A ∈ ⋃ B
Assertion pi1xfrval ⊢ φ → G ⁡ A ≃ ph ⁡ J = I * 𝑝 ⁡ J A * 𝑝 ⁡ J F ≃ ph ⁡ J

Proof

Step Hyp Ref Expression
1 pi1xfr.p ⊢ P = J π 1 F ⁡ 0
2 pi1xfr.q ⊢ Q = J π 1 F ⁡ 1
3 pi1xfr.b ⊢ B = Base P
4 pi1xfr.g ⊢ G = ran ⁡ g ∈ ⋃ B ⟼ g ≃ ph ⁡ J I * 𝑝 ⁡ J g * 𝑝 ⁡ J F ≃ ph ⁡ J
5 pi1xfr.j ⊢ φ → J ∈ TopOn ⁡ X
6 pi1xfr.f ⊢ φ → F ∈ II Cn J
7 pi1xfrval.i ⊢ φ → I ∈ II Cn J
8 pi1xfrval.1 ⊢ φ → F ⁡ 1 = I ⁡ 0
9 pi1xfrval.2 ⊢ φ → I ⁡ 1 = F ⁡ 0
10 pi1xfrval.a ⊢ φ → A ∈ ⋃ B
11 fvex ⊢ ≃ ph ⁡ J ∈ V
12 ecexg ⊢ ≃ ph ⁡ J ∈ V → g ≃ ph ⁡ J ∈ V
13 11 12 mp1i ⊢ φ ∧ g ∈ ⋃ B → g ≃ ph ⁡ J ∈ V
14 ecexg ⊢ ≃ ph ⁡ J ∈ V → I * 𝑝 ⁡ J g * 𝑝 ⁡ J F ≃ ph ⁡ J ∈ V
15 11 14 mp1i ⊢ φ ∧ g ∈ ⋃ B → I * 𝑝 ⁡ J g * 𝑝 ⁡ J F ≃ ph ⁡ J ∈ V
16 eceq1 ⊢ g = A → g ≃ ph ⁡ J = A ≃ ph ⁡ J
17 oveq1 ⊢ g = A → g * 𝑝 ⁡ J F = A * 𝑝 ⁡ J F
18 17 oveq2d ⊢ g = A → I * 𝑝 ⁡ J g * 𝑝 ⁡ J F = I * 𝑝 ⁡ J A * 𝑝 ⁡ J F
19 18 eceq1d ⊢ g = A → I * 𝑝 ⁡ J g * 𝑝 ⁡ J F ≃ ph ⁡ J = I * 𝑝 ⁡ J A * 𝑝 ⁡ J F ≃ ph ⁡ J
20 1 2 3 4 5 6 7 8 9 pi1xfrf ⊢ φ → G : B ⟶ Base Q
21 20 ffund ⊢ φ → Fun ⁡ G
22 4 13 15 16 19 21 fliftval ⊢ φ ∧ A ∈ ⋃ B → G ⁡ A ≃ ph ⁡ J = I * 𝑝 ⁡ J A * 𝑝 ⁡ J F ≃ ph ⁡ J
23 10 22 mpdan ⊢ φ → G ⁡ A ≃ ph ⁡ J = I * 𝑝 ⁡ J A * 𝑝 ⁡ J F ≃ ph ⁡ J