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 𝑃 = ( 𝐽 π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 ) )
pi1xfrval.a ( 𝜑𝐴 𝐵 )
Assertion pi1xfrval ( 𝜑 → ( 𝐺 ‘ [ 𝐴 ] ( ≃ph𝐽 ) ) = [ ( 𝐼 ( *𝑝𝐽 ) ( 𝐴 ( *𝑝𝐽 ) 𝐹 ) ) ] ( ≃ph𝐽 ) )

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 pi1xfrval.a ( 𝜑𝐴 𝐵 )
11 fvex ( ≃ph𝐽 ) ∈ V
12 ecexg ( ( ≃ph𝐽 ) ∈ V → [ 𝑔 ] ( ≃ph𝐽 ) ∈ V )
13 11 12 mp1i ( ( 𝜑𝑔 𝐵 ) → [ 𝑔 ] ( ≃ph𝐽 ) ∈ V )
14 ecexg ( ( ≃ph𝐽 ) ∈ V → [ ( 𝐼 ( *𝑝𝐽 ) ( 𝑔 ( *𝑝𝐽 ) 𝐹 ) ) ] ( ≃ph𝐽 ) ∈ V )
15 11 14 mp1i ( ( 𝜑𝑔 𝐵 ) → [ ( 𝐼 ( *𝑝𝐽 ) ( 𝑔 ( *𝑝𝐽 ) 𝐹 ) ) ] ( ≃ph𝐽 ) ∈ V )
16 eceq1 ( 𝑔 = 𝐴 → [ 𝑔 ] ( ≃ph𝐽 ) = [ 𝐴 ] ( ≃ph𝐽 ) )
17 oveq1 ( 𝑔 = 𝐴 → ( 𝑔 ( *𝑝𝐽 ) 𝐹 ) = ( 𝐴 ( *𝑝𝐽 ) 𝐹 ) )
18 17 oveq2d ( 𝑔 = 𝐴 → ( 𝐼 ( *𝑝𝐽 ) ( 𝑔 ( *𝑝𝐽 ) 𝐹 ) ) = ( 𝐼 ( *𝑝𝐽 ) ( 𝐴 ( *𝑝𝐽 ) 𝐹 ) ) )
19 18 eceq1d ( 𝑔 = 𝐴 → [ ( 𝐼 ( *𝑝𝐽 ) ( 𝑔 ( *𝑝𝐽 ) 𝐹 ) ) ] ( ≃ph𝐽 ) = [ ( 𝐼 ( *𝑝𝐽 ) ( 𝐴 ( *𝑝𝐽 ) 𝐹 ) ) ] ( ≃ph𝐽 ) )
20 1 2 3 4 5 6 7 8 9 pi1xfrf ( 𝜑𝐺 : 𝐵 ⟶ ( Base ‘ 𝑄 ) )
21 20 ffund ( 𝜑 → Fun 𝐺 )
22 4 13 15 16 19 21 fliftval ( ( 𝜑𝐴 𝐵 ) → ( 𝐺 ‘ [ 𝐴 ] ( ≃ph𝐽 ) ) = [ ( 𝐼 ( *𝑝𝐽 ) ( 𝐴 ( *𝑝𝐽 ) 𝐹 ) ) ] ( ≃ph𝐽 ) )
23 10 22 mpdan ( 𝜑 → ( 𝐺 ‘ [ 𝐴 ] ( ≃ph𝐽 ) ) = [ ( 𝐼 ( *𝑝𝐽 ) ( 𝐴 ( *𝑝𝐽 ) 𝐹 ) ) ] ( ≃ph𝐽 ) )