Metamath Proof Explorer

Theorem stoweidlem15

Description: This lemma is used to prove the existence of a function p as in Lemma 1 from BrosowskiDeutsh p. 90: p is in the subalgebra, such that 0 ≤ p ≤ 1, p__(t_0) = 0, and p > 0 on T - U. Here ( GI ) is used to represent p__(t_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem15.1 
|- Q = { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
stoweidlem15.3 
|- ( ph -> G : ( 1 ... M ) --> Q )
stoweidlem15.4 
|- ( ( ph /\ f e. A ) -> f : T --> RR )
Assertion stoweidlem15 
|- ( ( ( ph /\ I e. ( 1 ... M ) ) /\ S e. T ) -> ( ( ( G ` I ) ` S ) e. RR /\ 0 <_ ( ( G ` I ) ` S ) /\ ( ( G ` I ) ` S ) <_ 1 ) )

Proof

Step Hyp Ref Expression
1 stoweidlem15.1 
 |-  Q = { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
2 stoweidlem15.3 
 |-  ( ph -> G : ( 1 ... M ) --> Q )
3 stoweidlem15.4 
 |-  ( ( ph /\ f e. A ) -> f : T --> RR )
4 simpl 
 |-  ( ( ph /\ I e. ( 1 ... M ) ) -> ph )
5 2 ffvelrnda 
 |-  ( ( ph /\ I e. ( 1 ... M ) ) -> ( G ` I ) e. Q )
6 elrabi 
 |-  ( ( G ` I ) e. { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) } -> ( G ` I ) e. A )
7 6 1 eleq2s 
 |-  ( ( G ` I ) e. Q -> ( G ` I ) e. A )
8 5 7 syl 
 |-  ( ( ph /\ I e. ( 1 ... M ) ) -> ( G ` I ) e. A )
9 eleq1 
 |-  ( f = ( G ` I ) -> ( f e. A <-> ( G ` I ) e. A ) )
10 9 anbi2d 
 |-  ( f = ( G ` I ) -> ( ( ph /\ f e. A ) <-> ( ph /\ ( G ` I ) e. A ) ) )
11 feq1 
 |-  ( f = ( G ` I ) -> ( f : T --> RR <-> ( G ` I ) : T --> RR ) )
12 10 11 imbi12d 
 |-  ( f = ( G ` I ) -> ( ( ( ph /\ f e. A ) -> f : T --> RR ) <-> ( ( ph /\ ( G ` I ) e. A ) -> ( G ` I ) : T --> RR ) ) )
13 12 3 vtoclg 
 |-  ( ( G ` I ) e. A -> ( ( ph /\ ( G ` I ) e. A ) -> ( G ` I ) : T --> RR ) )
14 8 13 syl 
 |-  ( ( ph /\ I e. ( 1 ... M ) ) -> ( ( ph /\ ( G ` I ) e. A ) -> ( G ` I ) : T --> RR ) )
15 4 8 14 mp2and 
 |-  ( ( ph /\ I e. ( 1 ... M ) ) -> ( G ` I ) : T --> RR )
16 15 ffvelrnda 
 |-  ( ( ( ph /\ I e. ( 1 ... M ) ) /\ S e. T ) -> ( ( G ` I ) ` S ) e. RR )
17 5 1 eleqtrdi 
 |-  ( ( ph /\ I e. ( 1 ... M ) ) -> ( G ` I ) e. { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) } )
