Metamath Proof Explorer

Theorem stoweidlem30

Description: This lemma is used to prove the existence of a function p as in Lemma 1 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 stoweidlem30.1 
|- Q = { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
stoweidlem30.2 
|- P = ( t e. T |-> ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) ) )
stoweidlem30.3 
|- ( ph -> M e. NN )
stoweidlem30.4 
|- ( ph -> G : ( 1 ... M ) --> Q )
stoweidlem30.5 
|- ( ( ph /\ f e. A ) -> f : T --> RR )
Assertion stoweidlem30 
|- ( ( ph /\ S e. T ) -> ( P ` S ) = ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` S ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem30.1 
 |-  Q = { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
2 stoweidlem30.2 
 |-  P = ( t e. T |-> ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) ) )
3 stoweidlem30.3 
 |-  ( ph -> M e. NN )
4 stoweidlem30.4 
 |-  ( ph -> G : ( 1 ... M ) --> Q )
5 stoweidlem30.5 
 |-  ( ( ph /\ f e. A ) -> f : T --> RR )
6 eleq1 
 |-  ( s = S -> ( s e. T <-> S e. T ) )
7 6 anbi2d 
 |-  ( s = S -> ( ( ph /\ s e. T ) <-> ( ph /\ S e. T ) ) )
8 fveq2 
 |-  ( s = S -> ( P ` s ) = ( P ` S ) )
9 fveq2 
 |-  ( s = S -> ( ( G ` i ) ` s ) = ( ( G ` i ) ` S ) )
10 9 sumeq2sdv 
 |-  ( s = S -> sum_ i e. ( 1 ... M ) ( ( G ` i ) ` s ) = sum_ i e. ( 1 ... M ) ( ( G ` i ) ` S ) )
11 10 oveq2d 
 |-  ( s = S -> ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` s ) ) = ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` S ) ) )
12 8 11 eqeq12d 
 |-  ( s = S -> ( ( P ` s ) = ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` s ) ) <-> ( P ` S ) = ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` S ) ) ) )
13 7 12 imbi12d 
 |-  ( s = S -> ( ( ( ph /\ s e. T ) -> ( P ` s ) = ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` s ) ) ) <-> ( ( ph /\ S e. T ) -> ( P ` S ) = ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` S ) ) ) ) )
14 fveq2 
 |-  ( t = s -> ( ( G ` i ) ` t ) = ( ( G ` i ) ` s ) )
15 14 sumeq2sdv 
 |-  ( t = s -> sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) = sum_ i e. ( 1 ... M ) ( ( G ` i ) ` s ) )
16 15 oveq2d 
 |-  ( t = s -> ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) ) = ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` s ) ) )
17 simpr 
 |-  ( ( ph /\ s e. T ) -> s e. T )
18 3 nnrecred 
 |-  ( ph -> ( 1 / M ) e. RR )
19 18 adantr 
 |-  ( ( ph /\ s e. T ) -> ( 1 / M ) e. RR )
20 fzfid 
 |-  ( ( ph /\ s e. T ) -> ( 1 ... M ) e. Fin )
21 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 ) )
22 21 simp1d 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ s e. T ) -> ( ( G ` i ) ` s ) e. RR )
23 22 an32s 
 |-  ( ( ( ph /\ s e. T ) /\ i e. ( 1 ... M ) ) -> ( ( G ` i ) ` s ) e. RR )
24 20 23 fsumrecl 
 |-  ( ( ph /\ s e. T ) -> sum_ i e. ( 1 ... M ) ( ( G ` i ) ` s ) e. RR )
25 19 24 remulcld 
 |-  ( ( ph /\ s e. T ) -> ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` s ) ) e. RR )
26 2 16 17 25 fvmptd3 
 |-  ( ( ph /\ s e. T ) -> ( P ` s ) = ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` s ) ) )
27 13 26 vtoclg 
 |-  ( S e. T -> ( ( ph /\ S e. T ) -> ( P ` S ) = ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` S ) ) ) )
28 27 anabsi7 
 |-  ( ( ph /\ S e. T ) -> ( P ` S ) = ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` S ) ) )