# Metamath Proof Explorer

## 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}\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\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 syl6eq ${⊢}{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}\phantom{\rule{.4em}{0ex}}\left|\varnothing \left({t}\right)-{F}\left({t}\right)\right|<{E}$
9 1 8 syl ${⊢}{\phi }\to \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\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}↔\left|\varnothing \left({t}\right)-{F}\left({t}\right)\right|<{E}\right)$
13 12 ralbidv ${⊢}{g}=\varnothing \to \left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left|{g}\left({t}\right)-{F}\left({t}\right)\right|<{E}↔\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left|\varnothing \left({t}\right)-{F}\left({t}\right)\right|<{E}\right)$
14 13 rspcev ${⊢}\left(\varnothing \in {A}\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left|\varnothing \left({t}\right)-{F}\left({t}\right)\right|<{E}\right)\to \exists {g}\in {A}\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left|{g}\left({t}\right)-{F}\left({t}\right)\right|<{E}$
15 7 9 14 syl2anc ${⊢}{\phi }\to \exists {g}\in {A}\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left|{g}\left({t}\right)-{F}\left({t}\right)\right|<{E}$