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		simpr	$⊢ (φ \land y \in ran (s \in A ⟼ X + s)) \to y \in ran (s \in A ⟼ X + s)$
41	29	elrnmpt	$⊢ y \in ran (s \in A ⟼ X + s) \to (y \in ran (s \in A ⟼ X + s) \leftrightarrow \exists s \in A y = X + s)$
42	41	adantl	$⊢ (φ \land y \in ran (s \in A ⟼ X + s)) \to (y \in ran (s \in A ⟼ X + s) \leftrightarrow \exists s \in A y = X + s)$
43	40 42	mpbid	$⊢ (φ \land y \in ran (s \in A ⟼ X + s)) \to \exists s \in A y = X + s$
44		nfv	$⊢ Ⅎ s φ$
45		nfmpt1	$⊢ \underline{Ⅎ} s (s \in A ⟼ X + s)$
46	45	nfrn	$⊢ \underline{Ⅎ} s ran (s \in A ⟼ X + s)$
47	46	nfcri	$⊢ Ⅎ s y \in ran (s \in A ⟼ X + s)$
48	44 47	nfan	$⊢ Ⅎ s (φ \land y \in ran (s \in A ⟼ X + s))$
49		nfv	$⊢ Ⅎ s y \in B$
50		simp3	$⊢ (φ \land s \in A \land y = X + s) \to y = X + s$
51	5	3adant3	$⊢ (φ \land s \in A \land y = X + s) \to X + s \in B$
52	50 51	eqeltrd	$⊢ (φ \land s \in A \land y = X + s) \to y \in B$
53	52	3exp	$⊢ φ \to (s \in A \to (y = X + s \to y \in B))$
54	53	adantr	$⊢ (φ \land y \in ran (s \in A ⟼ X + s)) \to (s \in A \to (y = X + s \to y \in B))$
55	48 49 54	rexlimd	$⊢ (φ \land y \in ran (s \in A ⟼ X + s)) \to (\exists s \in A y = X + s \to y \in B)$
56	43 55	mpd	$⊢ (φ \land y \in ran (s \in A ⟼ X + s)) \to y \in B$
57	56	ralrimiva	$⊢ φ \to \forall y \in ran (s \in A ⟼ X + s) y \in B$
58		dfss3	$⊢ ran (s \in A ⟼ X + s) \subseteq B \leftrightarrow \forall y \in ran (s \in A ⟼ X + s) y \in B$
59	57 58	sylibr	$⊢ φ \to ran (s \in A ⟼ X + s) \subseteq B$
60		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)$
61	59 60	syl	$⊢ φ \to ({F ↾}_{B}) \circ (s \in A ⟼ X + s) = F \circ (s \in A ⟼ X + s)$
62	23 29	fmptd	$⊢ φ \to (s \in A ⟼ X + s) : A ⟶ ℝ$
63		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)))$
64	1 62 63	syl2anc	$⊢ φ \to F \circ (s \in A ⟼ X + s) = (x \in A ⟼ F ((s \in A ⟼ X + s) (x)))$
65	4	a1i	$⊢ φ \to G = (s \in A ⟼ F (X + s))$
66		oveq2	$⊢ s = x \to X + s = X + x$
67	66	fveq2d	$⊢ s = x \to F (X + s) = F (X + x)$
68	67	cbvmptv	$⊢ (s \in A ⟼ F (X + s)) = (x \in A ⟼ F (X + x))$
69	68	a1i	$⊢ φ \to (s \in A ⟼ F (X + s)) = (x \in A ⟼ F (X + x))$
70		eqidd	$⊢ (φ \land x \in A) \to (s \in A ⟼ X + s) = (s \in A ⟼ X + s)$
71	66	adantl	$⊢ ((φ \land x \in A) \land s = x) \to X + s = X + x$
72		simpr	$⊢ (φ \land x \in A) \to x \in A$
73	2	adantr	$⊢ (φ \land x \in A) \to X \in ℝ$
74	3	sselda	$⊢ (φ \land x \in A) \to x \in ℝ$
75	73 74	readdcld	$⊢ (φ \land x \in A) \to X + x \in ℝ$
76	70 71 72 75	fvmptd	$⊢ (φ \land x \in A) \to (s \in A ⟼ X + s) (x) = X + x$
77	76	eqcomd	$⊢ (φ \land x \in A) \to X + x = (s \in A ⟼ X + s) (x)$
78	77	fveq2d	$⊢ (φ \land x \in A) \to F (X + x) = F ((s \in A ⟼ X + s) (x))$
79	78	mpteq2dva	$⊢ φ \to (x \in A ⟼ F (X + x)) = (x \in A ⟼ F ((s \in A ⟼ X + s) (x)))$
80	65 69 79	3eqtrrd	$⊢ φ \to (x \in A ⟼ F ((s \in A ⟼ X + s) (x))) = G$
81	61 64 80	3eqtrd	$⊢ φ \to ({F ↾}_{B}) \circ (s \in A ⟼ X + s) = G$
82	81	oveq1d	$⊢ φ \to (({F ↾}_{B}) \circ (s \in A ⟼ X + s)) {lim}_{ℂ} D = G {lim}_{ℂ} D$
83	39 82	eleqtrd	$⊢ φ \to C \in (G {lim}_{ℂ} D)$

Metamath Proof Explorer

Theorem fourierdlem53

Proof