dvcn

Description: A differentiable function is continuous. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by Mario Carneiro, 7-Sep-2015)

		Ref	Expression
	Assertion	dvcn	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land dom F_{S}^{'} = A) \to F : A \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		simpl2	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land dom F_{S}^{'} = A) \to F : A ⟶ ℂ$
2		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} A = TopOpen (ℂ_{fld}) ↾_{𝑡} A$
3		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
4	2 3	dvcnp2	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land x \in dom F_{S}^{'}) \to F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) CnP TopOpen (ℂ_{fld})) (x)$
5	4	ralrimiva	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to \forall x \in dom F_{S}^{'} F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) CnP TopOpen (ℂ_{fld})) (x)$
6		raleq	$⊢ dom F_{S}^{'} = A \to (\forall x \in dom F_{S}^{'} F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) CnP TopOpen (ℂ_{fld})) (x) \leftrightarrow \forall x \in A F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) CnP TopOpen (ℂ_{fld})) (x))$
7	6	biimpd	$⊢ dom F_{S}^{'} = A \to (\forall x \in dom F_{S}^{'} F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) CnP TopOpen (ℂ_{fld})) (x) \to \forall x \in A F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) CnP TopOpen (ℂ_{fld})) (x))$
8	5 7	mpan9	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land dom F_{S}^{'} = A) \to \forall x \in A F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) CnP TopOpen (ℂ_{fld})) (x)$
9	3	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
10		simpl3	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land dom F_{S}^{'} = A) \to A \subseteq S$
11		simpl1	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land dom F_{S}^{'} = A) \to S \subseteq ℂ$
12	10 11	sstrd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land dom F_{S}^{'} = A) \to A \subseteq ℂ$
13		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land A \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} A \in TopOn (A)$
14	9 12 13	sylancr	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land dom F_{S}^{'} = A) \to TopOpen (ℂ_{fld}) ↾_{𝑡} A \in TopOn (A)$
15		cncnp	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} A \in TopOn (A) \land TopOpen (ℂ_{fld}) \in TopOn (ℂ)) \to (F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) Cn TopOpen (ℂ_{fld})) \leftrightarrow (F : A ⟶ ℂ \land \forall x \in A F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) CnP TopOpen (ℂ_{fld})) (x)))$
16	14 9 15	sylancl	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land dom F_{S}^{'} = A) \to (F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) Cn TopOpen (ℂ_{fld})) \leftrightarrow (F : A ⟶ ℂ \land \forall x \in A F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) CnP TopOpen (ℂ_{fld})) (x)))$
17	1 8 16	mpbir2and	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land dom F_{S}^{'} = A) \to F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) Cn TopOpen (ℂ_{fld}))$
18		ssid	$⊢ ℂ \subseteq ℂ$
19	9	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
20	3 2 19	cncfcn	$⊢ (A \subseteq ℂ \land ℂ \subseteq ℂ) \to A \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} A) Cn TopOpen (ℂ_{fld})$
21	12 18 20	sylancl	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land dom F_{S}^{'} = A) \to A \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} A) Cn TopOpen (ℂ_{fld})$
22	17 21	eleqtrrd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land dom F_{S}^{'} = A) \to F : A \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem dvcn

Proof