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 
|- F/ j ph
stoweidlem44.2 
|- F/ t ph
stoweidlem44.3 
|- K = ( topGen ` ran (,) )
stoweidlem44.4 
|- Q = { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
stoweidlem44.5 
|- P = ( t e. T |-> ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) ) )
stoweidlem44.6 
|- ( ph -> M e. NN )
stoweidlem44.7 
|- ( ph -> G : ( 1 ... M ) --> Q )
stoweidlem44.8 
|- ( ph -> A. t e. ( T \ U ) E. j e. ( 1 ... M ) 0 < ( ( G ` j ) ` t ) )
stoweidlem44.9 
|- T = U. J
stoweidlem44.10 
|- ( ph -> A C_ ( J Cn K ) )
stoweidlem44.11 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
stoweidlem44.12 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
stoweidlem44.13 
|- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
stoweidlem44.14 
|- ( ph -> Z e. T )
Assertion stoweidlem44 
|- ( ph -> E. p e. A ( A. t e. T ( 0 <_ ( p ` t ) /\ ( p ` t ) <_ 1 ) /\ ( p ` Z ) = 0 /\ A. t e. ( T \ U ) 0 < ( p ` t ) ) )

Proof

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