stoweidlem37

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

	Ref	Expression
Hypotheses	stoweidlem37.1	⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
	stoweidlem37.2	⊢ 𝑃 = ( 𝑡 ∈ 𝑇 ↦ ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
	stoweidlem37.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	stoweidlem37.4	⊢ ( 𝜑 → 𝐺 : ( 1 ... 𝑀 ) ⟶ 𝑄 )
	stoweidlem37.5	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
	stoweidlem37.6	⊢ ( 𝜑 → 𝑍 ∈ 𝑇 )
Assertion	stoweidlem37	⊢ ( 𝜑 → ( 𝑃 ‘ 𝑍 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem37.1	⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
2		stoweidlem37.2	⊢ 𝑃 = ( 𝑡 ∈ 𝑇 ↦ ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
3		stoweidlem37.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4		stoweidlem37.4	⊢ ( 𝜑 → 𝐺 : ( 1 ... 𝑀 ) ⟶ 𝑄 )
5		stoweidlem37.5	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
6		stoweidlem37.6	⊢ ( 𝜑 → 𝑍 ∈ 𝑇 )
7	1 2 3 4 5	stoweidlem30	⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝑇 ) → ( 𝑃 ‘ 𝑍 ) = ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑍 ) ) )
8	6 7	mpdan	⊢ ( 𝜑 → ( 𝑃 ‘ 𝑍 ) = ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑍 ) ) )
9	4	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑖 ) ∈ 𝑄 )
10		fveq1	⊢ ( ℎ = ( 𝐺 ‘ 𝑖 ) → ( ℎ ‘ 𝑍 ) = ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑍 ) )
11	10	eqeq1d	⊢ ( ℎ = ( 𝐺 ‘ 𝑖 ) → ( ( ℎ ‘ 𝑍 ) = 0 ↔ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑍 ) = 0 ) )
12		fveq1	⊢ ( ℎ = ( 𝐺 ‘ 𝑖 ) → ( ℎ ‘ 𝑡 ) = ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
13	12	breq2d	⊢ ( ℎ = ( 𝐺 ‘ 𝑖 ) → ( 0 ≤ ( ℎ ‘ 𝑡 ) ↔ 0 ≤ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
14	12	breq1d	⊢ ( ℎ = ( 𝐺 ‘ 𝑖 ) → ( ( ℎ ‘ 𝑡 ) ≤ 1 ↔ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) )
15	13 14	anbi12d	⊢ ( ℎ = ( 𝐺 ‘ 𝑖 ) → ( ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∧ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) ) )
16	15	ralbidv	⊢ ( ℎ = ( 𝐺 ‘ 𝑖 ) → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∧ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) ) )
17	11 16	anbi12d	⊢ ( ℎ = ( 𝐺 ‘ 𝑖 ) → ( ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) ↔ ( ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∧ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) ) ) )
18	17 1	elrab2	⊢ ( ( 𝐺 ‘ 𝑖 ) ∈ 𝑄 ↔ ( ( 𝐺 ‘ 𝑖 ) ∈ 𝐴 ∧ ( ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∧ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) ) ) )
19	9 18	sylib	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐺 ‘ 𝑖 ) ∈ 𝐴 ∧ ( ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∧ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) ) ) )
20	19	simprld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑍 ) = 0 )
21	20	sumeq2dv	⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑍 ) = Σ 𝑖 ∈ ( 1 ... 𝑀 ) 0 )
22		fzfi	⊢ ( 1 ... 𝑀 ) ∈ Fin
23		olc	⊢ ( ( 1 ... 𝑀 ) ∈ Fin → ( ( 1 ... 𝑀 ) ⊆ ( ℤ_≥ ‘ 1 ) ∨ ( 1 ... 𝑀 ) ∈ Fin ) )
24		sumz	⊢ ( ( ( 1 ... 𝑀 ) ⊆ ( ℤ_≥ ‘ 1 ) ∨ ( 1 ... 𝑀 ) ∈ Fin ) → Σ 𝑖 ∈ ( 1 ... 𝑀 ) 0 = 0 )
25	22 23 24	mp2b	⊢ Σ 𝑖 ∈ ( 1 ... 𝑀 ) 0 = 0
26	21 25	eqtrdi	⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑍 ) = 0 )
27	26	oveq2d	⊢ ( 𝜑 → ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑍 ) ) = ( ( 1 / 𝑀 ) · 0 ) )
28	3	nncnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
29	3	nnne0d	⊢ ( 𝜑 → 𝑀 ≠ 0 )
30	28 29	reccld	⊢ ( 𝜑 → ( 1 / 𝑀 ) ∈ ℂ )
31	30	mul01d	⊢ ( 𝜑 → ( ( 1 / 𝑀 ) · 0 ) = 0 )
32	8 27 31	3eqtrd	⊢ ( 𝜑 → ( 𝑃 ‘ 𝑍 ) = 0 )

Metamath Proof Explorer

Theorem stoweidlem37

Proof