Metamath Proof Explorer

Theorem fargshiftfva

Description: The values of a shifted function correspond to the value of the original function. (Contributed by Alexander van der Vekens, 24-Nov-2017)

Ref Expression
Hypothesis fargshift.g 
|- G = ( x e. ( 0 ..^ ( # ` F ) ) |-> ( F ` ( x + 1 ) ) )
Assertion fargshiftfva 
|- ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) -> ( A. k e. ( 1 ... N ) ( E ` ( F ` k ) ) = [_ k / x ]_ P -> A. l e. ( 0 ..^ N ) ( E ` ( G ` l ) ) = [_ ( l + 1 ) / x ]_ P ) )

Proof

Step Hyp Ref Expression
1 fargshift.g 
 |-  G = ( x e. ( 0 ..^ ( # ` F ) ) |-> ( F ` ( x + 1 ) ) )
2 fz0add1fz1 
 |-  ( ( N e. NN0 /\ l e. ( 0 ..^ N ) ) -> ( l + 1 ) e. ( 1 ... N ) )
3 simpl 
 |-  ( ( ( l + 1 ) e. ( 1 ... N ) /\ ( N e. NN0 /\ l e. ( 0 ..^ N ) ) ) -> ( l + 1 ) e. ( 1 ... N ) )
4 3 adantr 
 |-  ( ( ( ( l + 1 ) e. ( 1 ... N ) /\ ( N e. NN0 /\ l e. ( 0 ..^ N ) ) ) /\ F : ( 1 ... N ) --> dom E ) -> ( l + 1 ) e. ( 1 ... N ) )
5 2fveq3 
 |-  ( k = ( l + 1 ) -> ( E ` ( F ` k ) ) = ( E ` ( F ` ( l + 1 ) ) ) )
6 csbeq1 
 |-  ( k = ( l + 1 ) -> [_ k / x ]_ P = [_ ( l + 1 ) / x ]_ P )
7 5 6 eqeq12d 
 |-  ( k = ( l + 1 ) -> ( ( E ` ( F ` k ) ) = [_ k / x ]_ P <-> ( E ` ( F ` ( l + 1 ) ) ) = [_ ( l + 1 ) / x ]_ P ) )
8 7 adantl 
 |-  ( ( ( ( ( l + 1 ) e. ( 1 ... N ) /\ ( N e. NN0 /\ l e. ( 0 ..^ N ) ) ) /\ F : ( 1 ... N ) --> dom E ) /\ k = ( l + 1 ) ) -> ( ( E ` ( F ` k ) ) = [_ k / x ]_ P <-> ( E ` ( F ` ( l + 1 ) ) ) = [_ ( l + 1 ) / x ]_ P ) )
9 simpl 
 |-  ( ( N e. NN0 /\ l e. ( 0 ..^ N ) ) -> N e. NN0 )
10 9 adantl 
 |-  ( ( ( l + 1 ) e. ( 1 ... N ) /\ ( N e. NN0 /\ l e. ( 0 ..^ N ) ) ) -> N e. NN0 )
11 10 anim1i 
 |-  ( ( ( ( l + 1 ) e. ( 1 ... N ) /\ ( N e. NN0 /\ l e. ( 0 ..^ N ) ) ) /\ F : ( 1 ... N ) --> dom E ) -> ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) )
12 11 adantr 
 |-  ( ( ( ( ( l + 1 ) e. ( 1 ... N ) /\ ( N e. NN0 /\ l e. ( 0 ..^ N ) ) ) /\ F : ( 1 ... N ) --> dom E ) /\ k = ( l + 1 ) ) -> ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) )
13 simpr 
 |-  ( ( N e. NN0 /\ l e. ( 0 ..^ N ) ) -> l e. ( 0 ..^ N ) )
14 13 ad3antlr 
 |-  ( ( ( ( ( l + 1 ) e. ( 1 ... N ) /\ ( N e. NN0 /\ l e. ( 0 ..^ N ) ) ) /\ F : ( 1 ... N ) --> dom E ) /\ k = ( l + 1 ) ) -> l e. ( 0 ..^ N ) )
15 1 fargshiftfv 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) -> ( l e. ( 0 ..^ N ) -> ( G ` l ) = ( F ` ( l + 1 ) ) ) )
16 15 imp 
 |-  ( ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) /\ l e. ( 0 ..^ N ) ) -> ( G ` l ) = ( F ` ( l + 1 ) ) )
17 16 eqcomd 
 |-  ( ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) /\ l e. ( 0 ..^ N ) ) -> ( F ` ( l + 1 ) ) = ( G ` l ) )
