This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 ∈ V
Assertion shftfn ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ∈ ℂ ) → ( 𝐹 shift 𝐴 ) Fn { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ 𝐵 } )

Proof

Step Hyp Ref Expression
1 shftfval.1 ⊢ 𝐹 ∈ V
2 relopabv ⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) }
3 2 a1i ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ∈ ℂ ) → Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } )
4 fnfun ⊢ ( 𝐹 Fn 𝐵 → Fun 𝐹 )
5 4 adantr ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ∈ ℂ ) → Fun 𝐹 )
6 funmo ⊢ ( Fun 𝐹 → ∃* 𝑤 ( 𝑧 − 𝐴 ) 𝐹 𝑤 )
7 vex ⊢ 𝑧 ∈ V
8 vex ⊢ 𝑤 ∈ V
9 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ ℂ ↔ 𝑧 ∈ ℂ ) )
10 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 − 𝐴 ) = ( 𝑧 − 𝐴 ) )
11 10 breq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 − 𝐴 ) 𝐹 𝑦 ↔ ( 𝑧 − 𝐴 ) 𝐹 𝑦 ) )
12 9 11 anbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) ↔ ( 𝑧 ∈ ℂ ∧ ( 𝑧 − 𝐴 ) 𝐹 𝑦 ) ) )
13 breq2 ⊢ ( 𝑦 = 𝑤 → ( ( 𝑧 − 𝐴 ) 𝐹 𝑦 ↔ ( 𝑧 − 𝐴 ) 𝐹 𝑤 ) )
14 13 anbi2d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑧 ∈ ℂ ∧ ( 𝑧 − 𝐴 ) 𝐹 𝑦 ) ↔ ( 𝑧 ∈ ℂ ∧ ( 𝑧 − 𝐴 ) 𝐹 𝑤 ) ) )
15 eqid ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) }
16 7 8 12 14 15 brab ⊢ ( 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } 𝑤 ↔ ( 𝑧 ∈ ℂ ∧ ( 𝑧 − 𝐴 ) 𝐹 𝑤 ) )
17 16 simprbi ⊢ ( 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } 𝑤 → ( 𝑧 − 𝐴 ) 𝐹 𝑤 )
18 17 moimi ⊢ ( ∃* 𝑤 ( 𝑧 − 𝐴 ) 𝐹 𝑤 → ∃* 𝑤 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } 𝑤 )
19 6 18 syl ⊢ ( Fun 𝐹 → ∃* 𝑤 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } 𝑤 )
20 19 alrimiv ⊢ ( Fun 𝐹 → ∀ 𝑧 ∃* 𝑤 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } 𝑤 )
21 5 20 syl ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ∈ ℂ ) → ∀ 𝑧 ∃* 𝑤 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } 𝑤 )
22 dffun6 ⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } ↔ ( Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } ∧ ∀ 𝑧 ∃* 𝑤 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } 𝑤 ) )
23 3 21 22 sylanbrc ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ∈ ℂ ) → Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } )
24 1 shftfval ⊢ ( 𝐴 ∈ ℂ → ( 𝐹 shift 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } )
25 24 adantl ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ∈ ℂ ) → ( 𝐹 shift 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } )
26 25 funeqd ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ∈ ℂ ) → ( Fun ( 𝐹 shift 𝐴 ) ↔ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } ) )
27 23 26 mpbird ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ∈ ℂ ) → Fun ( 𝐹 shift 𝐴 ) )
28 1 shftdm ⊢ ( 𝐴 ∈ ℂ → dom ( 𝐹 shift 𝐴 ) = { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ dom 𝐹 } )
29 fndm ⊢ ( 𝐹 Fn 𝐵 → dom 𝐹 = 𝐵 )
30 29 eleq2d ⊢ ( 𝐹 Fn 𝐵 → ( ( 𝑥 − 𝐴 ) ∈ dom 𝐹 ↔ ( 𝑥 − 𝐴 ) ∈ 𝐵 ) )
31 30 rabbidv ⊢ ( 𝐹 Fn 𝐵 → { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ dom 𝐹 } = { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ 𝐵 } )
32 28 31 sylan9eqr ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ∈ ℂ ) → dom ( 𝐹 shift 𝐴 ) = { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ 𝐵 } )
33 df-fn ⊢ ( ( 𝐹 shift 𝐴 ) Fn { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ 𝐵 } ↔ ( Fun ( 𝐹 shift 𝐴 ) ∧ dom ( 𝐹 shift 𝐴 ) = { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ 𝐵 } ) )
34 27 32 33 sylanbrc ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ∈ ℂ ) → ( 𝐹 shift 𝐴 ) Fn { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ 𝐵 } )