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	|- P = ( J pi1 A )
	pi1co.q	|- Q = ( K pi1 B )
	pi1co.v	|- V = ( Base ` P )
	pi1co.g	|- G = ran ( g e. U. V |-> <. [ g ] ( ~=ph ` J ) , [ ( F o. g ) ] ( ~=ph ` K ) >. )
	pi1co.j	|- ( ph -> J e. ( TopOn ` X ) )
	pi1co.f	|- ( ph -> F e. ( J Cn K ) )
	pi1co.a	|- ( ph -> A e. X )
	pi1co.b	|- ( ph -> ( F ` A ) = B )
Assertion	pi1coval	|- ( ( ph /\ T e. U. V ) -> ( G ` [ T ] ( ~=ph ` J ) ) = [ ( F o. T ) ] ( ~=ph ` K ) )

Proof

Step	Hyp	Ref	Expression
1		pi1co.p	|- P = ( J pi1 A )
2		pi1co.q	|- Q = ( K pi1 B )
3		pi1co.v	|- V = ( Base ` P )
4		pi1co.g	|- G = ran ( g e. U. V |-> <. [ g ] ( ~=ph ` J ) , [ ( F o. g ) ] ( ~=ph ` K ) >. )
5		pi1co.j	|- ( ph -> J e. ( TopOn ` X ) )
6		pi1co.f	|- ( ph -> F e. ( J Cn K ) )
7		pi1co.a	|- ( ph -> A e. X )
8		pi1co.b	|- ( ph -> ( F ` A ) = B )
9		fvex	|- ( ~=ph ` J ) e. _V
10		ecexg	|- ( ( ~=ph ` J ) e. _V -> [ g ] ( ~=ph ` J ) e. _V )
11	9 10	mp1i	|- ( ( ph /\ g e. U. V ) -> [ g ] ( ~=ph ` J ) e. _V )
12		fvex	|- ( ~=ph ` K ) e. _V
13		ecexg	|- ( ( ~=ph ` K ) e. _V -> [ ( F o. g ) ] ( ~=ph ` K ) e. _V )
14	12 13	mp1i	|- ( ( ph /\ g e. U. V ) -> [ ( F o. g ) ] ( ~=ph ` K ) e. _V )
15		eceq1	|- ( g = T -> [ g ] ( ~=ph ` J ) = [ T ] ( ~=ph ` J ) )
16		coeq2	|- ( g = T -> ( F o. g ) = ( F o. T ) )
17	16	eceq1d	|- ( g = T -> [ ( F o. g ) ] ( ~=ph ` K ) = [ ( F o. T ) ] ( ~=ph ` K ) )
18	1 2 3 4 5 6 7 8	pi1cof	|- ( ph -> G : V --> ( Base ` Q ) )
19	18	ffund	|- ( ph -> Fun G )
20	4 11 14 15 17 19	fliftval	|- ( ( ph /\ T e. U. V ) -> ( G ` [ T ] ( ~=ph ` J ) ) = [ ( F o. T ) ] ( ~=ph ` K ) )