18 12 14 17 syl2anc 
 |-  ( ( ( ( ( l + 1 ) e. ( 1 ... N ) /\ ( N e. NN0 /\ l e. ( 0 ..^ N ) ) ) /\ F : ( 1 ... N ) --> dom E ) /\ k = ( l + 1 ) ) -> ( F ` ( l + 1 ) ) = ( G ` l ) )
19 18 fveqeq2d 
 |-  ( ( ( ( ( l + 1 ) e. ( 1 ... N ) /\ ( N e. NN0 /\ l e. ( 0 ..^ N ) ) ) /\ F : ( 1 ... N ) --> dom E ) /\ k = ( l + 1 ) ) -> ( ( E ` ( F ` ( l + 1 ) ) ) = [_ ( l + 1 ) / x ]_ P <-> ( E ` ( G ` l ) ) = [_ ( l + 1 ) / x ]_ P ) )
20 8 19 bitrd 
 |-  ( ( ( ( ( l + 1 ) e. ( 1 ... N ) /\ ( N e. NN0 /\ l e. ( 0 ..^ N ) ) ) /\ F : ( 1 ... N ) --> dom E ) /\ k = ( l + 1 ) ) -> ( ( E ` ( F ` k ) ) = [_ k / x ]_ P <-> ( E ` ( G ` l ) ) = [_ ( l + 1 ) / x ]_ P ) )
21 4 20 rspcdv 
 |-  ( ( ( ( l + 1 ) e. ( 1 ... N ) /\ ( N e. NN0 /\ l e. ( 0 ..^ N ) ) ) /\ F : ( 1 ... N ) --> dom E ) -> ( A. k e. ( 1 ... N ) ( E ` ( F ` k ) ) = [_ k / x ]_ P -> ( E ` ( G ` l ) ) = [_ ( l + 1 ) / x ]_ P ) )
22 21 ex 
 |-  ( ( ( l + 1 ) e. ( 1 ... N ) /\ ( N e. NN0 /\ l e. ( 0 ..^ N ) ) ) -> ( F : ( 1 ... N ) --> dom E -> ( A. k e. ( 1 ... N ) ( E ` ( F ` k ) ) = [_ k / x ]_ P -> ( E ` ( G ` l ) ) = [_ ( l + 1 ) / x ]_ P ) ) )
23 22 com23 
 |-  ( ( ( l + 1 ) e. ( 1 ... N ) /\ ( N e. NN0 /\ l e. ( 0 ..^ N ) ) ) -> ( A. k e. ( 1 ... N ) ( E ` ( F ` k ) ) = [_ k / x ]_ P -> ( F : ( 1 ... N ) --> dom E -> ( E ` ( G ` l ) ) = [_ ( l + 1 ) / x ]_ P ) ) )
24 2 23 mpancom 
 |-  ( ( N e. NN0 /\ l e. ( 0 ..^ N ) ) -> ( A. k e. ( 1 ... N ) ( E ` ( F ` k ) ) = [_ k / x ]_ P -> ( F : ( 1 ... N ) --> dom E -> ( E ` ( G ` l ) ) = [_ ( l + 1 ) / x ]_ P ) ) )
25 24 ex 
 |-  ( N e. NN0 -> ( l e. ( 0 ..^ N ) -> ( A. k e. ( 1 ... N ) ( E ` ( F ` k ) ) = [_ k / x ]_ P -> ( F : ( 1 ... N ) --> dom E -> ( E ` ( G ` l ) ) = [_ ( l + 1 ) / x ]_ P ) ) ) )
26 25 com24 
 |-  ( N e. NN0 -> ( F : ( 1 ... N ) --> dom E -> ( A. k e. ( 1 ... N ) ( E ` ( F ` k ) ) = [_ k / x ]_ P -> ( l e. ( 0 ..^ N ) -> ( E ` ( G ` l ) ) = [_ ( l + 1 ) / x ]_ P ) ) ) )
27 26 imp31 
 |-  ( ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) /\ A. k e. ( 1 ... N ) ( E ` ( F ` k ) ) = [_ k / x ]_ P ) -> ( l e. ( 0 ..^ N ) -> ( E ` ( G ` l ) ) = [_ ( l + 1 ) / x ]_ P ) )
28 27 ralrimiv 
 |-  ( ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) /\ A. k e. ( 1 ... N ) ( E ` ( F ` k ) ) = [_ k / x ]_ P ) -> A. l e. ( 0 ..^ N ) ( E ` ( G ` l ) ) = [_ ( l + 1 ) / x ]_ P )
29 28 ex 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) -> ( A. k e. ( 1 ... N ) ( E ` ( F ` k ) ) = [_ k / x ]_ P -> A. l e. ( 0 ..^ N ) ( E ` ( G ` l ) ) = [_ ( l + 1 ) / x ]_ P ) )