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	⊢ ( 𝜑 → 𝑇 = ∅ )
	stoweidlem9.2	⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ 1 ) ∈ 𝐴 )
Assertion	stoweidlem9	⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝑔 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem9.1	⊢ ( 𝜑 → 𝑇 = ∅ )
2		stoweidlem9.2	⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ 1 ) ∈ 𝐴 )
3		mpteq1	⊢ ( 𝑇 = ∅ → ( 𝑡 ∈ 𝑇 ↦ 1 ) = ( 𝑡 ∈ ∅ ↦ 1 ) )
4		mpt0	⊢ ( 𝑡 ∈ ∅ ↦ 1 ) = ∅
5	3 4	eqtrdi	⊢ ( 𝑇 = ∅ → ( 𝑡 ∈ 𝑇 ↦ 1 ) = ∅ )
6	1 5	syl	⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ 1 ) = ∅ )
7	6 2	eqeltrrd	⊢ ( 𝜑 → ∅ ∈ 𝐴 )
8		rzal	⊢ ( 𝑇 = ∅ → ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ∅ ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 )
9	1 8	syl	⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ∅ ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 )
10		fveq1	⊢ ( 𝑔 = ∅ → ( 𝑔 ‘ 𝑡 ) = ( ∅ ‘ 𝑡 ) )
11	10	fvoveq1d	⊢ ( 𝑔 = ∅ → ( abs ‘ ( ( 𝑔 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) = ( abs ‘ ( ( ∅ ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) )
12	11	breq1d	⊢ ( 𝑔 = ∅ → ( ( abs ‘ ( ( 𝑔 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 ↔ ( abs ‘ ( ( ∅ ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 ) )
13	12	ralbidv	⊢ ( 𝑔 = ∅ → ( ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝑔 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 ↔ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ∅ ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 ) )
14	13	rspcev	⊢ ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ∅ ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 ) → ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝑔 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 )
15	7 9 14	syl2anc	⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝑔 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 )