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	$⊢ Q = \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
	stoweidlem30.2	$⊢ P = (t \in T ⟼ (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (t))$
	stoweidlem30.3	$⊢ φ \to M \in ℕ$
	stoweidlem30.4	$⊢ φ \to G : (1 \dots M) ⟶ Q$
	stoweidlem30.5	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
Assertion	stoweidlem30	$⊢ (φ \land S \in T) \to P (S) = (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (S)$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem30.1	$⊢ Q = \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
2		stoweidlem30.2	$⊢ P = (t \in T ⟼ (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (t))$
3		stoweidlem30.3	$⊢ φ \to M \in ℕ$
4		stoweidlem30.4	$⊢ φ \to G : (1 \dots M) ⟶ Q$
5		stoweidlem30.5	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
6		eleq1	$⊢ s = S \to (s \in T \leftrightarrow S \in T)$
7	6	anbi2d	$⊢ s = S \to ((φ \land s \in T) \leftrightarrow (φ \land S \in T))$
8		fveq2	$⊢ s = S \to P (s) = P (S)$
9		fveq2	$⊢ s = S \to G (i) (s) = G (i) (S)$
10	9	sumeq2sdv	$⊢ s = S \to \sum_{i = 1}^{M} G (i) (s) = \sum_{i = 1}^{M} G (i) (S)$
11	10	oveq2d	$⊢ s = S \to (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (s) = (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (S)$
12	8 11	eqeq12d	$⊢ s = S \to (P (s) = (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (s) \leftrightarrow P (S) = (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (S))$
13	7 12	imbi12d	$⊢ s = S \to (((φ \land s \in T) \to P (s) = (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (s)) \leftrightarrow ((φ \land S \in T) \to P (S) = (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (S)))$
14		fveq2	$⊢ t = s \to G (i) (t) = G (i) (s)$
15	14	sumeq2sdv	$⊢ t = s \to \sum_{i = 1}^{M} G (i) (t) = \sum_{i = 1}^{M} G (i) (s)$
16	15	oveq2d	$⊢ t = s \to (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (t) = (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (s)$
17		simpr	$⊢ (φ \land s \in T) \to s \in T$
18	3	nnrecred	$⊢ φ \to \frac{1}{M} \in ℝ$
19	18	adantr	$⊢ (φ \land s \in T) \to \frac{1}{M} \in ℝ$
20		fzfid	$⊢ (φ \land s \in T) \to (1 \dots M) \in Fin$
21	1 4 5	stoweidlem15	$⊢ ((φ \land i \in (1 \dots M)) \land s \in T) \to (G (i) (s) \in ℝ \land 0 \leq G (i) (s) \land G (i) (s) \leq 1)$
22	21	simp1d	$⊢ ((φ \land i \in (1 \dots M)) \land s \in T) \to G (i) (s) \in ℝ$
23	22	an32s	$⊢ ((φ \land s \in T) \land i \in (1 \dots M)) \to G (i) (s) \in ℝ$
24	20 23	fsumrecl	$⊢ (φ \land s \in T) \to \sum_{i = 1}^{M} G (i) (s) \in ℝ$
25	19 24	remulcld	$⊢ (φ \land s \in T) \to (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (s) \in ℝ$
26	2 16 17 25	fvmptd3	$⊢ (φ \land s \in T) \to P (s) = (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (s)$
27	13 26	vtoclg	$⊢ S \in T \to ((φ \land S \in T) \to P (S) = (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (S))$
28	27	anabsi7	$⊢ (φ \land S \in T) \to P (S) = (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (S)$

Metamath Proof Explorer

Theorem stoweidlem30

Proof