# Metamath Proof Explorer

## Theorem stoweidlem44

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 to represent t_0 in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem44.1 ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}{\phi }$
stoweidlem44.2 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{\phi }$
stoweidlem44.3 ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
stoweidlem44.4 ${⊢}{Q}=\left\{{h}\in {A}|\left({h}\left({Z}\right)=0\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {h}\left({t}\right)\wedge {h}\left({t}\right)\le 1\right)\right)\right\}$
stoweidlem44.5 ${⊢}{P}=\left({t}\in {T}⟼\left(\frac{1}{{M}}\right)\sum _{{i}=1}^{{M}}{G}\left({i}\right)\left({t}\right)\right)$
stoweidlem44.6 ${⊢}{\phi }\to {M}\in ℕ$
stoweidlem44.7 ${⊢}{\phi }\to {G}:\left(1\dots {M}\right)⟶{Q}$
stoweidlem44.8 ${⊢}{\phi }\to \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}\exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}0<{G}\left({j}\right)\left({t}\right)$
stoweidlem44.9 ${⊢}{T}=\bigcup {J}$
stoweidlem44.10 ${⊢}{\phi }\to {A}\subseteq {J}\mathrm{Cn}{K}$
stoweidlem44.11 ${⊢}\left({\phi }\wedge {f}\in {A}\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right)+{g}\left({t}\right)\right)\in {A}$
stoweidlem44.12 ${⊢}\left({\phi }\wedge {f}\in {A}\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)\in {A}$
stoweidlem44.13 ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({t}\in {T}⟼{x}\right)\in {A}$
stoweidlem44.14 ${⊢}{\phi }\to {Z}\in {T}$
Assertion stoweidlem44 ${⊢}{\phi }\to \exists {p}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {p}\left({t}\right)\wedge {p}\left({t}\right)\le 1\right)\wedge {p}\left({Z}\right)=0\wedge \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}0<{p}\left({t}\right)\right)$

### Proof

