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 pi1 ( F ` 0 ) )
pi1xfr.q 
|- Q = ( J pi1 ( F ` 1 ) )
pi1xfr.b 
|- B = ( Base ` P )
pi1xfr.g 
|- G = ran ( g e. U. B |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) >. )
pi1xfr.j 
|- ( ph -> J e. ( TopOn ` X ) )
pi1xfr.f 
|- ( ph -> F e. ( II Cn J ) )
pi1xfrval.i 
|- ( ph -> I e. ( II Cn J ) )
pi1xfrval.1 
|- ( ph -> ( F ` 1 ) = ( I ` 0 ) )
pi1xfrval.2 
|- ( ph -> ( I ` 1 ) = ( F ` 0 ) )
pi1xfrval.a 
|- ( ph -> A e. U. B )
Assertion pi1xfrval 
|- ( ph -> ( G ` [ A ] ( ~=ph ` J ) ) = [ ( I ( *p ` J ) ( A ( *p ` J ) F ) ) ] ( ~=ph ` J ) )

Proof

Step Hyp Ref Expression
1 pi1xfr.p 
 |-  P = ( J pi1 ( F ` 0 ) )
2 pi1xfr.q 
 |-  Q = ( J pi1 ( F ` 1 ) )
3 pi1xfr.b 
 |-  B = ( Base ` P )
4 pi1xfr.g 
 |-  G = ran ( g e. U. B |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) >. )
5 pi1xfr.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
6 pi1xfr.f 
 |-  ( ph -> F e. ( II Cn J ) )
7 pi1xfrval.i 
 |-  ( ph -> I e. ( II Cn J ) )
8 pi1xfrval.1 
 |-  ( ph -> ( F ` 1 ) = ( I ` 0 ) )
9 pi1xfrval.2 
 |-  ( ph -> ( I ` 1 ) = ( F ` 0 ) )
10 pi1xfrval.a 
 |-  ( ph -> A e. U. B )
11 fvex 
 |-  ( ~=ph ` J ) e. _V
12 ecexg 
 |-  ( ( ~=ph ` J ) e. _V -> [ g ] ( ~=ph ` J ) e. _V )
13 11 12 mp1i 
 |-  ( ( ph /\ g e. U. B ) -> [ g ] ( ~=ph ` J ) e. _V )
14 ecexg 
 |-  ( ( ~=ph ` J ) e. _V -> [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) e. _V )
15 11 14 mp1i 
 |-  ( ( ph /\ g e. U. B ) -> [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) e. _V )
16 eceq1 
 |-  ( g = A -> [ g ] ( ~=ph ` J ) = [ A ] ( ~=ph ` J ) )
17 oveq1 
 |-  ( g = A -> ( g ( *p ` J ) F ) = ( A ( *p ` J ) F ) )
18 17 oveq2d 
 |-  ( g = A -> ( I ( *p ` J ) ( g ( *p ` J ) F ) ) = ( I ( *p ` J ) ( A ( *p ` J ) F ) ) )
19 18 eceq1d 
 |-  ( g = A -> [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) = [ ( I ( *p ` J ) ( A ( *p ` J ) F ) ) ] ( ~=ph ` J ) )
20 1 2 3 4 5 6 7 8 9 pi1xfrf 
 |-  ( ph -> G : B --> ( Base ` Q ) )
21 20 ffund 
 |-  ( ph -> Fun G )
22 4 13 15 16 19 21 fliftval 
 |-  ( ( ph /\ A e. U. B ) -> ( G ` [ A ] ( ~=ph ` J ) ) = [ ( I ( *p ` J ) ( A ( *p ` J ) F ) ) ] ( ~=ph ` J ) )
23 10 22 mpdan 
 |-  ( ph -> ( G ` [ A ] ( ~=ph ` J ) ) = [ ( I ( *p ` J ) ( A ( *p ` J ) F ) ) ] ( ~=ph ` J ) )