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	|- ( ph -> T = (/) )
	stoweidlem9.2	|- ( ph -> ( t e. T |-> 1 ) e. A )
Assertion	stoweidlem9	|- ( ph -> E. g e. A A. t e. T ( abs ` ( ( g ` t ) - ( F ` t ) ) ) < E )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem9.1	|- ( ph -> T = (/) )
2		stoweidlem9.2	|- ( ph -> ( t e. T |-> 1 ) e. A )
3		mpteq1	|- ( T = (/) -> ( t e. T |-> 1 ) = ( t e. (/) |-> 1 ) )
4		mpt0	|- ( t e. (/) |-> 1 ) = (/)
5	3 4	eqtrdi	|- ( T = (/) -> ( t e. T |-> 1 ) = (/) )
6	1 5	syl	|- ( ph -> ( t e. T |-> 1 ) = (/) )
7	6 2	eqeltrrd	|- ( ph -> (/) e. A )
8		rzal	|- ( T = (/) -> A. t e. T ( abs ` ( ( (/) ` t ) - ( F ` t ) ) ) < E )
9	1 8	syl	|- ( ph -> A. t e. T ( abs ` ( ( (/) ` t ) - ( F ` t ) ) ) < E )
10		fveq1	|- ( g = (/) -> ( g ` t ) = ( (/) ` t ) )
11	10	fvoveq1d	|- ( g = (/) -> ( abs ` ( ( g ` t ) - ( F ` t ) ) ) = ( abs ` ( ( (/) ` t ) - ( F ` t ) ) ) )
12	11	breq1d	|- ( g = (/) -> ( ( abs ` ( ( g ` t ) - ( F ` t ) ) ) < E <-> ( abs ` ( ( (/) ` t ) - ( F ` t ) ) ) < E ) )
13	12	ralbidv	|- ( g = (/) -> ( A. t e. T ( abs ` ( ( g ` t ) - ( F ` t ) ) ) < E <-> A. t e. T ( abs ` ( ( (/) ` t ) - ( F ` t ) ) ) < E ) )
14	13	rspcev	|- ( ( (/) e. A /\ A. t e. T ( abs ` ( ( (/) ` t ) - ( F ` t ) ) ) < E ) -> E. g e. A A. t e. T ( abs ` ( ( g ` t ) - ( F ` t ) ) ) < E )
15	7 9 14	syl2anc	|- ( ph -> E. g e. A A. t e. T ( abs ` ( ( g ` t ) - ( F ` t ) ) ) < E )