Theorem stoweidlem9

Description: Lemma for stoweid : here the Stone Weierstrass theorem is proven for the trivial case, T is the empty set. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem9.1	$$⊢\phi \to T=\varnothing$$
	stoweidlem9.2	$$⊢\phi \to \left(t\in T⟼1\right)\in A$$
Assertion	stoweidlem9	$$⊢\phi \to \exists g\in A\forall t\in T\left|g\left(t\right)-F\left(t\right)\right|<E$$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem9.1	$$⊢\phi \to T=\varnothing$$
2		stoweidlem9.2	$$⊢\phi \to \left(t\in T⟼1\right)\in A$$
3		mpteq1	$$⊢T=\varnothing \to \left(t\in T⟼1\right)=\left(t\in \varnothing ⟼1\right)$$
4		mpt0	$$⊢\left(t\in \varnothing ⟼1\right)=\varnothing$$
5	3 4	eqtrdi	$$⊢T=\varnothing \to \left(t\in T⟼1\right)=\varnothing$$
6	1 5	syl	$$⊢\phi \to \left(t\in T⟼1\right)=\varnothing$$
7	6 2	eqeltrrd	$$⊢\phi \to \varnothing \in A$$
8		rzal	$$⊢T=\varnothing \to \forall t\in T\left|\varnothing \left(t\right)-F\left(t\right)\right|<E$$
9	1 8	syl	$$⊢\phi \to \forall t\in T\left|\varnothing \left(t\right)-F\left(t\right)\right|<E$$
10		fveq1	$$⊢g=\varnothing \to g\left(t\right)=\varnothing \left(t\right)$$
11	10	fvoveq1d	$$⊢g=\varnothing \to \left|g\left(t\right)-F\left(t\right)\right|=\left|\varnothing \left(t\right)-F\left(t\right)\right|$$
12	11	breq1d	$$⊢g=\varnothing \to \left(\left|g\left(t\right)-F\left(t\right)\right|<E\leftrightarrow \left|\varnothing \left(t\right)-F\left(t\right)\right|<E\right)$$
13	12	ralbidv	$$⊢g=\varnothing \to \left(\forall t\in T\left|g\left(t\right)-F\left(t\right)\right|<E\leftrightarrow \forall t\in T\left|\varnothing \left(t\right)-F\left(t\right)\right|<E\right)$$
14	13	rspcev	$$⊢\left(\varnothing \in A\wedge \forall t\in T\left|\varnothing \left(t\right)-F\left(t\right)\right|<E\right)\to \exists g\in A\forall t\in T\left|g\left(t\right)-F\left(t\right)\right|<E$$
15	7 9 14	syl2anc	$$⊢\phi \to \exists g\in A\forall t\in T\left|g\left(t\right)-F\left(t\right)\right|<E$$