Step Hyp Ref Expression
1 stoweidlem44.1 ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}{\phi }$
2 stoweidlem44.2 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{\phi }$
3 stoweidlem44.3 ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
4 stoweidlem44.4 ${⊢}{Q}=\left\{{h}\in {A}|\left({h}\left({Z}\right)=0\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {h}\left({t}\right)\wedge {h}\left({t}\right)\le 1\right)\right)\right\}$
5 stoweidlem44.5 ${⊢}{P}=\left({t}\in {T}⟼\left(\frac{1}{{M}}\right)\sum _{{i}=1}^{{M}}{G}\left({i}\right)\left({t}\right)\right)$
6 stoweidlem44.6 ${⊢}{\phi }\to {M}\in ℕ$
7 stoweidlem44.7 ${⊢}{\phi }\to {G}:\left(1\dots {M}\right)⟶{Q}$
8 stoweidlem44.8 ${⊢}{\phi }\to \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}\exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}0<{G}\left({j}\right)\left({t}\right)$
9 stoweidlem44.9 ${⊢}{T}=\bigcup {J}$
10 stoweidlem44.10 ${⊢}{\phi }\to {A}\subseteq {J}\mathrm{Cn}{K}$
11 stoweidlem44.11 ${⊢}\left({\phi }\wedge {f}\in {A}\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right)+{g}\left({t}\right)\right)\in {A}$
12 stoweidlem44.12 ${⊢}\left({\phi }\wedge {f}\in {A}\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)\in {A}$
13 stoweidlem44.13 ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({t}\in {T}⟼{x}\right)\in {A}$
14 stoweidlem44.14 ${⊢}{\phi }\to {Z}\in {T}$
15 eqid ${⊢}\left({t}\in {T}⟼\sum _{{i}=1}^{{M}}{G}\left({i}\right)\left({t}\right)\right)=\left({t}\in {T}⟼\sum _{{i}=1}^{{M}}{G}\left({i}\right)\left({t}\right)\right)$
16 eqid ${⊢}\left({t}\in {T}⟼\frac{1}{{M}}\right)=\left({t}\in {T}⟼\frac{1}{{M}}\right)$
17 6 nnrecred ${⊢}{\phi }\to \frac{1}{{M}}\in ℝ$
18 ssrab2 ${⊢}\left\{{h}\in {A}|\left({h}\left({Z}\right)=0\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {h}\left({t}\right)\wedge {h}\left({t}\right)\le 1\right)\right)\right\}\subseteq {A}$
19 4 18 eqsstri ${⊢}{Q}\subseteq {A}$
20 fss ${⊢}\left({G}:\left(1\dots {M}\right)⟶{Q}\wedge {Q}\subseteq {A}\right)\to {G}:\left(1\dots {M}\right)⟶{A}$
21 7 19 20 sylancl ${⊢}{\phi }\to {G}:\left(1\dots {M}\right)⟶{A}$
22 eqid ${⊢}{J}\mathrm{Cn}{K}={J}\mathrm{Cn}{K}$
23 10 sselda ${⊢}\left({\phi }\wedge {f}\in {A}\right)\to {f}\in \left({J}\mathrm{Cn}{K}\right)$
24 3 9 22 23 fcnre ${⊢}\left({\phi }\wedge {f}\in {A}\right)\to {f}:{T}⟶ℝ$
25 2 5 15 16 6 17 21 11 12 13 24 stoweidlem32 ${⊢}{\phi }\to {P}\in {A}$
26 4 5 6 7 24 stoweidlem38 ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to \left(0\le {P}\left({t}\right)\wedge {P}\left({t}\right)\le 1\right)$
27 26 ex ${⊢}{\phi }\to \left({t}\in {T}\to \left(0\le {P}\left({t}\right)\wedge {P}\left({t}\right)\le 1\right)\right)$
28 2 27 ralrimi ${⊢}{\phi }\to \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {P}\left({t}\right)\wedge {P}\left({t}\right)\le 1\right)$
29 4 5 6 7 24 14 stoweidlem37 ${⊢}{\phi }\to {P}\left({Z}\right)=0$
30 nfv ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}{t}\in \left({T}\setminus {U}\right)$
31 1 30 nfan ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)$
32 nfv ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}0<\left(\frac{1}{{M}}\right)\sum _{{i}=1}^{{M}}{G}\left({i}\right)\left({t}\right)$
33 8 r19.21bi ${⊢}\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\to \exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}0<{G}\left({j}\right)\left({t}\right)$
34 df-rex ${⊢}\exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}0<{G}\left({j}\right)\left({t}\right)↔\exists {j}\phantom{\rule{.4em}{0ex}}\left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)$
35 33 34 sylib ${⊢}\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\to \exists {j}\phantom{\rule{.4em}{0ex}}\left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)$
36 17 ad2antrr ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to \frac{1}{{M}}\in ℝ$
37 simpll ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to {\phi }$
38 eldifi ${⊢}{t}\in \left({T}\setminus {U}\right)\to {t}\in {T}$
39 38 ad2antlr ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to {t}\in {T}$
40 fzfid ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to \left(1\dots {M}\right)\in \mathrm{Fin}$
41 4 7 24 stoweidlem15 ${⊢}\left(\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\wedge {t}\in {T}\right)\to \left({G}\left({i}\right)\left({t}\right)\in ℝ\wedge 0\le {G}\left({i}\right)\left({t}\right)\wedge {G}\left({i}\right)\left({t}\right)\le 1\right)$
42 41 an32s ${⊢}\left(\left({\phi }\wedge {t}\in {T}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to \left({G}\left({i}\right)\left({t}\right)\in ℝ\wedge 0\le {G}\left({i}\right)\left({t}\right)\wedge {G}\left({i}\right)\left({t}\right)\le 1\right)$
43 42 simp1d ${⊢}\left(\left({\phi }\wedge {t}\in {T}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to {G}\left({i}\right)\left({t}\right)\in ℝ$
44 40 43 fsumrecl ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to \sum _{{i}=1}^{{M}}{G}\left({i}\right)\left({t}\right)\in ℝ$
45 37 39 44 syl2anc ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to \sum _{{i}=1}^{{M}}{G}\left({i}\right)\left({t}\right)\in ℝ$
46 6 nnred ${⊢}{\phi }\to {M}\in ℝ$
47 6 nngt0d ${⊢}{\phi }\to 0<{M}$
48 46 47 recgt0d ${⊢}{\phi }\to 0<\frac{1}{{M}}$
49 48 ad2antrr ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to 0<\frac{1}{{M}}$
50 0red ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to 0\in ℝ$
51 simprl ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to {j}\in \left(1\dots {M}\right)$
52 37 51 39 3jca ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to \left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {T}\right)$
53 snfi ${⊢}\left\{{j}\right\}\in \mathrm{Fin}$
54 53 a1i ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {T}\right)\to \left\{{j}\right\}\in \mathrm{Fin}$
55 simpl1 ${⊢}\left(\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {T}\right)\wedge {i}\in \left\{{j}\right\}\right)\to {\phi }$
56 simpl3 ${⊢}\left(\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {T}\right)\wedge {i}\in \left\{{j}\right\}\right)\to {t}\in {T}$
57 elsni ${⊢}{i}\in \left\{{j}\right\}\to {i}={j}$
58 57 adantl ${⊢}\left(\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {T}\right)\wedge {i}\in \left\{{j}\right\}\right)\to {i}={j}$
59 simpl2 ${⊢}\left(\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {T}\right)\wedge {i}\in \left\{{j}\right\}\right)\to {j}\in \left(1\dots {M}\right)$
60 58 59 eqeltrd ${⊢}\left(\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {T}\right)\wedge {i}\in \left\{{j}\right\}\right)\to {i}\in \left(1\dots {M}\right)$
61 55 56 60 43 syl21anc ${⊢}\left(\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {T}\right)\wedge {i}\in \left\{{j}\right\}\right)\to {G}\left({i}\right)\left({t}\right)\in ℝ$
62 54 61 fsumrecl ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {T}\right)\to \sum _{{i}\in \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)\in ℝ$
63 52 62 syl ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to \sum _{{i}\in \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)\in ℝ$
64 50 63 readdcld ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to 0+\sum _{{i}\in \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)\in ℝ$
65 fzfi ${⊢}\left(1\dots {M}\right)\in \mathrm{Fin}$
66 diffi ${⊢}\left(1\dots {M}\right)\in \mathrm{Fin}\to \left(1\dots {M}\right)\setminus \left\{{j}\right\}\in \mathrm{Fin}$
67 65 66 mp1i ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to \left(1\dots {M}\right)\setminus \left\{{j}\right\}\in \mathrm{Fin}$
68 eldifi ${⊢}{i}\in \left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\to {i}\in \left(1\dots {M}\right)$
69 68 43 sylan2 ${⊢}\left(\left({\phi }\wedge {t}\in {T}\right)\wedge {i}\in \left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\right)\to {G}\left({i}\right)\left({t}\right)\in ℝ$
70 67 69 fsumrecl ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to \sum _{{i}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)\in ℝ$
71 37 39 70 syl2anc ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to \sum _{{i}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)\in ℝ$
72 71 63 readdcld ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to \sum _{{i}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)+\sum _{{i}\in \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)\in ℝ$
73 00id ${⊢}0+0=0$
74 simprr ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to 0<{G}\left({j}\right)\left({t}\right)$
75 4 7 24 stoweidlem15 ${⊢}\left(\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\wedge {t}\in {T}\right)\to \left({G}\left({j}\right)\left({t}\right)\in ℝ\wedge 0\le {G}\left({j}\right)\left({t}\right)\wedge {G}\left({j}\right)\left({t}\right)\le 1\right)$
76 75 simp1d ${⊢}\left(\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\wedge {t}\in {T}\right)\to {G}\left({j}\right)\left({t}\right)\in ℝ$
77 37 51 39 76 syl21anc ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to {G}\left({j}\right)\left({t}\right)\in ℝ$
78 77 recnd ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to {G}\left({j}\right)\left({t}\right)\in ℂ$
79 fveq2 ${⊢}{i}={j}\to {G}\left({i}\right)={G}\left({j}\right)$
80 79 fveq1d ${⊢}{i}={j}\to {G}\left({i}\right)\left({t}\right)={G}\left({j}\right)\left({t}\right)$
81 80 sumsn ${⊢}\left({j}\in \left(1\dots {M}\right)\wedge {G}\left({j}\right)\left({t}\right)\in ℂ\right)\to \sum _{{i}\in \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)={G}\left({j}\right)\left({t}\right)$
82 51 78 81 syl2anc ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to \sum _{{i}\in \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)={G}\left({j}\right)\left({t}\right)$
83 74 82 breqtrrd ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to 0<\sum _{{i}\in \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)$
84 50 63 50 83 ltadd2dd ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to 0+0<0+\sum _{{i}\in \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)$
85 73 84 eqbrtrrid ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to 0<0+\sum _{{i}\in \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)$
86 0red ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {T}\right)\to 0\in ℝ$
87 70 3adant2 ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {T}\right)\to \sum _{{i}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)\in ℝ$
88 simpll ${⊢}\left(\left({\phi }\wedge {t}\in {T}\right)\wedge {i}\in \left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\right)\to {\phi }$
89 68 adantl ${⊢}\left(\left({\phi }\wedge {t}\in {T}\right)\wedge {i}\in \left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\right)\to {i}\in \left(1\dots {M}\right)$
90 simplr ${⊢}\left(\left({\phi }\wedge {t}\in {T}\right)\wedge {i}\in \left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\right)\to {t}\in {T}$
91 88 89 90 41 syl21anc ${⊢}\left(\left({\phi }\wedge {t}\in {T}\right)\wedge {i}\in \left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\right)\to \left({G}\left({i}\right)\left({t}\right)\in ℝ\wedge 0\le {G}\left({i}\right)\left({t}\right)\wedge {G}\left({i}\right)\left({t}\right)\le 1\right)$
92 91 simp2d ${⊢}\left(\left({\phi }\wedge {t}\in {T}\right)\wedge {i}\in \left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\right)\to 0\le {G}\left({i}\right)\left({t}\right)$
93 67 69 92 fsumge0 ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to 0\le \sum _{{i}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)$
94 93 3adant2 ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {T}\right)\to 0\le \sum _{{i}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)$
95 86 87 62 94 leadd1dd ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {T}\right)\to 0+\sum _{{i}\in \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)\le \sum _{{i}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)+\sum _{{i}\in \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)$
96 52 95 syl ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to 0+\sum _{{i}\in \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)\le \sum _{{i}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)+\sum _{{i}\in \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)$
97 50 64 72 85 96 ltletrd ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to 0<\sum _{{i}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)+\sum _{{i}\in \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)$
98 eldifn ${⊢}{x}\in \left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\to ¬{x}\in \left\{{j}\right\}$
99 imnan ${⊢}\left({x}\in \left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\to ¬{x}\in \left\{{j}\right\}\right)↔¬\left({x}\in \left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\wedge {x}\in \left\{{j}\right\}\right)$
100 98 99 mpbi ${⊢}¬\left({x}\in \left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\wedge {x}\in \left\{{j}\right\}\right)$
101 elin ${⊢}{x}\in \left(\left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\cap \left\{{j}\right\}\right)↔\left({x}\in \left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\wedge {x}\in \left\{{j}\right\}\right)$
102 100 101 mtbir ${⊢}¬{x}\in \left(\left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\cap \left\{{j}\right\}\right)$
103 102 nel0 ${⊢}\left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\cap \left\{{j}\right\}=\varnothing$
104 103 a1i ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {T}\right)\to \left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\cap \left\{{j}\right\}=\varnothing$
105 undif1 ${⊢}\left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\cup \left\{{j}\right\}=\left(1\dots {M}\right)\cup \left\{{j}\right\}$
106 snssi ${⊢}{j}\in \left(1\dots {M}\right)\to \left\{{j}\right\}\subseteq \left(1\dots {M}\right)$
107 106 3ad2ant2 ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {T}\right)\to \left\{{j}\right\}\subseteq \left(1\dots {M}\right)$
108 ssequn2 ${⊢}\left\{{j}\right\}\subseteq \left(1\dots {M}\right)↔\left(1\dots {M}\right)\cup \left\{{j}\right\}=\left(1\dots {M}\right)$
109 107 108 sylib ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {T}\right)\to \left(1\dots {M}\right)\cup \left\{{j}\right\}=\left(1\dots {M}\right)$
110 105 109 syl5req ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {T}\right)\to \left(1\dots {M}\right)=\left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\cup \left\{{j}\right\}$
111 fzfid ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {T}\right)\to \left(1\dots {M}\right)\in \mathrm{Fin}$
112 43 3adantl2 ${⊢}\left(\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {T}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to {G}\left({i}\right)\left({t}\right)\in ℝ$
113 112 recnd ${⊢}\left(\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {T}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to {G}\left({i}\right)\left({t}\right)\in ℂ$
114 104 110 111 113 fsumsplit ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {T}\right)\to \sum _{{i}=1}^{{M}}{G}\left({i}\right)\left({t}\right)=\sum _{{i}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)+\sum _{{i}\in \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)$
115 52 114 syl ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to \sum _{{i}=1}^{{M}}{G}\left({i}\right)\left({t}\right)=\sum _{{i}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)+\sum _{{i}\in \left\{{j}\right\}}{G}\left({i}\right)\left({t}\right)$
116 97 115 breqtrrd ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to 0<\sum _{{i}=1}^{{M}}{G}\left({i}\right)\left({t}\right)$
117 36 45 49 116 mulgt0d ${⊢}\left(\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\wedge \left({j}\in \left(1\dots {M}\right)\wedge 0<{G}\left({j}\right)\left({t}\right)\right)\right)\to 0<\left(\frac{1}{{M}}\right)\sum _{{i}=1}^{{M}}{G}\left({i}\right)\left({t}\right)$
118 31 32 35 117 exlimdd ${⊢}\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\to 0<\left(\frac{1}{{M}}\right)\sum _{{i}=1}^{{M}}{G}\left({i}\right)\left({t}\right)$
119 4 5 6 7 24 stoweidlem30 ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to {P}\left({t}\right)=\left(\frac{1}{{M}}\right)\sum _{{i}=1}^{{M}}{G}\left({i}\right)\left({t}\right)$
120 38 119 sylan2 ${⊢}\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\to {P}\left({t}\right)=\left(\frac{1}{{M}}\right)\sum _{{i}=1}^{{M}}{G}\left({i}\right)\left({t}\right)$
121 118 120 breqtrrd ${⊢}\left({\phi }\wedge {t}\in \left({T}\setminus {U}\right)\right)\to 0<{P}\left({t}\right)$
122 121 ex ${⊢}{\phi }\to \left({t}\in \left({T}\setminus {U}\right)\to 0<{P}\left({t}\right)\right)$
123 2 122 ralrimi ${⊢}{\phi }\to \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}0<{P}\left({t}\right)$
124 28 29 123 3jca ${⊢}{\phi }\to \left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {P}\left({t}\right)\wedge {P}\left({t}\right)\le 1\right)\wedge {P}\left({Z}\right)=0\wedge \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}0<{P}\left({t}\right)\right)$
125 eleq1 ${⊢}{p}={P}\to \left({p}\in {A}↔{P}\in {A}\right)$
126 nfmpt1 ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}\left({t}\in {T}⟼\left(\frac{1}{{M}}\right)\sum _{{i}=1}^{{M}}{G}\left({i}\right)\left({t}\right)\right)$
127 5 126 nfcxfr ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}{P}$
128 127 nfeq2 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{p}={P}$
129 fveq1 ${⊢}{p}={P}\to {p}\left({t}\right)={P}\left({t}\right)$
130 129 breq2d ${⊢}{p}={P}\to \left(0\le {p}\left({t}\right)↔0\le {P}\left({t}\right)\right)$
131 129 breq1d ${⊢}{p}={P}\to \left({p}\left({t}\right)\le 1↔{P}\left({t}\right)\le 1\right)$
132 130 131 anbi12d ${⊢}{p}={P}\to \left(\left(0\le {p}\left({t}\right)\wedge {p}\left({t}\right)\le 1\right)↔\left(0\le {P}\left({t}\right)\wedge {P}\left({t}\right)\le 1\right)\right)$
133 128 132 ralbid ${⊢}{p}={P}\to \left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {p}\left({t}\right)\wedge {p}\left({t}\right)\le 1\right)↔\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {P}\left({t}\right)\wedge {P}\left({t}\right)\le 1\right)\right)$
134 fveq1 ${⊢}{p}={P}\to {p}\left({Z}\right)={P}\left({Z}\right)$
135 134 eqeq1d ${⊢}{p}={P}\to \left({p}\left({Z}\right)=0↔{P}\left({Z}\right)=0\right)$
136 129 breq2d ${⊢}{p}={P}\to \left(0<{p}\left({t}\right)↔0<{P}\left({t}\right)\right)$
137 128 136 ralbid ${⊢}{p}={P}\to \left(\forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}0<{p}\left({t}\right)↔\forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}0<{P}\left({t}\right)\right)$
138 133 135 137 3anbi123d ${⊢}{p}={P}\to \left(\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {p}\left({t}\right)\wedge {p}\left({t}\right)\le 1\right)\wedge {p}\left({Z}\right)=0\wedge \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}0<{p}\left({t}\right)\right)↔\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {P}\left({t}\right)\wedge {P}\left({t}\right)\le 1\right)\wedge {P}\left({Z}\right)=0\wedge \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}0<{P}\left({t}\right)\right)\right)$
139 125 138 anbi12d ${⊢}{p}={P}\to \left(\left({p}\in {A}\wedge \left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {p}\left({t}\right)\wedge {p}\left({t}\right)\le 1\right)\wedge {p}\left({Z}\right)=0\wedge \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}0<{p}\left({t}\right)\right)\right)↔\left({P}\in {A}\wedge \left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {P}\left({t}\right)\wedge {P}\left({t}\right)\le 1\right)\wedge {P}\left({Z}\right)=0\wedge \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}0<{P}\left({t}\right)\right)\right)\right)$
140 139 spcegv ${⊢}{P}\in {A}\to \left(\left({P}\in {A}\wedge \left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {P}\left({t}\right)\wedge {P}\left({t}\right)\le 1\right)\wedge {P}\left({Z}\right)=0\wedge \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}0<{P}\left({t}\right)\right)\right)\to \exists {p}\phantom{\rule{.4em}{0ex}}\left({p}\in {A}\wedge \left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {p}\left({t}\right)\wedge {p}\left({t}\right)\le 1\right)\wedge {p}\left({Z}\right)=0\wedge \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}0<{p}\left({t}\right)\right)\right)\right)$
141 25 140 syl ${⊢}{\phi }\to \left(\left({P}\in {A}\wedge \left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {P}\left({t}\right)\wedge {P}\left({t}\right)\le 1\right)\wedge {P}\left({Z}\right)=0\wedge \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}0<{P}\left({t}\right)\right)\right)\to \exists {p}\phantom{\rule{.4em}{0ex}}\left({p}\in {A}\wedge \left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {p}\left({t}\right)\wedge {p}\left({t}\right)\le 1\right)\wedge {p}\left({Z}\right)=0\wedge \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}0<{p}\left({t}\right)\right)\right)\right)$
142 25 124 141 mp2and ${⊢}{\phi }\to \exists {p}\phantom{\rule{.4em}{0ex}}\left({p}\in {A}\wedge \left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {p}\left({t}\right)\wedge {p}\left({t}\right)\le 1\right)\wedge {p}\left({Z}\right)=0\wedge \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}0<{p}\left({t}\right)\right)\right)$
143 df-rex ${⊢}\exists {p}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {p}\left({t}\right)\wedge {p}\left({t}\right)\le 1\right)\wedge {p}\left({Z}\right)=0\wedge \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}0<{p}\left({t}\right)\right)↔\exists {p}\phantom{\rule{.4em}{0ex}}\left({p}\in {A}\wedge \left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {p}\left({t}\right)\wedge {p}\left({t}\right)\le 1\right)\wedge {p}\left({Z}\right)=0\wedge \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}0<{p}\left({t}\right)\right)\right)$
144 142 143 sylibr ${⊢}{\phi }\to \exists {p}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {p}\left({t}\right)\wedge {p}\left({t}\right)\le 1\right)\wedge {p}\left({Z}\right)=0\wedge \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}0<{p}\left({t}\right)\right)$