Theorem stoweidlem55

Description: This lemma proves the existence of a function p as in the proof of Lemma 1 in BrosowskiDeutsh p. 90: p is in the subalgebra, such that 0 <= p <= 1, p__(t_0) = 0, and p > 0 on T - U. Here Z is used to represent t_0 in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem55.1	⊢ Ⅎ 𝑡 𝑈
	stoweidlem55.2	⊢ Ⅎ 𝑡 𝜑
	stoweidlem55.3	⊢ 𝐾 = ( topGen ‘ ran (,) )
	stoweidlem55.4	⊢ ( 𝜑 → 𝐽 ∈ Comp )
	stoweidlem55.5	⊢ 𝑇 = ∪ 𝐽
	stoweidlem55.6	⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
	stoweidlem55.7	⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
	stoweidlem55.8	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
	stoweidlem55.9	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
	stoweidlem55.10	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
	stoweidlem55.11	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
	stoweidlem55.12	⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
	stoweidlem55.13	⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
	stoweidlem55.14	⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
	stoweidlem55.15	⊢ 𝑊 = { 𝑤 ∈ 𝐽 ∣ ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } }
Assertion	stoweidlem55	⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem55.1	⊢ Ⅎ 𝑡 𝑈
2		stoweidlem55.2	⊢ Ⅎ 𝑡 𝜑
3		stoweidlem55.3	⊢ 𝐾 = ( topGen ‘ ran (,) )
4		stoweidlem55.4	⊢ ( 𝜑 → 𝐽 ∈ Comp )
5		stoweidlem55.5	⊢ 𝑇 = ∪ 𝐽
6		stoweidlem55.6	⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
7		stoweidlem55.7	⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
8		stoweidlem55.8	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
9		stoweidlem55.9	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
10		stoweidlem55.10	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
11		stoweidlem55.11	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
12		stoweidlem55.12	⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
13		stoweidlem55.13	⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
14		stoweidlem55.14	⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
15		stoweidlem55.15	⊢ 𝑊 = { 𝑤 ∈ 𝐽 ∣ ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } }
16		0re	⊢ 0 ∈ ℝ
17	10	stoweidlem4	⊢ ( ( 𝜑 ∧ 0 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 0 ) ∈ 𝐴 )
18	16 17	mpan2	⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ 0 ) ∈ 𝐴 )
19	18	adantr	⊢ ( ( 𝜑 ∧ ( 𝑇 ∖ 𝑈 ) = ∅ ) → ( 𝑡 ∈ 𝑇 ↦ 0 ) ∈ 𝐴 )
20		nfcv	⊢ Ⅎ 𝑡 𝑇
21	20 1	nfdif	⊢ Ⅎ 𝑡 ( 𝑇 ∖ 𝑈 )
22		nfcv	⊢ Ⅎ 𝑡 ∅
23	21 22	nfeq	⊢ Ⅎ 𝑡 ( 𝑇 ∖ 𝑈 ) = ∅
24	2 23	nfan	⊢ Ⅎ 𝑡 ( 𝜑 ∧ ( 𝑇 ∖ 𝑈 ) = ∅ )
25		0le0	⊢ 0 ≤ 0
26		0cn	⊢ 0 ∈ ℂ
27		eqid	⊢ ( 𝑡 ∈ 𝑇 ↦ 0 ) = ( 𝑡 ∈ 𝑇 ↦ 0 )
28	27	fvmpt2	⊢ ( ( 𝑡 ∈ 𝑇 ∧ 0 ∈ ℂ ) → ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) = 0 )
29	26 28	mpan2	⊢ ( 𝑡 ∈ 𝑇 → ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) = 0 )
30	25 29	breqtrrid	⊢ ( 𝑡 ∈ 𝑇 → 0 ≤ ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) )
31	30	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑇 ∖ 𝑈 ) = ∅ ) ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) )
32		0le1	⊢ 0 ≤ 1
33	29 32	eqbrtrdi	⊢ ( 𝑡 ∈ 𝑇 → ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ≤ 1 )
34	33	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑇 ∖ 𝑈 ) = ∅ ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ≤ 1 )
35	31 34	jca	⊢ ( ( ( 𝜑 ∧ ( 𝑇 ∖ 𝑈 ) = ∅ ) ∧ 𝑡 ∈ 𝑇 ) → ( 0 ≤ ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ∧ ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ≤ 1 ) )
36	35	ex	⊢ ( ( 𝜑 ∧ ( 𝑇 ∖ 𝑈 ) = ∅ ) → ( 𝑡 ∈ 𝑇 → ( 0 ≤ ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ∧ ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ≤ 1 ) ) )
37	24 36	ralrimi	⊢ ( ( 𝜑 ∧ ( 𝑇 ∖ 𝑈 ) = ∅ ) → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ∧ ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ≤ 1 ) )
38	13 12	jca	⊢ ( 𝜑 → ( 𝑍 ∈ 𝑈 ∧ 𝑈 ∈ 𝐽 ) )
39		elunii	⊢ ( ( 𝑍 ∈ 𝑈 ∧ 𝑈 ∈ 𝐽 ) → 𝑍 ∈ ∪ 𝐽 )
40	39 5	eleqtrrdi	⊢ ( ( 𝑍 ∈ 𝑈 ∧ 𝑈 ∈ 𝐽 ) → 𝑍 ∈ 𝑇 )
41		eqidd	⊢ ( 𝑡 = 𝑍 → 0 = 0 )
42		c0ex	⊢ 0 ∈ V
43	41 27 42	fvmpt	⊢ ( 𝑍 ∈ 𝑇 → ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑍 ) = 0 )
44	38 40 43	3syl	⊢ ( 𝜑 → ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑍 ) = 0 )
45	44	adantr	⊢ ( ( 𝜑 ∧ ( 𝑇 ∖ 𝑈 ) = ∅ ) → ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑍 ) = 0 )
46	23	rzalf	⊢ ( ( 𝑇 ∖ 𝑈 ) = ∅ → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) )
47	46	adantl	⊢ ( ( 𝜑 ∧ ( 𝑇 ∖ 𝑈 ) = ∅ ) → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) )
48		nfcv	⊢ Ⅎ 𝑡 𝑝
49		nfmpt1	⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ 0 )
50	48 49	nfeq	⊢ Ⅎ 𝑡 𝑝 = ( 𝑡 ∈ 𝑇 ↦ 0 )
51		fveq1	⊢ ( 𝑝 = ( 𝑡 ∈ 𝑇 ↦ 0 ) → ( 𝑝 ‘ 𝑡 ) = ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) )
52	51	breq2d	⊢ ( 𝑝 = ( 𝑡 ∈ 𝑇 ↦ 0 ) → ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ↔ 0 ≤ ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ) )
53	51	breq1d	⊢ ( 𝑝 = ( 𝑡 ∈ 𝑇 ↦ 0 ) → ( ( 𝑝 ‘ 𝑡 ) ≤ 1 ↔ ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ≤ 1 ) )
54	52 53	anbi12d	⊢ ( 𝑝 = ( 𝑡 ∈ 𝑇 ↦ 0 ) → ( ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ∧ ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ≤ 1 ) ) )
55	50 54	ralbid	⊢ ( 𝑝 = ( 𝑡 ∈ 𝑇 ↦ 0 ) → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ∧ ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ≤ 1 ) ) )
56		fveq1	⊢ ( 𝑝 = ( 𝑡 ∈ 𝑇 ↦ 0 ) → ( 𝑝 ‘ 𝑍 ) = ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑍 ) )
57	56	eqeq1d	⊢ ( 𝑝 = ( 𝑡 ∈ 𝑇 ↦ 0 ) → ( ( 𝑝 ‘ 𝑍 ) = 0 ↔ ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑍 ) = 0 ) )
58	51	breq2d	⊢ ( 𝑝 = ( 𝑡 ∈ 𝑇 ↦ 0 ) → ( 0 < ( 𝑝 ‘ 𝑡 ) ↔ 0 < ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ) )
59	50 58	ralbid	⊢ ( 𝑝 = ( 𝑡 ∈ 𝑇 ↦ 0 ) → ( ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ↔ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ) )
60	55 57 59	3anbi123d	⊢ ( 𝑝 = ( 𝑡 ∈ 𝑇 ↦ 0 ) → ( ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ↔ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ∧ ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ≤ 1 ) ∧ ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ) ) )
61	60	rspcev	⊢ ( ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ∧ ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ≤ 1 ) ∧ ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( ( 𝑡 ∈ 𝑇 ↦ 0 ) ‘ 𝑡 ) ) ) → ∃ 𝑝 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) )
62	19 37 45 47 61	syl13anc	⊢ ( ( 𝜑 ∧ ( 𝑇 ∖ 𝑈 ) = ∅ ) → ∃ 𝑝 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) )
63	23	nfn	⊢ Ⅎ 𝑡 ¬ ( 𝑇 ∖ 𝑈 ) = ∅
64	2 63	nfan	⊢ Ⅎ 𝑡 ( 𝜑 ∧ ¬ ( 𝑇 ∖ 𝑈 ) = ∅ )
65	4	adantr	⊢ ( ( 𝜑 ∧ ¬ ( 𝑇 ∖ 𝑈 ) = ∅ ) → 𝐽 ∈ Comp )
66	7	adantr	⊢ ( ( 𝜑 ∧ ¬ ( 𝑇 ∖ 𝑈 ) = ∅ ) → 𝐴 ⊆ 𝐶 )
67	8	3adant1r	⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑇 ∖ 𝑈 ) = ∅ ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
68	9	3adant1r	⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑇 ∖ 𝑈 ) = ∅ ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
69	10	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑇 ∖ 𝑈 ) = ∅ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
70	11	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑇 ∖ 𝑈 ) = ∅ ) ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
71	12	adantr	⊢ ( ( 𝜑 ∧ ¬ ( 𝑇 ∖ 𝑈 ) = ∅ ) → 𝑈 ∈ 𝐽 )
72		neqne	⊢ ( ¬ ( 𝑇 ∖ 𝑈 ) = ∅ → ( 𝑇 ∖ 𝑈 ) ≠ ∅ )
73	72	adantl	⊢ ( ( 𝜑 ∧ ¬ ( 𝑇 ∖ 𝑈 ) = ∅ ) → ( 𝑇 ∖ 𝑈 ) ≠ ∅ )
74	13	adantr	⊢ ( ( 𝜑 ∧ ¬ ( 𝑇 ∖ 𝑈 ) = ∅ ) → 𝑍 ∈ 𝑈 )
75	1 64 3 14 15 5 6 65 66 67 68 69 70 71 73 74	stoweidlem53	⊢ ( ( 𝜑 ∧ ¬ ( 𝑇 ∖ 𝑈 ) = ∅ ) → ∃ 𝑝 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) )
76	62 75	pm2.61dan	⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) )