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	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem53.2	$⊢ φ \to X \in ℝ$
	fourierdlem53.3	$⊢ φ \to A \subseteq ℝ$
	fourierdlem53.g	$⊢ G = (s \in A ⟼ F (X + s))$
	fourierdlem53.xps	$⊢ (φ \land s \in A) \to X + s \in B$
	fourierdlem53.b	$⊢ φ \to B \subseteq ℝ$
	fourierdlem53.sned	$⊢ (φ \land s \in A) \to s \neq D$
	fourierdlem53.c	$⊢ φ \to C \in (({F ↾}_{B}) {lim}_{ℂ} (X + D))$
	fourierdlem53.d	$⊢ φ \to D \in ℂ$
Assertion	fourierdlem53	$⊢ φ \to C \in (G {lim}_{ℂ} D)$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem53.1	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem53.2	$⊢ φ \to X \in ℝ$
3		fourierdlem53.3	$⊢ φ \to A \subseteq ℝ$
4		fourierdlem53.g	$⊢ G = (s \in A ⟼ F (X + s))$
5		fourierdlem53.xps	$⊢ (φ \land s \in A) \to X + s \in B$
6		fourierdlem53.b	$⊢ φ \to B \subseteq ℝ$
7		fourierdlem53.sned	$⊢ (φ \land s \in A) \to s \neq D$
8		fourierdlem53.c	$⊢ φ \to C \in (({F ↾}_{B}) {lim}_{ℂ} (X + D))$
9		fourierdlem53.d	$⊢ φ \to D \in ℂ$
10	1 6	fssresd	$⊢ φ \to ({F ↾}_{B}) : B ⟶ ℝ$
11	10	fdmd	$⊢ φ \to dom ({F ↾}_{B}) = B$
12	11	eqcomd	$⊢ φ \to B = dom ({F ↾}_{B})$
13	12	adantr	$⊢ (φ \land s \in A) \to B = dom ({F ↾}_{B})$
14	5 13	eleqtrd	$⊢ (φ \land s \in A) \to X + s \in dom ({F ↾}_{B})$
15	2	recnd	$⊢ φ \to X \in ℂ$
16	15	adantr	$⊢ (φ \land s \in A) \to X \in ℂ$
17	3	sselda	$⊢ (φ \land s \in A) \to s \in ℝ$
18	17	recnd	$⊢ (φ \land s \in A) \to s \in ℂ$
19	9	adantr	$⊢ (φ \land s \in A) \to D \in ℂ$
20	16 18 19 7	addneintrd	$⊢ (φ \land s \in A) \to X + s \neq X + D$
21	20	neneqd	$⊢ (φ \land s \in A) \to \neg X + s = X + D$
22	2	adantr	$⊢ (φ \land s \in A) \to X \in ℝ$
23	22 17	readdcld	$⊢ (φ \land s \in A) \to X + s \in ℝ$
24		elsng	$⊢ X + s \in ℝ \to (X + s \in \{X + D\} \leftrightarrow X + s = X + D)$
25	23 24	syl	$⊢ (φ \land s \in A) \to (X + s \in \{X + D\} \leftrightarrow X + s = X + D)$
26	21 25	mtbird	$⊢ (φ \land s \in A) \to \neg X + s \in \{X + D\}$
27	14 26	eldifd	$⊢ (φ \land s \in A) \to X + s \in (dom ({F ↾}_{B}) ∖ \{X + D\})$
28	27	ralrimiva	$⊢ φ \to \forall s \in A X + s \in (dom ({F ↾}_{B}) ∖ \{X + D\})$
29		eqid	$⊢ (s \in A ⟼ X + s) = (s \in A ⟼ X + s)$
30	29	rnmptss	$⊢ \forall s \in A X + s \in (dom ({F ↾}_{B}) ∖ \{X + D\}) \to ran (s \in A ⟼ X + s) \subseteq dom ({F ↾}_{B}) ∖ \{X + D\}$
31	28 30	syl	$⊢ φ \to ran (s \in A ⟼ X + s) \subseteq dom ({F ↾}_{B}) ∖ \{X + D\}$
32		eqid	$⊢ (s \in A ⟼ X) = (s \in A ⟼ X)$
33		eqid	$⊢ (s \in A ⟼ s) = (s \in A ⟼ s)$
34		ax-resscn	$⊢ ℝ \subseteq ℂ$
35	3 34	sstrdi	$⊢ φ \to A \subseteq ℂ$
36	32 35 15 9	constlimc	$⊢ φ \to X \in ((s \in A ⟼ X) {lim}_{ℂ} D)$
37	35 33 9	idlimc	$⊢ φ \to D \in ((s \in A ⟼ s) {lim}_{ℂ} D)$
38	32 33 29 16 18 36 37	addlimc	$⊢ φ \to X + D \in ((s \in A ⟼ X + s) {lim}_{ℂ} D)$
39	31 38 8	limccog	$⊢ φ \to C \in ((({F ↾}_{B}) \circ (s \in A ⟼ X + s)) {lim}_{ℂ} D)$
40		nfv	$⊢ Ⅎ s φ$
41	40 29 5	rnmptssd	$⊢ φ \to ran (s \in A ⟼ X + s) \subseteq B$
42		cores	$⊢ ran (s \in A ⟼ X + s) \subseteq B \to ({F ↾}_{B}) \circ (s \in A ⟼ X + s) = F \circ (s \in A ⟼ X + s)$
43	41 42	syl	$⊢ φ \to ({F ↾}_{B}) \circ (s \in A ⟼ X + s) = F \circ (s \in A ⟼ X + s)$
44	23 29	fmptd	$⊢ φ \to (s \in A ⟼ X + s) : A ⟶ ℝ$
45		fcompt	$⊢ (F : ℝ ⟶ ℝ \land (s \in A ⟼ X + s) : A ⟶ ℝ) \to F \circ (s \in A ⟼ X + s) = (x \in A ⟼ F ((s \in A ⟼ X + s) (x)))$
46	1 44 45	syl2anc	$⊢ φ \to F \circ (s \in A ⟼ X + s) = (x \in A ⟼ F ((s \in A ⟼ X + s) (x)))$
47	4	a1i	$⊢ φ \to G = (s \in A ⟼ F (X + s))$
48		oveq2	$⊢ s = x \to X + s = X + x$
49	48	fveq2d	$⊢ s = x \to F (X + s) = F (X + x)$
50	49	cbvmptv	$⊢ (s \in A ⟼ F (X + s)) = (x \in A ⟼ F (X + x))$
51	50	a1i	$⊢ φ \to (s \in A ⟼ F (X + s)) = (x \in A ⟼ F (X + x))$
52		eqidd	$⊢ (φ \land x \in A) \to (s \in A ⟼ X + s) = (s \in A ⟼ X + s)$
53	48	adantl	$⊢ ((φ \land x \in A) \land s = x) \to X + s = X + x$
54		simpr	$⊢ (φ \land x \in A) \to x \in A$
55	2	adantr	$⊢ (φ \land x \in A) \to X \in ℝ$
56	3	sselda	$⊢ (φ \land x \in A) \to x \in ℝ$
57	55 56	readdcld	$⊢ (φ \land x \in A) \to X + x \in ℝ$
58	52 53 54 57	fvmptd	$⊢ (φ \land x \in A) \to (s \in A ⟼ X + s) (x) = X + x$
59	58	eqcomd	$⊢ (φ \land x \in A) \to X + x = (s \in A ⟼ X + s) (x)$
60	59	fveq2d	$⊢ (φ \land x \in A) \to F (X + x) = F ((s \in A ⟼ X + s) (x))$
61	60	mpteq2dva	$⊢ φ \to (x \in A ⟼ F (X + x)) = (x \in A ⟼ F ((s \in A ⟼ X + s) (x)))$
62	47 51 61	3eqtrrd	$⊢ φ \to (x \in A ⟼ F ((s \in A ⟼ X + s) (x))) = G$
63	43 46 62	3eqtrd	$⊢ φ \to ({F ↾}_{B}) \circ (s \in A ⟼ X + s) = G$
64	63	oveq1d	$⊢ φ \to (({F ↾}_{B}) \circ (s \in A ⟼ X + s)) {lim}_{ℂ} D = G {lim}_{ℂ} D$
65	39 64	eleqtrd	$⊢ φ \to C \in (G {lim}_{ℂ} D)$

Metamath Proof Explorer

Theorem fourierdlem53

Proof