Theorem stoweidlem58

Description: This theorem proves Lemma 2 in BrosowskiDeutsh p. 91. Here D is used to represent the set A of Lemma 2, because here the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem58.1	⊢ Ⅎ 𝑡 𝐷
	stoweidlem58.2	⊢ Ⅎ 𝑡 𝑈
	stoweidlem58.3	⊢ Ⅎ 𝑡 𝜑
	stoweidlem58.4	⊢ 𝐾 = ( topGen ‘ ran (,) )
	stoweidlem58.5	⊢ 𝑇 = ∪ 𝐽
	stoweidlem58.6	⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
	stoweidlem58.7	⊢ ( 𝜑 → 𝐽 ∈ Comp )
	stoweidlem58.8	⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
	stoweidlem58.9	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
	stoweidlem58.10	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
	stoweidlem58.11	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑎 ) ∈ 𝐴 )
	stoweidlem58.12	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
	stoweidlem58.13	⊢ ( 𝜑 → 𝐵 ∈ ( Clsd ‘ 𝐽 ) )
	stoweidlem58.14	⊢ ( 𝜑 → 𝐷 ∈ ( Clsd ‘ 𝐽 ) )
	stoweidlem58.15	⊢ ( 𝜑 → ( 𝐵 ∩ 𝐷 ) = ∅ )
	stoweidlem58.16	⊢ 𝑈 = ( 𝑇 ∖ 𝐵 )
	stoweidlem58.17	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
	stoweidlem58.18	⊢ ( 𝜑 → 𝐸 < ( 1 / 3 ) )
Assertion	stoweidlem58	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem58.1	⊢ Ⅎ 𝑡 𝐷
2		stoweidlem58.2	⊢ Ⅎ 𝑡 𝑈
3		stoweidlem58.3	⊢ Ⅎ 𝑡 𝜑
4		stoweidlem58.4	⊢ 𝐾 = ( topGen ‘ ran (,) )
5		stoweidlem58.5	⊢ 𝑇 = ∪ 𝐽
6		stoweidlem58.6	⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
7		stoweidlem58.7	⊢ ( 𝜑 → 𝐽 ∈ Comp )
8		stoweidlem58.8	⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
9		stoweidlem58.9	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
10		stoweidlem58.10	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
11		stoweidlem58.11	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑎 ) ∈ 𝐴 )
12		stoweidlem58.12	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
13		stoweidlem58.13	⊢ ( 𝜑 → 𝐵 ∈ ( Clsd ‘ 𝐽 ) )
14		stoweidlem58.14	⊢ ( 𝜑 → 𝐷 ∈ ( Clsd ‘ 𝐽 ) )
15		stoweidlem58.15	⊢ ( 𝜑 → ( 𝐵 ∩ 𝐷 ) = ∅ )
16		stoweidlem58.16	⊢ 𝑈 = ( 𝑇 ∖ 𝐵 )
17		stoweidlem58.17	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
18		stoweidlem58.18	⊢ ( 𝜑 → 𝐸 < ( 1 / 3 ) )
19	1	nfeq1	⊢ Ⅎ 𝑡 𝐷 = ∅
20	3 19	nfan	⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝐷 = ∅ )
21		eqid	⊢ ( 𝑡 ∈ 𝑇 ↦ 1 ) = ( 𝑡 ∈ 𝑇 ↦ 1 )
22	11	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐷 = ∅ ) ∧ 𝑎 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑎 ) ∈ 𝐴 )
23	13	adantr	⊢ ( ( 𝜑 ∧ 𝐷 = ∅ ) → 𝐵 ∈ ( Clsd ‘ 𝐽 ) )
24	17	adantr	⊢ ( ( 𝜑 ∧ 𝐷 = ∅ ) → 𝐸 ∈ ℝ+ )
25		simpr	⊢ ( ( 𝜑 ∧ 𝐷 = ∅ ) → 𝐷 = ∅ )
26	1 20 21 5 22 23 24 25	stoweidlem18	⊢ ( ( 𝜑 ∧ 𝐷 = ∅ ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) )
27		nfcv	⊢ Ⅎ 𝑡 ∅
28	1 27	nfne	⊢ Ⅎ 𝑡 𝐷 ≠ ∅
29	3 28	nfan	⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝐷 ≠ ∅ )
30		eqid	⊢ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } = { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) }
31		eqid	⊢ { 𝑤 ∈ 𝐽 ∣ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) } = { 𝑤 ∈ 𝐽 ∣ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) }
32	7	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ≠ ∅ ) → 𝐽 ∈ Comp )
33	8	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ≠ ∅ ) → 𝐴 ⊆ 𝐶 )
34	9	3adant1r	⊢ ( ( ( 𝜑 ∧ 𝐷 ≠ ∅ ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
35	10	3adant1r	⊢ ( ( ( 𝜑 ∧ 𝐷 ≠ ∅ ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
36	11	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐷 ≠ ∅ ) ∧ 𝑎 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑎 ) ∈ 𝐴 )
37	12	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐷 ≠ ∅ ) ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
38	13	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ≠ ∅ ) → 𝐵 ∈ ( Clsd ‘ 𝐽 ) )
39	14	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ≠ ∅ ) → 𝐷 ∈ ( Clsd ‘ 𝐽 ) )
40	15	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ≠ ∅ ) → ( 𝐵 ∩ 𝐷 ) = ∅ )
41		simpr	⊢ ( ( 𝜑 ∧ 𝐷 ≠ ∅ ) → 𝐷 ≠ ∅ )
42	17	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ≠ ∅ ) → 𝐸 ∈ ℝ+ )
43	18	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ≠ ∅ ) → 𝐸 < ( 1 / 3 ) )
44	1 2 29 30 31 4 5 6 16 32 33 34 35 36 37 38 39 40 41 42 43	stoweidlem57	⊢ ( ( 𝜑 ∧ 𝐷 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) )
45	26 44	pm2.61dane	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) )