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 { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ 𝐵 } )