Metamath Proof Explorer


Theorem shftfn

Description: Functionality and domain of a sequence shifted by A . (Contributed by NM, 20-Jul-2005) (Revised by Mario Carneiro, 3-Nov-2013)

Ref Expression
Hypothesis shftfval.1 F V
Assertion shftfn F Fn B A F shift A Fn x | x A B

Proof

Step Hyp Ref Expression
1 shftfval.1 F V
2 relopab Rel x y | x x A F y
3 2 a1i F Fn B A Rel x y | x x A F y
4 fnfun F Fn B Fun F
5 4 adantr F Fn B A Fun F
6 funmo Fun F * w z A F w
7 vex z V
8 vex w V
9 eleq1w x = z x z
10 oveq1 x = z x A = z A
11 10 breq1d x = z x A F y z A F y
12 9 11 anbi12d x = z x x A F y z z A F y
13 breq2 y = w z A F y z A F w
14 13 anbi2d y = w z z A F y z z A F w
15 eqid x y | x x A F y = x y | x x A F y
16 7 8 12 14 15 brab z x y | x x A F y w z z A F w
17 16 simprbi z x y | x x A F y w z A F w
18 17 moimi * w z A F w * w z x y | x x A F y w
19 6 18 syl Fun F * w z x y | x x A F y w
20 19 alrimiv Fun F z * w z x y | x x A F y w
21 5 20 syl F Fn B A z * w z x y | x x A F y w
22 dffun6 Fun x y | x x A F y Rel x y | x x A F y z * w z x y | x x A F y w
23 3 21 22 sylanbrc F Fn B A Fun x y | x x A F y
24 1 shftfval A F shift A = x y | x x A F y
25 24 adantl F Fn B A F shift A = x y | x x A F y
26 25 funeqd F Fn B A Fun F shift A Fun x y | x x A F y
27 23 26 mpbird F Fn B A Fun F shift A
28 1 shftdm A dom F shift A = x | x A dom F
29 fndm F Fn B dom F = B
30 29 eleq2d F Fn B x A dom F x A B
31 30 rabbidv F Fn B x | x A dom F = x | x A B
32 28 31 sylan9eqr F Fn B A dom F shift A = x | x A B
33 df-fn F shift A Fn x | x A B Fun F shift A dom F shift A = x | x A B
34 27 32 33 sylanbrc F Fn B A F shift A Fn x | x A B