stoweidlem38

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

Proof

Step	Hyp	Ref	Expression
1		stoweidlem38.1	$⊢ Q = \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
2		stoweidlem38.2	$⊢ P = (t \in T ⟼ (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (t))$
3		stoweidlem38.3	$⊢ φ \to M \in ℕ$
4		stoweidlem38.4	$⊢ φ \to G : (1 \dots M) ⟶ Q$
5		stoweidlem38.5	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
6	3	nnrecred	$⊢ φ \to \frac{1}{M} \in ℝ$
7	6	adantr	$⊢ (φ \land S \in T) \to \frac{1}{M} \in ℝ$
8		fzfid	$⊢ (φ \land S \in T) \to (1 \dots M) \in Fin$
9	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)$
10	9	simp1d	$⊢ ((φ \land i \in (1 \dots M)) \land S \in T) \to G (i) (S) \in ℝ$
11	10	an32s	$⊢ ((φ \land S \in T) \land i \in (1 \dots M)) \to G (i) (S) \in ℝ$
12	8 11	fsumrecl	$⊢ (φ \land S \in T) \to \sum_{i = 1}^{M} G (i) (S) \in ℝ$
13		1red	$⊢ φ \to 1 \in ℝ$
14		0le1	$⊢ 0 \leq 1$
15	14	a1i	$⊢ φ \to 0 \leq 1$
16	3	nnred	$⊢ φ \to M \in ℝ$
17	3	nngt0d	$⊢ φ \to 0 < M$
18		divge0	$⊢ ((1 \in ℝ \land 0 \leq 1) \land (M \in ℝ \land 0 < M)) \to 0 \leq \frac{1}{M}$
19	13 15 16 17 18	syl22anc	$⊢ φ \to 0 \leq \frac{1}{M}$
20	19	adantr	$⊢ (φ \land S \in T) \to 0 \leq \frac{1}{M}$
21	9	simp2d	$⊢ ((φ \land i \in (1 \dots M)) \land S \in T) \to 0 \leq G (i) (S)$
22	21	an32s	$⊢ ((φ \land S \in T) \land i \in (1 \dots M)) \to 0 \leq G (i) (S)$
23	8 11 22	fsumge0	$⊢ (φ \land S \in T) \to 0 \leq \sum_{i = 1}^{M} G (i) (S)$
24	7 12 20 23	mulge0d	$⊢ (φ \land S \in T) \to 0 \leq (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (S)$
25	1 2 3 4 5	stoweidlem30	$⊢ (φ \land S \in T) \to P (S) = (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (S)$
26	24 25	breqtrrd	$⊢ (φ \land S \in T) \to 0 \leq P (S)$
27		1red	$⊢ ((φ \land S \in T) \land i \in (1 \dots M)) \to 1 \in ℝ$
28	9	simp3d	$⊢ ((φ \land i \in (1 \dots M)) \land S \in T) \to G (i) (S) \leq 1$
29	28	an32s	$⊢ ((φ \land S \in T) \land i \in (1 \dots M)) \to G (i) (S) \leq 1$
30	8 11 27 29	fsumle	$⊢ (φ \land S \in T) \to \sum_{i = 1}^{M} G (i) (S) \leq \sum_{i = 1}^{M} 1$
31		fzfid	$⊢ φ \to (1 \dots M) \in Fin$
32		ax-1cn	$⊢ 1 \in ℂ$
33		fsumconst	$⊢ ((1 \dots M) \in Fin \land 1 \in ℂ) \to \sum_{i = 1}^{M} 1 = \|(1 \dots M)\| \cdot 1$
34	31 32 33	sylancl	$⊢ φ \to \sum_{i = 1}^{M} 1 = \|(1 \dots M)\| \cdot 1$
35	3	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
36		hashfz1	$⊢ M \in ℕ_{0} \to \|(1 \dots M)\| = M$
37	35 36	syl	$⊢ φ \to \|(1 \dots M)\| = M$
38	37	oveq1d	$⊢ φ \to \|(1 \dots M)\| \cdot 1 = M \cdot 1$
39	3	nncnd	$⊢ φ \to M \in ℂ$
40	39	mulid1d	$⊢ φ \to M \cdot 1 = M$
41	34 38 40	3eqtrd	$⊢ φ \to \sum_{i = 1}^{M} 1 = M$
42	41	adantr	$⊢ (φ \land S \in T) \to \sum_{i = 1}^{M} 1 = M$
43	30 42	breqtrd	$⊢ (φ \land S \in T) \to \sum_{i = 1}^{M} G (i) (S) \leq M$
44	16	adantr	$⊢ (φ \land S \in T) \to M \in ℝ$
45		1red	$⊢ (φ \land S \in T) \to 1 \in ℝ$
46		0lt1	$⊢ 0 < 1$
47	46	a1i	$⊢ (φ \land S \in T) \to 0 < 1$
48	16 17	jca	$⊢ φ \to (M \in ℝ \land 0 < M)$
49	48	adantr	$⊢ (φ \land S \in T) \to (M \in ℝ \land 0 < M)$
50		divgt0	$⊢ ((1 \in ℝ \land 0 < 1) \land (M \in ℝ \land 0 < M)) \to 0 < \frac{1}{M}$
51	45 47 49 50	syl21anc	$⊢ (φ \land S \in T) \to 0 < \frac{1}{M}$
52		lemul2	$⊢ (\sum_{i = 1}^{M} G (i) (S) \in ℝ \land M \in ℝ \land (\frac{1}{M} \in ℝ \land 0 < \frac{1}{M})) \to (\sum_{i = 1}^{M} G (i) (S) \leq M \leftrightarrow (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (S) \leq (\frac{1}{M}) \cdot M)$
53	12 44 7 51 52	syl112anc	$⊢ (φ \land S \in T) \to (\sum_{i = 1}^{M} G (i) (S) \leq M \leftrightarrow (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (S) \leq (\frac{1}{M}) \cdot M)$
54	43 53	mpbid	$⊢ (φ \land S \in T) \to (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (S) \leq (\frac{1}{M}) \cdot M$
55	25 54	eqbrtrd	$⊢ (φ \land S \in T) \to P (S) \leq (\frac{1}{M}) \cdot M$
56	32	a1i	$⊢ φ \to 1 \in ℂ$
57	3	nnne0d	$⊢ φ \to M \neq 0$
58	56 39 57	3jca	$⊢ φ \to (1 \in ℂ \land M \in ℂ \land M \neq 0)$
59	58	adantr	$⊢ (φ \land S \in T) \to (1 \in ℂ \land M \in ℂ \land M \neq 0)$
60		divcan1	$⊢ (1 \in ℂ \land M \in ℂ \land M \neq 0) \to (\frac{1}{M}) \cdot M = 1$
61	59 60	syl	$⊢ (φ \land S \in T) \to (\frac{1}{M}) \cdot M = 1$
62	55 61	breqtrd	$⊢ (φ \land S \in T) \to P (S) \leq 1$
63	26 62	jca	$⊢ (φ \land S \in T) \to (0 \leq P (S) \land P (S) \leq 1)$

Metamath Proof Explorer

Theorem stoweidlem38

Proof