Theorem stoweidlem30

Description: This lemma is used to prove the existence of a function p as in Lemma 1 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	stoweidlem30.1	⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
	stoweidlem30.2	⊢ 𝑃 = ( 𝑡 ∈ 𝑇 ↦ ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
	stoweidlem30.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	stoweidlem30.4	⊢ ( 𝜑 → 𝐺 : ( 1 ... 𝑀 ) ⟶ 𝑄 )
	stoweidlem30.5	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
Assertion	stoweidlem30	⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → ( 𝑃 ‘ 𝑆 ) = ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem30.1	⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
2		stoweidlem30.2	⊢ 𝑃 = ( 𝑡 ∈ 𝑇 ↦ ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
3		stoweidlem30.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4		stoweidlem30.4	⊢ ( 𝜑 → 𝐺 : ( 1 ... 𝑀 ) ⟶ 𝑄 )
5		stoweidlem30.5	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
6		eleq1	⊢ ( 𝑠 = 𝑆 → ( 𝑠 ∈ 𝑇 ↔ 𝑆 ∈ 𝑇 ) )
7	6	anbi2d	⊢ ( 𝑠 = 𝑆 → ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ↔ ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) ) )
8		fveq2	⊢ ( 𝑠 = 𝑆 → ( 𝑃 ‘ 𝑠 ) = ( 𝑃 ‘ 𝑆 ) )
9		fveq2	⊢ ( 𝑠 = 𝑆 → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) = ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) )
10	9	sumeq2sdv	⊢ ( 𝑠 = 𝑆 → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) = Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) )
11	10	oveq2d	⊢ ( 𝑠 = 𝑆 → ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) ) = ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ) )
12	8 11	eqeq12d	⊢ ( 𝑠 = 𝑆 → ( ( 𝑃 ‘ 𝑠 ) = ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) ) ↔ ( 𝑃 ‘ 𝑆 ) = ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ) ) )
13	7 12	imbi12d	⊢ ( 𝑠 = 𝑆 → ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) → ( 𝑃 ‘ 𝑠 ) = ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) ) ) ↔ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → ( 𝑃 ‘ 𝑆 ) = ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ) ) ) )
14		fveq2	⊢ ( 𝑡 = 𝑠 → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) = ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) )
15	14	sumeq2sdv	⊢ ( 𝑡 = 𝑠 → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) = Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) )
16	15	oveq2d	⊢ ( 𝑡 = 𝑠 → ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) ) )
17		simpr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) → 𝑠 ∈ 𝑇 )
18	3	nnrecred	⊢ ( 𝜑 → ( 1 / 𝑀 ) ∈ ℝ )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) → ( 1 / 𝑀 ) ∈ ℝ )
20		fzfid	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) → ( 1 ... 𝑀 ) ∈ Fin )
21	1 4 5	stoweidlem15	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑠 ∈ 𝑇 ) → ( ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) ∧ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) ≤ 1 ) )
22	21	simp1d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑠 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) ∈ ℝ )
23	22	an32s	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) ∈ ℝ )
24	20 23	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) ∈ ℝ )
25	19 24	remulcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) → ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) ) ∈ ℝ )
26	2 16 17 25	fvmptd3	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) → ( 𝑃 ‘ 𝑠 ) = ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) ) )
27	13 26	vtoclg	⊢ ( 𝑆 ∈ 𝑇 → ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → ( 𝑃 ‘ 𝑆 ) = ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ) ) )
28	27	anabsi7	⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → ( 𝑃 ‘ 𝑆 ) = ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ) )