18 fveq1 
 |-  ( h = ( G ` I ) -> ( h ` Z ) = ( ( G ` I ) ` Z ) )
19 18 eqeq1d 
 |-  ( h = ( G ` I ) -> ( ( h ` Z ) = 0 <-> ( ( G ` I ) ` Z ) = 0 ) )
20 fveq1 
 |-  ( h = ( G ` I ) -> ( h ` t ) = ( ( G ` I ) ` t ) )
21 20 breq2d 
 |-  ( h = ( G ` I ) -> ( 0 <_ ( h ` t ) <-> 0 <_ ( ( G ` I ) ` t ) ) )
22 20 breq1d 
 |-  ( h = ( G ` I ) -> ( ( h ` t ) <_ 1 <-> ( ( G ` I ) ` t ) <_ 1 ) )
23 21 22 anbi12d 
 |-  ( h = ( G ` I ) -> ( ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> ( 0 <_ ( ( G ` I ) ` t ) /\ ( ( G ` I ) ` t ) <_ 1 ) ) )
24 23 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 ) ) )
25 19 24 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 ) ) ) )
26 25 elrab 
 |-  ( ( G ` I ) e. { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) } <-> ( ( G ` I ) e. A /\ ( ( ( G ` I ) ` Z ) = 0 /\ A. t e. T ( 0 <_ ( ( G ` I ) ` t ) /\ ( ( G ` I ) ` t ) <_ 1 ) ) ) )
27 17 26 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 ) ) ) )
28 27 simprd 
 |-  ( ( ph /\ I e. ( 1 ... M ) ) -> ( ( ( G ` I ) ` Z ) = 0 /\ A. t e. T ( 0 <_ ( ( G ` I ) ` t ) /\ ( ( G ` I ) ` t ) <_ 1 ) ) )
29 28 simprd 
 |-  ( ( ph /\ I e. ( 1 ... M ) ) -> A. t e. T ( 0 <_ ( ( G ` I ) ` t ) /\ ( ( G ` I ) ` t ) <_ 1 ) )
30 fveq2 
 |-  ( s = t -> ( ( G ` I ) ` s ) = ( ( G ` I ) ` t ) )
31 30 breq2d 
 |-  ( s = t -> ( 0 <_ ( ( G ` I ) ` s ) <-> 0 <_ ( ( G ` I ) ` t ) ) )
32 30 breq1d 
 |-  ( s = t -> ( ( ( G ` I ) ` s ) <_ 1 <-> ( ( G ` I ) ` t ) <_ 1 ) )
33 31 32 anbi12d 
 |-  ( s = t -> ( ( 0 <_ ( ( G ` I ) ` s ) /\ ( ( G ` I ) ` s ) <_ 1 ) <-> ( 0 <_ ( ( G ` I ) ` t ) /\ ( ( G ` I ) ` t ) <_ 1 ) ) )
34 33 cbvralvw 
 |-  ( A. s e. T ( 0 <_ ( ( G ` I ) ` s ) /\ ( ( G ` I ) ` s ) <_ 1 ) <-> A. t e. T ( 0 <_ ( ( G ` I ) ` t ) /\ ( ( G ` I ) ` t ) <_ 1 ) )
35 fveq2 
 |-  ( s = S -> ( ( G ` I ) ` s ) = ( ( G ` I ) ` S ) )
36 35 breq2d 
 |-  ( s = S -> ( 0 <_ ( ( G ` I ) ` s ) <-> 0 <_ ( ( G ` I ) ` S ) ) )
37 35 breq1d 
 |-  ( s = S -> ( ( ( G ` I ) ` s ) <_ 1 <-> ( ( G ` I ) ` S ) <_ 1 ) )
38 36 37 anbi12d 
 |-  ( s = S -> ( ( 0 <_ ( ( G ` I ) ` s ) /\ ( ( G ` I ) ` s ) <_ 1 ) <-> ( 0 <_ ( ( G ` I ) ` S ) /\ ( ( G ` I ) ` S ) <_ 1 ) ) )
39 38 rspccva 
 |-  ( ( A. s e. T ( 0 <_ ( ( G ` I ) ` s ) /\ ( ( G ` I ) ` s ) <_ 1 ) /\ S e. T ) -> ( 0 <_ ( ( G ` I ) ` S ) /\ ( ( G ` I ) ` S ) <_ 1 ) )
40 34 39 sylanbr 
 |-  ( ( A. t e. T ( 0 <_ ( ( G ` I ) ` t ) /\ ( ( G ` I ) ` t ) <_ 1 ) /\ S e. T ) -> ( 0 <_ ( ( G ` I ) ` S ) /\ ( ( G ` I ) ` S ) <_ 1 ) )
41 29 40 sylan 
 |-  ( ( ( ph /\ I e. ( 1 ... M ) ) /\ S e. T ) -> ( 0 <_ ( ( G ` I ) ` S ) /\ ( ( G ` I ) ` S ) <_ 1 ) )
42 41 simpld 
 |-  ( ( ( ph /\ I e. ( 1 ... M ) ) /\ S e. T ) -> 0 <_ ( ( G ` I ) ` S ) )
43 41 simprd 
 |-  ( ( ( ph /\ I e. ( 1 ... M ) ) /\ S e. T ) -> ( ( G ` I ) ` S ) <_ 1 )
44 16 42 43 3jca 
 |-  ( ( ( ph /\ I e. ( 1 ... M ) ) /\ S e. T ) -> ( ( ( G ` I ) ` S ) e. RR /\ 0 <_ ( ( G ` I ) ` S ) /\ ( ( G ` I ) ` S ) <_ 1 ) )