dvres3

Description: Restriction of a complex differentiable function to the reals. (Contributed by Mario Carneiro, 10-Feb-2015)

		Ref	Expression
	Assertion	dvres3	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \subseteq ℂ \land S \subseteq dom F_{ℂ}^{'})) \to S D ({F ↾}_{S}) = {F_{ℂ}^{'} ↾}_{S}$

Proof

Step	Hyp	Ref	Expression
1		reldv	$⊢ Rel {({F ↾}_{S})}_{S}^{'}$
2		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
3	2	ad2antrr	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \subseteq ℂ \land S \subseteq dom F_{ℂ}^{'})) \to S \subseteq ℂ$
4		simplr	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \subseteq ℂ \land S \subseteq dom F_{ℂ}^{'})) \to F : A ⟶ ℂ$
5		simprr	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \subseteq ℂ \land S \subseteq dom F_{ℂ}^{'})) \to S \subseteq dom F_{ℂ}^{'}$
6		ssidd	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \subseteq ℂ \land S \subseteq dom F_{ℂ}^{'})) \to ℂ \subseteq ℂ$
7		simprl	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \subseteq ℂ \land S \subseteq dom F_{ℂ}^{'})) \to A \subseteq ℂ$
8	6 4 7	dvbss	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \subseteq ℂ \land S \subseteq dom F_{ℂ}^{'})) \to dom F_{ℂ}^{'} \subseteq A$
9	5 8	sstrd	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \subseteq ℂ \land S \subseteq dom F_{ℂ}^{'})) \to S \subseteq A$
10	4 9	fssresd	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \subseteq ℂ \land S \subseteq dom F_{ℂ}^{'})) \to ({F ↾}_{S}) : S ⟶ ℂ$
11		ssidd	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \subseteq ℂ \land S \subseteq dom F_{ℂ}^{'})) \to S \subseteq S$
12	3 10 11	dvbss	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \subseteq ℂ \land S \subseteq dom F_{ℂ}^{'})) \to dom {({F ↾}_{S})}_{S}^{'} \subseteq S$
13		ssdmres	$⊢ S \subseteq dom F_{ℂ}^{'} \leftrightarrow dom ({F_{ℂ}^{'} ↾}_{S}) = S$
14	5 13	sylib	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \subseteq ℂ \land S \subseteq dom F_{ℂ}^{'})) \to dom ({F_{ℂ}^{'} ↾}_{S}) = S$
15	12 14	sseqtrrd	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \subseteq ℂ \land S \subseteq dom F_{ℂ}^{'})) \to dom {({F ↾}_{S})}_{S}^{'} \subseteq dom ({F_{ℂ}^{'} ↾}_{S})$
16		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})$
17	1 15 16	sylancr	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \subseteq ℂ \land S \subseteq dom F_{ℂ}^{'})) \to {{({F ↾}_{S})}_{S}^{'} ↾}_{dom ({F_{ℂ}^{'} ↾}_{S})} = S D ({F ↾}_{S})$
18		dvfg	$⊢ S \in \{ℝ, ℂ\} \to {({F ↾}_{S})}_{S}^{'} : dom {({F ↾}_{S})}_{S}^{'} ⟶ ℂ$
19	18	ad2antrr	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \subseteq ℂ \land S \subseteq dom F_{ℂ}^{'})) \to {({F ↾}_{S})}_{S}^{'} : dom {({F ↾}_{S})}_{S}^{'} ⟶ ℂ$
20	19	ffund	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \subseteq ℂ \land S \subseteq dom F_{ℂ}^{'})) \to Fun {({F ↾}_{S})}_{S}^{'}$
21		dvres2	$⊢ ((ℂ \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq ℂ \land S \subseteq ℂ)) \to {F_{ℂ}^{'} ↾}_{S} \subseteq S D ({F ↾}_{S})$
22	6 4 7 3 21	syl22anc	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \subseteq ℂ \land S \subseteq dom F_{ℂ}^{'})) \to {F_{ℂ}^{'} ↾}_{S} \subseteq S D ({F ↾}_{S})$
23		funssres	$⊢ (Fun {({F ↾}_{S})}_{S}^{'} \land {F_{ℂ}^{'} ↾}_{S} \subseteq S D ({F ↾}_{S})) \to {{({F ↾}_{S})}_{S}^{'} ↾}_{dom ({F_{ℂ}^{'} ↾}_{S})} = {F_{ℂ}^{'} ↾}_{S}$
24	20 22 23	syl2anc	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \subseteq ℂ \land S \subseteq dom F_{ℂ}^{'})) \to {{({F ↾}_{S})}_{S}^{'} ↾}_{dom ({F_{ℂ}^{'} ↾}_{S})} = {F_{ℂ}^{'} ↾}_{S}$
25	17 24	eqtr3d	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ) \land (A \subseteq ℂ \land S \subseteq dom F_{ℂ}^{'})) \to S D ({F ↾}_{S}) = {F_{ℂ}^{'} ↾}_{S}$

Metamath Proof Explorer

Theorem dvres3

Proof