Metamath Proof Explorer

Theorem 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 e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
stoweidlem38.2 
|- P = ( t e. T |-> ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) ) )
stoweidlem38.3 
|- ( ph -> M e. NN )
stoweidlem38.4 
|- ( ph -> G : ( 1 ... M ) --> Q )
stoweidlem38.5 
|- ( ( ph /\ f e. A ) -> f : T --> RR )
Assertion stoweidlem38 
|- ( ( ph /\ S e. T ) -> ( 0 <_ ( P ` S ) /\ ( P ` S ) <_ 1 ) )

Proof

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