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 ‘ 𝐽 ) )