Theorem fourierdlem53

Description: The limit of F ( s ) at ( X + D ) is the limit of F ( X + s ) at D . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem53.1	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
	fourierdlem53.2	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	fourierdlem53.3	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	fourierdlem53.g	⊢ 𝐺 = ( 𝑠 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
	fourierdlem53.xps	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑋 + 𝑠 ) ∈ 𝐵 )
	fourierdlem53.b	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
	fourierdlem53.sned	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ≠ 𝐷 )
	fourierdlem53.c	⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ ( 𝑋 + 𝐷 ) ) )
	fourierdlem53.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
Assertion	fourierdlem53	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐺 limℂ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem53.1	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2		fourierdlem53.2	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
3		fourierdlem53.3	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
4		fourierdlem53.g	⊢ 𝐺 = ( 𝑠 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
5		fourierdlem53.xps	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑋 + 𝑠 ) ∈ 𝐵 )
6		fourierdlem53.b	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
7		fourierdlem53.sned	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ≠ 𝐷 )
8		fourierdlem53.c	⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ ( 𝑋 + 𝐷 ) ) )
9		fourierdlem53.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
10	1 6	fssresd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ℝ )
11	10	fdmd	⊢ ( 𝜑 → dom ( 𝐹 ↾ 𝐵 ) = 𝐵 )
12	11	eqcomd	⊢ ( 𝜑 → 𝐵 = dom ( 𝐹 ↾ 𝐵 ) )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝐵 = dom ( 𝐹 ↾ 𝐵 ) )
14	5 13	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑋 + 𝑠 ) ∈ dom ( 𝐹 ↾ 𝐵 ) )
15	2	recnd	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑋 ∈ ℂ )
17	3	sselda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ℝ )
18	17	recnd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ℂ )
19	9	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝐷 ∈ ℂ )
20	16 18 19 7	addneintrd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑋 + 𝑠 ) ≠ ( 𝑋 + 𝐷 ) )
21	20	neneqd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ¬ ( 𝑋 + 𝑠 ) = ( 𝑋 + 𝐷 ) )
22	2	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑋 ∈ ℝ )
23	22 17	readdcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
24		elsng	⊢ ( ( 𝑋 + 𝑠 ) ∈ ℝ → ( ( 𝑋 + 𝑠 ) ∈ { ( 𝑋 + 𝐷 ) } ↔ ( 𝑋 + 𝑠 ) = ( 𝑋 + 𝐷 ) ) )
25	23 24	syl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝑋 + 𝑠 ) ∈ { ( 𝑋 + 𝐷 ) } ↔ ( 𝑋 + 𝑠 ) = ( 𝑋 + 𝐷 ) ) )
26	21 25	mtbird	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ¬ ( 𝑋 + 𝑠 ) ∈ { ( 𝑋 + 𝐷 ) } )
27	14 26	eldifd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑋 + 𝑠 ) ∈ ( dom ( 𝐹 ↾ 𝐵 ) ∖ { ( 𝑋 + 𝐷 ) } ) )
28	27	ralrimiva	⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝐴 ( 𝑋 + 𝑠 ) ∈ ( dom ( 𝐹 ↾ 𝐵 ) ∖ { ( 𝑋 + 𝐷 ) } ) )
29		eqid	⊢ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) = ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) )
30	29	rnmptss	⊢ ( ∀ 𝑠 ∈ 𝐴 ( 𝑋 + 𝑠 ) ∈ ( dom ( 𝐹 ↾ 𝐵 ) ∖ { ( 𝑋 + 𝐷 ) } ) → ran ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ⊆ ( dom ( 𝐹 ↾ 𝐵 ) ∖ { ( 𝑋 + 𝐷 ) } ) )
31	28 30	syl	⊢ ( 𝜑 → ran ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ⊆ ( dom ( 𝐹 ↾ 𝐵 ) ∖ { ( 𝑋 + 𝐷 ) } ) )
32		eqid	⊢ ( 𝑠 ∈ 𝐴 ↦ 𝑋 ) = ( 𝑠 ∈ 𝐴 ↦ 𝑋 )
33		eqid	⊢ ( 𝑠 ∈ 𝐴 ↦ 𝑠 ) = ( 𝑠 ∈ 𝐴 ↦ 𝑠 )
34		ax-resscn	⊢ ℝ ⊆ ℂ
35	3 34	sstrdi	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
36	32 35 15 9	constlimc	⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝑠 ∈ 𝐴 ↦ 𝑋 ) limℂ 𝐷 ) )
37	35 33 9	idlimc	⊢ ( 𝜑 → 𝐷 ∈ ( ( 𝑠 ∈ 𝐴 ↦ 𝑠 ) limℂ 𝐷 ) )
38	32 33 29 16 18 36 37	addlimc	⊢ ( 𝜑 → ( 𝑋 + 𝐷 ) ∈ ( ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) limℂ 𝐷 ) )
39	31 38 8	limccog	⊢ ( 𝜑 → 𝐶 ∈ ( ( ( 𝐹 ↾ 𝐵 ) ∘ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ) limℂ 𝐷 ) )
40		nfv	⊢ Ⅎ 𝑠 𝜑
41	40 29 5	rnmptssd	⊢ ( 𝜑 → ran ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ⊆ 𝐵 )
42		cores	⊢ ( ran ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ⊆ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ∘ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ) = ( 𝐹 ∘ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ) )
43	41 42	syl	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐵 ) ∘ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ) = ( 𝐹 ∘ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ) )
44	23 29	fmptd	⊢ ( 𝜑 → ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) : 𝐴 ⟶ ℝ )
45		fcompt	⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) : 𝐴 ⟶ ℝ ) → ( 𝐹 ∘ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ ( ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ‘ 𝑥 ) ) ) )
46	1 44 45	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ ( ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ‘ 𝑥 ) ) ) )
47	4	a1i	⊢ ( 𝜑 → 𝐺 = ( 𝑠 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) )
48		oveq2	⊢ ( 𝑠 = 𝑥 → ( 𝑋 + 𝑠 ) = ( 𝑋 + 𝑥 ) )
49	48	fveq2d	⊢ ( 𝑠 = 𝑥 → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑥 ) ) )
50	49	cbvmptv	⊢ ( 𝑠 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝑋 + 𝑥 ) ) )
51	50	a1i	⊢ ( 𝜑 → ( 𝑠 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝑋 + 𝑥 ) ) ) )
52		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) = ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) )
53	48	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑠 = 𝑥 ) → ( 𝑋 + 𝑠 ) = ( 𝑋 + 𝑥 ) )
54		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
55	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑋 ∈ ℝ )
56	3	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
57	55 56	readdcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑋 + 𝑥 ) ∈ ℝ )
58	52 53 54 57	fvmptd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ‘ 𝑥 ) = ( 𝑋 + 𝑥 ) )
59	58	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑋 + 𝑥 ) = ( ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ‘ 𝑥 ) )
60	59	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝑋 + 𝑥 ) ) = ( 𝐹 ‘ ( ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ‘ 𝑥 ) ) )
61	60	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝑋 + 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ ( ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ‘ 𝑥 ) ) ) )
62	47 51 61	3eqtrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ ( ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ‘ 𝑥 ) ) ) = 𝐺 )
63	43 46 62	3eqtrd	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐵 ) ∘ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ) = 𝐺 )
64	63	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐹 ↾ 𝐵 ) ∘ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ) limℂ 𝐷 ) = ( 𝐺 limℂ 𝐷 ) )
65	39 64	eleqtrd	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐺 limℂ 𝐷 ) )