dvres3a

Description: Restriction of a complex differentiable function to the reals. This version of dvres3 assumes that F is differentiable on its domain, but does not require F to be differentiable on the whole real line. (Contributed by Mario Carneiro, 11-Feb-2015)

		Ref	Expression
	Hypothesis	dvres3a.j	$⊢ J = TopOpen (ℂ_{fld})$
	Assertion	dvres3a	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to S D ({F ↾}_{S}) = {F_{ℂ}^{'} ↾}_{S}$

Proof

Step	Hyp	Ref	Expression
1		dvres3a.j	$⊢ J = TopOpen (ℂ_{fld})$
2		reldv	$⊢ Rel {({F ↾}_{S})}_{S}^{'}$
3		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
4	3	ad2antrr	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to S \subseteq ℂ$
5		simplr	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to F : A ⟶ ℂ$
6		inss2	$⊢ S \cap A \subseteq A$
7		fssres	$⊢ (F : A ⟶ ℂ \land S \cap A \subseteq A) \to ({F ↾}_{(S \cap A)}) : S \cap A ⟶ ℂ$
8	5 6 7	sylancl	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to ({F ↾}_{(S \cap A)}) : S \cap A ⟶ ℂ$
9		rescom	$⊢ {({F ↾}_{A}) ↾}_{S} = {({F ↾}_{S}) ↾}_{A}$
10		resres	$⊢ {({F ↾}_{S}) ↾}_{A} = {F ↾}_{(S \cap A)}$
11	9 10	eqtri	$⊢ {({F ↾}_{A}) ↾}_{S} = {F ↾}_{(S \cap A)}$
12		ffn	$⊢ F : A ⟶ ℂ \to F Fn A$
13		fnresdm	$⊢ F Fn A \to {F ↾}_{A} = F$
14	5 12 13	3syl	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to {F ↾}_{A} = F$
15	14	reseq1d	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to {({F ↾}_{A}) ↾}_{S} = {F ↾}_{S}$
16	11 15	syl5eqr	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to {F ↾}_{(S \cap A)} = {F ↾}_{S}$
17	16	feq1d	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to (({F ↾}_{(S \cap A)}) : S \cap A ⟶ ℂ \leftrightarrow ({F ↾}_{S}) : S \cap A ⟶ ℂ)$
18	8 17	mpbid	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to ({F ↾}_{S}) : S \cap A ⟶ ℂ$
19		inss1	$⊢ S \cap A \subseteq S$
20	19	a1i	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to S \cap A \subseteq S$
21	4 18 20	dvbss	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to dom {({F ↾}_{S})}_{S}^{'} \subseteq S \cap A$
22		dmres	$⊢ dom ({F_{ℂ}^{'} ↾}_{S}) = S \cap dom F_{ℂ}^{'}$
23		simprr	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to dom F_{ℂ}^{'} = A$
24	23	ineq2d	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to S \cap dom F_{ℂ}^{'} = S \cap A$
25	22 24	syl5eq	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to dom ({F_{ℂ}^{'} ↾}_{S}) = S \cap A$
26	21 25	sseqtrrd	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to dom {({F ↾}_{S})}_{S}^{'} \subseteq dom ({F_{ℂ}^{'} ↾}_{S})$
27		relssres	$⊢ (Rel {({F ↾}_{S})}_{S}^{'} \land dom {({F ↾}_{S})}_{S}^{'} \subseteq dom ({F_{ℂ}^{'} ↾}_{S})) \to {{({F ↾}_{S})}_{S}^{'} ↾}_{dom ({F_{ℂ}^{'} ↾}_{S})} = S D ({F ↾}_{S})$
28	2 26 27	sylancr	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to {{({F ↾}_{S})}_{S}^{'} ↾}_{dom ({F_{ℂ}^{'} ↾}_{S})} = S D ({F ↾}_{S})$
29		dvfg	$⊢ S \in \{ℝ, ℂ\} \to {({F ↾}_{S})}_{S}^{'} : dom {({F ↾}_{S})}_{S}^{'} ⟶ ℂ$
30	29	ad2antrr	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to {({F ↾}_{S})}_{S}^{'} : dom {({F ↾}_{S})}_{S}^{'} ⟶ ℂ$
31	30	ffund	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to Fun {({F ↾}_{S})}_{S}^{'}$
32		ssidd	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to ℂ \subseteq ℂ$
33	1	cnfldtopon	$⊢ J \in TopOn (ℂ)$
34		simprl	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to A \in J$
35		toponss	$⊢ (J \in TopOn (ℂ) \land A \in J) \to A \subseteq ℂ$
36	33 34 35	sylancr	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to A \subseteq ℂ$
37		dvres2	$⊢ ((ℂ \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq ℂ \land S \subseteq ℂ)) \to {F_{ℂ}^{'} ↾}_{S} \subseteq S D ({F ↾}_{S})$
38	32 5 36 4 37	syl22anc	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to {F_{ℂ}^{'} ↾}_{S} \subseteq S D ({F ↾}_{S})$
39		funssres	$⊢ (Fun {({F ↾}_{S})}_{S}^{'} \land {F_{ℂ}^{'} ↾}_{S} \subseteq S D ({F ↾}_{S})) \to {{({F ↾}_{S})}_{S}^{'} ↾}_{dom ({F_{ℂ}^{'} ↾}_{S})} = {F_{ℂ}^{'} ↾}_{S}$
40	31 38 39	syl2anc	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to {{({F ↾}_{S})}_{S}^{'} ↾}_{dom ({F_{ℂ}^{'} ↾}_{S})} = {F_{ℂ}^{'} ↾}_{S}$
41	28 40	eqtr3d	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \in J \land dom F_{ℂ}^{'} = A)) \to S D ({F ↾}_{S}) = {F_{ℂ}^{'} ↾}_{S}$

Metamath Proof Explorer

Theorem dvres3a

Proof