Theorem pi1coval

Description: The value of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 10-Aug-2015) (Proof shortened 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	pi1coval	⊢ ( ( 𝜑 ∧ 𝑇 ∈ ∪ 𝑉 ) → ( 𝐺 ‘ [ 𝑇 ] ( ≃ph ‘ 𝐽 ) ) = [ ( 𝐹 ∘ 𝑇 ) ] ( ≃ph ‘ 𝐾 ) )

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		fvex	⊢ ( ≃ph ‘ 𝐾 ) ∈ V
13		ecexg	⊢ ( ( ≃ph ‘ 𝐾 ) ∈ V → [ ( 𝐹 ∘ 𝑔 ) ] ( ≃ph ‘ 𝐾 ) ∈ V )
14	12 13	mp1i	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝑉 ) → [ ( 𝐹 ∘ 𝑔 ) ] ( ≃ph ‘ 𝐾 ) ∈ V )
15		eceq1	⊢ ( 𝑔 = 𝑇 → [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ 𝑇 ] ( ≃ph ‘ 𝐽 ) )
16		coeq2	⊢ ( 𝑔 = 𝑇 → ( 𝐹 ∘ 𝑔 ) = ( 𝐹 ∘ 𝑇 ) )
17	16	eceq1d	⊢ ( 𝑔 = 𝑇 → [ ( 𝐹 ∘ 𝑔 ) ] ( ≃ph ‘ 𝐾 ) = [ ( 𝐹 ∘ 𝑇 ) ] ( ≃ph ‘ 𝐾 ) )
18	1 2 3 4 5 6 7 8	pi1cof	⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ ( Base ‘ 𝑄 ) )
19	18	ffund	⊢ ( 𝜑 → Fun 𝐺 )
20	4 11 14 15 17 19	fliftval	⊢ ( ( 𝜑 ∧ 𝑇 ∈ ∪ 𝑉 ) → ( 𝐺 ‘ [ 𝑇 ] ( ≃ph ‘ 𝐽 ) ) = [ ( 𝐹 ∘ 𝑇 ) ] ( ≃ph ‘ 𝐾 ) )