Metamath Proof Explorer

Theorem stoweidlem37

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

Proof

Step Hyp Ref Expression
1 stoweidlem37.1 
 |-  Q = { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
2 stoweidlem37.2 
 |-  P = ( t e. T |-> ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) ) )
3 stoweidlem37.3 
 |-  ( ph -> M e. NN )
4 stoweidlem37.4 
 |-  ( ph -> G : ( 1 ... M ) --> Q )
5 stoweidlem37.5 
 |-  ( ( ph /\ f e. A ) -> f : T --> RR )
6 stoweidlem37.6 
 |-  ( ph -> Z e. T )
7 1 2 3 4 5 stoweidlem30 
 |-  ( ( ph /\ Z e. T ) -> ( P ` Z ) = ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` Z ) ) )
8 6 7 mpdan 
 |-  ( ph -> ( P ` Z ) = ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` Z ) ) )
9 4 ffvelrnda 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( G ` i ) e. Q )
10 fveq1 
 |-  ( h = ( G ` i ) -> ( h ` Z ) = ( ( G ` i ) ` Z ) )
11 10 eqeq1d 
 |-  ( h = ( G ` i ) -> ( ( h ` Z ) = 0 <-> ( ( G ` i ) ` Z ) = 0 ) )
12 fveq1 
 |-  ( h = ( G ` i ) -> ( h ` t ) = ( ( G ` i ) ` t ) )
13 12 breq2d 
 |-  ( h = ( G ` i ) -> ( 0 <_ ( h ` t ) <-> 0 <_ ( ( G ` i ) ` t ) ) )
14 12 breq1d 
 |-  ( h = ( G ` i ) -> ( ( h ` t ) <_ 1 <-> ( ( G ` i ) ` t ) <_ 1 ) )
15 13 14 anbi12d 
 |-  ( h = ( G ` i ) -> ( ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> ( 0 <_ ( ( G ` i ) ` t ) /\ ( ( G ` i ) ` t ) <_ 1 ) ) )
16 15 ralbidv 
 |-  ( h = ( G ` i ) -> ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> A. t e. T ( 0 <_ ( ( G ` i ) ` t ) /\ ( ( G ` i ) ` t ) <_ 1 ) ) )
17 11 16 anbi12d 
 |-  ( h = ( G ` i ) -> ( ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) <-> ( ( ( G ` i ) ` Z ) = 0 /\ A. t e. T ( 0 <_ ( ( G ` i ) ` t ) /\ ( ( G ` i ) ` t ) <_ 1 ) ) ) )
18 17 1 elrab2 
 |-  ( ( G ` i ) e. Q <-> ( ( G ` i ) e. A /\ ( ( ( G ` i ) ` Z ) = 0 /\ A. t e. T ( 0 <_ ( ( G ` i ) ` t ) /\ ( ( G ` i ) ` t ) <_ 1 ) ) ) )
19 9 18 sylib 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( G ` i ) e. A /\ ( ( ( G ` i ) ` Z ) = 0 /\ A. t e. T ( 0 <_ ( ( G ` i ) ` t ) /\ ( ( G ` i ) ` t ) <_ 1 ) ) ) )
20 19 simprld 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( G ` i ) ` Z ) = 0 )
21 20 sumeq2dv 
 |-  ( ph -> sum_ i e. ( 1 ... M ) ( ( G ` i ) ` Z ) = sum_ i e. ( 1 ... M ) 0 )
22 fzfi 
 |-  ( 1 ... M ) e. Fin
23 olc 
 |-  ( ( 1 ... M ) e. Fin -> ( ( 1 ... M ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... M ) e. Fin ) )
24 sumz 
 |-  ( ( ( 1 ... M ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... M ) e. Fin ) -> sum_ i e. ( 1 ... M ) 0 = 0 )
25 22 23 24 mp2b 
 |-  sum_ i e. ( 1 ... M ) 0 = 0
26 21 25 eqtrdi 
 |-  ( ph -> sum_ i e. ( 1 ... M ) ( ( G ` i ) ` Z ) = 0 )
27 26 oveq2d 
 |-  ( ph -> ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` Z ) ) = ( ( 1 / M ) x. 0 ) )
28 3 nncnd 
 |-  ( ph -> M e. CC )
29 3 nnne0d 
 |-  ( ph -> M =/= 0 )
30 28 29 reccld 
 |-  ( ph -> ( 1 / M ) e. CC )
31 30 mul01d 
 |-  ( ph -> ( ( 1 / M ) x. 0 ) = 0 )
32 8 27 31 3eqtrd 
 |-  ( ph -> ( P ` Z ) = 0 )