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 relopabv ⊢ 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