Theorem shftfval

Description: The value of the sequence shifter operation is a function on CC . A is ordinarily an integer. (Contributed by NM, 20-Jul-2005) (Revised by Mario Carneiro, 3-Nov-2013)

	Ref	Expression
Hypothesis	shftfval.1	⊢ 𝐹 ∈ V
Assertion	shftfval	⊢ ( 𝐴 ∈ ℂ → ( 𝐹 shift 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } )

Proof

Step	Hyp	Ref	Expression
1		shftfval.1	⊢ 𝐹 ∈ V
2		ovex	⊢ ( 𝑥 − 𝐴 ) ∈ V
3		vex	⊢ 𝑦 ∈ V
4	2 3	breldm	⊢ ( ( 𝑥 − 𝐴 ) 𝐹 𝑦 → ( 𝑥 − 𝐴 ) ∈ dom 𝐹 )
5		npcan	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝑥 − 𝐴 ) + 𝐴 ) = 𝑥 )
6	5	eqcomd	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → 𝑥 = ( ( 𝑥 − 𝐴 ) + 𝐴 ) )
7	6	ancoms	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → 𝑥 = ( ( 𝑥 − 𝐴 ) + 𝐴 ) )
8		oveq1	⊢ ( 𝑤 = ( 𝑥 − 𝐴 ) → ( 𝑤 + 𝐴 ) = ( ( 𝑥 − 𝐴 ) + 𝐴 ) )
9	8	rspceeqv	⊢ ( ( ( 𝑥 − 𝐴 ) ∈ dom 𝐹 ∧ 𝑥 = ( ( 𝑥 − 𝐴 ) + 𝐴 ) ) → ∃ 𝑤 ∈ dom 𝐹 𝑥 = ( 𝑤 + 𝐴 ) )
10	4 7 9	syl2anr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) → ∃ 𝑤 ∈ dom 𝐹 𝑥 = ( 𝑤 + 𝐴 ) )
11		vex	⊢ 𝑥 ∈ V
12		eqeq1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 = ( 𝑤 + 𝐴 ) ↔ 𝑥 = ( 𝑤 + 𝐴 ) ) )
13	12	rexbidv	⊢ ( 𝑧 = 𝑥 → ( ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) ↔ ∃ 𝑤 ∈ dom 𝐹 𝑥 = ( 𝑤 + 𝐴 ) ) )
14	11 13	elab	⊢ ( 𝑥 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } ↔ ∃ 𝑤 ∈ dom 𝐹 𝑥 = ( 𝑤 + 𝐴 ) )
15	10 14	sylibr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) → 𝑥 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } )
16	2 3	brelrn	⊢ ( ( 𝑥 − 𝐴 ) 𝐹 𝑦 → 𝑦 ∈ ran 𝐹 )
17	16	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) → 𝑦 ∈ ran 𝐹 )
18	15 17	jca	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) → ( 𝑥 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } ∧ 𝑦 ∈ ran 𝐹 ) )
19	18	expl	⊢ ( 𝐴 ∈ ℂ → ( ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) → ( 𝑥 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } ∧ 𝑦 ∈ ran 𝐹 ) ) )
20	19	ssopab2dv	⊢ ( 𝐴 ∈ ℂ → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } ∧ 𝑦 ∈ ran 𝐹 ) } )
21		df-xp	⊢ ( { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } × ran 𝐹 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } ∧ 𝑦 ∈ ran 𝐹 ) }
22	20 21	sseqtrrdi	⊢ ( 𝐴 ∈ ℂ → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } ⊆ ( { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } × ran 𝐹 ) )
23	1	dmex	⊢ dom 𝐹 ∈ V
24	23	abrexex	⊢ { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } ∈ V
25	1	rnex	⊢ ran 𝐹 ∈ V
26	24 25	xpex	⊢ ( { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } × ran 𝐹 ) ∈ V
27		ssexg	⊢ ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } ⊆ ( { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } × ran 𝐹 ) ∧ ( { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } × ran 𝐹 ) ∈ V ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } ∈ V )
28	22 26 27	sylancl	⊢ ( 𝐴 ∈ ℂ → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } ∈ V )
29		breq	⊢ ( 𝑧 = 𝐹 → ( ( 𝑥 − 𝑤 ) 𝑧 𝑦 ↔ ( 𝑥 − 𝑤 ) 𝐹 𝑦 ) )
30	29	anbi2d	⊢ ( 𝑧 = 𝐹 → ( ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝑤 ) 𝑧 𝑦 ) ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝑤 ) 𝐹 𝑦 ) ) )
31	30	opabbidv	⊢ ( 𝑧 = 𝐹 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝑤 ) 𝑧 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝑤 ) 𝐹 𝑦 ) } )
32		oveq2	⊢ ( 𝑤 = 𝐴 → ( 𝑥 − 𝑤 ) = ( 𝑥 − 𝐴 ) )
33	32	breq1d	⊢ ( 𝑤 = 𝐴 → ( ( 𝑥 − 𝑤 ) 𝐹 𝑦 ↔ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) )
34	33	anbi2d	⊢ ( 𝑤 = 𝐴 → ( ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝑤 ) 𝐹 𝑦 ) ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) ) )
35	34	opabbidv	⊢ ( 𝑤 = 𝐴 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝑤 ) 𝐹 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } )
36		df-shft	⊢ shift = ( 𝑧 ∈ V , 𝑤 ∈ ℂ ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝑤 ) 𝑧 𝑦 ) } )
37	31 35 36	ovmpog	⊢ ( ( 𝐹 ∈ V ∧ 𝐴 ∈ ℂ ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } ∈ V ) → ( 𝐹 shift 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } )
38	1 37	mp3an1	⊢ ( ( 𝐴 ∈ ℂ ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } ∈ V ) → ( 𝐹 shift 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } )
39	28 38	mpdan	⊢ ( 𝐴 ∈ ℂ → ( 𝐹 shift 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } )