Metamath Proof Explorer

Theorem stoweidlem18

Description: This theorem proves Lemma 2 in BrosowskiDeutsh p. 92 when A is empty, the trivial case. Here D is used to denote the set A of Lemma 2, because the variable A is used for the subalgebra. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem18.1 
|- F/_ t D
stoweidlem18.2 
|- F/ t ph
stoweidlem18.3 
|- F = ( t e. T |-> 1 )
stoweidlem18.4 
|- T = U. J
stoweidlem18.5 
|- ( ( ph /\ a e. RR ) -> ( t e. T |-> a ) e. A )
stoweidlem18.6 
|- ( ph -> B e. ( Clsd ` J ) )
stoweidlem18.7 
|- ( ph -> E e. RR+ )
stoweidlem18.8 
|- ( ph -> D = (/) )
Assertion stoweidlem18 
|- ( ph -> E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. D ( x ` t ) < E /\ A. t e. B ( 1 - E ) < ( x ` t ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem18.1 
 |-  F/_ t D
2 stoweidlem18.2 
 |-  F/ t ph
3 stoweidlem18.3 
 |-  F = ( t e. T |-> 1 )
4 stoweidlem18.4 
 |-  T = U. J
5 stoweidlem18.5 
 |-  ( ( ph /\ a e. RR ) -> ( t e. T |-> a ) e. A )
6 stoweidlem18.6 
 |-  ( ph -> B e. ( Clsd ` J ) )
7 stoweidlem18.7 
 |-  ( ph -> E e. RR+ )
8 stoweidlem18.8 
 |-  ( ph -> D = (/) )
9 1re 
 |-  1 e. RR
10 5 stoweidlem4 
 |-  ( ( ph /\ 1 e. RR ) -> ( t e. T |-> 1 ) e. A )
11 9 10 mpan2 
 |-  ( ph -> ( t e. T |-> 1 ) e. A )
12 3 11 eqeltrid 
 |-  ( ph -> F e. A )
13 0le1 
 |-  0 <_ 1
14 simpr 
 |-  ( ( ph /\ t e. T ) -> t e. T )
15 3 fvmpt2 
 |-  ( ( t e. T /\ 1 e. RR ) -> ( F ` t ) = 1 )
16 14 9 15 sylancl 
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) = 1 )
17 13 16 breqtrrid 
 |-  ( ( ph /\ t e. T ) -> 0 <_ ( F ` t ) )
18 1le1 
 |-  1 <_ 1
19 16 18 eqbrtrdi 
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) <_ 1 )
20 17 19 jca 
 |-  ( ( ph /\ t e. T ) -> ( 0 <_ ( F ` t ) /\ ( F ` t ) <_ 1 ) )
21 20 ex 
 |-  ( ph -> ( t e. T -> ( 0 <_ ( F ` t ) /\ ( F ` t ) <_ 1 ) ) )
22 2 21 ralrimi 
 |-  ( ph -> A. t e. T ( 0 <_ ( F ` t ) /\ ( F ` t ) <_ 1 ) )
23 nfcv 
 |-  F/_ t (/)
24 1 23 nfeq 
 |-  F/ t D = (/)
25 24 rzalf 
 |-  ( D = (/) -> A. t e. D ( F ` t ) < E )
26 8 25 syl 
 |-  ( ph -> A. t e. D ( F ` t ) < E )
27 1red 
 |-  ( ph -> 1 e. RR )
28 27 7 ltsubrpd 
 |-  ( ph -> ( 1 - E ) < 1 )
29 28 adantr 
 |-  ( ( ph /\ t e. B ) -> ( 1 - E ) < 1 )
30 4 cldss 
 |-  ( B e. ( Clsd ` J ) -> B C_ T )
31 6 30 syl 
 |-  ( ph -> B C_ T )
32 31 sselda 
 |-  ( ( ph /\ t e. B ) -> t e. T )
33 32 9 15 sylancl 
 |-  ( ( ph /\ t e. B ) -> ( F ` t ) = 1 )
34 29 33 breqtrrd 
 |-  ( ( ph /\ t e. B ) -> ( 1 - E ) < ( F ` t ) )
35 34 ex 
 |-  ( ph -> ( t e. B -> ( 1 - E ) < ( F ` t ) ) )
36 2 35 ralrimi 
 |-  ( ph -> A. t e. B ( 1 - E ) < ( F ` t ) )
37 nfcv 
 |-  F/_ t x
38 nfmpt1 
 |-  F/_ t ( t e. T |-> 1 )
39 3 38 nfcxfr 
 |-  F/_ t F
40 37 39 nfeq 
 |-  F/ t x = F
41 fveq1 
 |-  ( x = F -> ( x ` t ) = ( F ` t ) )
42 41 breq2d 
 |-  ( x = F -> ( 0 <_ ( x ` t ) <-> 0 <_ ( F ` t ) ) )
43 41 breq1d 
 |-  ( x = F -> ( ( x ` t ) <_ 1 <-> ( F ` t ) <_ 1 ) )
44 42 43 anbi12d 
 |-  ( x = F -> ( ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) <-> ( 0 <_ ( F ` t ) /\ ( F ` t ) <_ 1 ) ) )
45 40 44 ralbid 
 |-  ( x = F -> ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) <-> A. t e. T ( 0 <_ ( F ` t ) /\ ( F ` t ) <_ 1 ) ) )
46 41 breq1d 
 |-  ( x = F -> ( ( x ` t ) < E <-> ( F ` t ) < E ) )
47 40 46 ralbid 
 |-  ( x = F -> ( A. t e. D ( x ` t ) < E <-> A. t e. D ( F ` t ) < E ) )
48 41 breq2d 
 |-  ( x = F -> ( ( 1 - E ) < ( x ` t ) <-> ( 1 - E ) < ( F ` t ) ) )
49 40 48 ralbid 
 |-  ( x = F -> ( A. t e. B ( 1 - E ) < ( x ` t ) <-> A. t e. B ( 1 - E ) < ( F ` t ) ) )
50 45 47 49 3anbi123d 
 |-  ( x = F -> ( ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. D ( x ` t ) < E /\ A. t e. B ( 1 - E ) < ( x ` t ) ) <-> ( A. t e. T ( 0 <_ ( F ` t ) /\ ( F ` t ) <_ 1 ) /\ A. t e. D ( F ` t ) < E /\ A. t e. B ( 1 - E ) < ( F ` t ) ) ) )
51 50 rspcev 
 |-  ( ( F e. A /\ ( A. t e. T ( 0 <_ ( F ` t ) /\ ( F ` t ) <_ 1 ) /\ A. t e. D ( F ` t ) < E /\ A. t e. B ( 1 - E ) < ( F ` t ) ) ) -> E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. D ( x ` t ) < E /\ A. t e. B ( 1 - E ) < ( x ` t ) ) )
52 12 22 26 36 51 syl13anc 
 |-  ( ph -> E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. D ( x ` t ) < E /\ A. t e. B ( 1 - E ) < ( x ` t ) ) )