Metamath Proof Explorer

Theorem pcorev2

Description: Concatenation with the reverse path. (Contributed by Mario Carneiro, 12-Feb-2015)

Ref Expression
Hypotheses pcorev2.1 
|- G = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )
pcorev2.2 
|- P = ( ( 0 [,] 1 ) X. { ( F ` 0 ) } )
Assertion pcorev2 
|- ( F e. ( II Cn J ) -> ( F ( *p ` J ) G ) ( ~=ph ` J ) P )

Proof

Step Hyp Ref Expression
1 pcorev2.1 
 |-  G = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )
2 pcorev2.2 
 |-  P = ( ( 0 [,] 1 ) X. { ( F ` 0 ) } )
3 1 pcorevcl 
 |-  ( F e. ( II Cn J ) -> ( G e. ( II Cn J ) /\ ( G ` 0 ) = ( F ` 1 ) /\ ( G ` 1 ) = ( F ` 0 ) ) )
4 3 simp1d 
 |-  ( F e. ( II Cn J ) -> G e. ( II Cn J ) )
5 eqid 
 |-  ( y e. ( 0 [,] 1 ) |-> ( G ` ( 1 - y ) ) ) = ( y e. ( 0 [,] 1 ) |-> ( G ` ( 1 - y ) ) )
6 eqid 
 |-  ( ( 0 [,] 1 ) X. { ( G ` 1 ) } ) = ( ( 0 [,] 1 ) X. { ( G ` 1 ) } )
7 5 6 pcorev 
 |-  ( G e. ( II Cn J ) -> ( ( y e. ( 0 [,] 1 ) |-> ( G ` ( 1 - y ) ) ) ( *p ` J ) G ) ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( G ` 1 ) } ) )
8 4 7 syl 
 |-  ( F e. ( II Cn J ) -> ( ( y e. ( 0 [,] 1 ) |-> ( G ` ( 1 - y ) ) ) ( *p ` J ) G ) ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( G ` 1 ) } ) )
9 iirev 
 |-  ( y e. ( 0 [,] 1 ) -> ( 1 - y ) e. ( 0 [,] 1 ) )
10 oveq2 
 |-  ( x = ( 1 - y ) -> ( 1 - x ) = ( 1 - ( 1 - y ) ) )
11 10 fveq2d 
 |-  ( x = ( 1 - y ) -> ( F ` ( 1 - x ) ) = ( F ` ( 1 - ( 1 - y ) ) ) )
12 fvex 
 |-  ( F ` ( 1 - ( 1 - y ) ) ) e. _V
13 11 1 12 fvmpt 
 |-  ( ( 1 - y ) e. ( 0 [,] 1 ) -> ( G ` ( 1 - y ) ) = ( F ` ( 1 - ( 1 - y ) ) ) )
14 9 13 syl 
 |-  ( y e. ( 0 [,] 1 ) -> ( G ` ( 1 - y ) ) = ( F ` ( 1 - ( 1 - y ) ) ) )
15 ax-1cn 
 |-  1 e. CC
16 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
17 16 sseli 
 |-  ( y e. ( 0 [,] 1 ) -> y e. RR )
18 17 recnd 
 |-  ( y e. ( 0 [,] 1 ) -> y e. CC )
19 nncan 
 |-  ( ( 1 e. CC /\ y e. CC ) -> ( 1 - ( 1 - y ) ) = y )
20 15 18 19 sylancr 
 |-  ( y e. ( 0 [,] 1 ) -> ( 1 - ( 1 - y ) ) = y )
21 20 fveq2d 
 |-  ( y e. ( 0 [,] 1 ) -> ( F ` ( 1 - ( 1 - y ) ) ) = ( F ` y ) )
22 14 21 eqtrd 
 |-  ( y e. ( 0 [,] 1 ) -> ( G ` ( 1 - y ) ) = ( F ` y ) )
23 22 mpteq2ia 
 |-  ( y e. ( 0 [,] 1 ) |-> ( G ` ( 1 - y ) ) ) = ( y e. ( 0 [,] 1 ) |-> ( F ` y ) )
24 iiuni 
 |-  ( 0 [,] 1 ) = U. II
25 eqid 
 |-  U. J = U. J
26 24 25 cnf 
 |-  ( F e. ( II Cn J ) -> F : ( 0 [,] 1 ) --> U. J )
27 26 feqmptd 
 |-  ( F e. ( II Cn J ) -> F = ( y e. ( 0 [,] 1 ) |-> ( F ` y ) ) )
28 23 27 eqtr4id 
 |-  ( F e. ( II Cn J ) -> ( y e. ( 0 [,] 1 ) |-> ( G ` ( 1 - y ) ) ) = F )
29 28 oveq1d 
 |-  ( F e. ( II Cn J ) -> ( ( y e. ( 0 [,] 1 ) |-> ( G ` ( 1 - y ) ) ) ( *p ` J ) G ) = ( F ( *p ` J ) G ) )
30 3 simp3d 
 |-  ( F e. ( II Cn J ) -> ( G ` 1 ) = ( F ` 0 ) )
31 30 sneqd 
 |-  ( F e. ( II Cn J ) -> { ( G ` 1 ) } = { ( F ` 0 ) } )
32 31 xpeq2d 
 |-  ( F e. ( II Cn J ) -> ( ( 0 [,] 1 ) X. { ( G ` 1 ) } ) = ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) )
33 32 2 eqtr4di 
 |-  ( F e. ( II Cn J ) -> ( ( 0 [,] 1 ) X. { ( G ` 1 ) } ) = P )
34 8 29 33 3brtr3d 
 |-  ( F e. ( II Cn J ) -> ( F ( *p ` J ) G ) ( ~=ph ` J ) P )