Metamath Proof Explorer

Theorem stoweidlem23

Description: This lemma is used to prove the existence of a function p_t as in the beginning of Lemma 1 BrosowskiDeutsh p. 90: for all t in T - U, there exists a function p in the subalgebra, such that p_t ( t_0 ) = 0 , p_t ( t ) > 0, and 0 <= p_t <= 1. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem23.1 
|- F/ t ph
stoweidlem23.2 
|- F/_ t G
stoweidlem23.3 
|- H = ( t e. T |-> ( ( G ` t ) - ( G ` Z ) ) )
stoweidlem23.4 
|- ( ( ph /\ f e. A ) -> f : T --> RR )
stoweidlem23.5 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
stoweidlem23.6 
|- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
stoweidlem23.7 
|- ( ph -> S e. T )
stoweidlem23.8 
|- ( ph -> Z e. T )
stoweidlem23.9 
|- ( ph -> G e. A )
stoweidlem23.10 
|- ( ph -> ( G ` S ) =/= ( G ` Z ) )
Assertion stoweidlem23 
|- ( ph -> ( H e. A /\ ( H ` S ) =/= ( H ` Z ) /\ ( H ` Z ) = 0 ) )

Proof

Step Hyp Ref Expression
1 stoweidlem23.1 
 |-  F/ t ph
2 stoweidlem23.2 
 |-  F/_ t G
3 stoweidlem23.3 
 |-  H = ( t e. T |-> ( ( G ` t ) - ( G ` Z ) ) )
4 stoweidlem23.4 
 |-  ( ( ph /\ f e. A ) -> f : T --> RR )
5 stoweidlem23.5 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
6 stoweidlem23.6 
 |-  ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
7 stoweidlem23.7 
 |-  ( ph -> S e. T )
8 stoweidlem23.8 
 |-  ( ph -> Z e. T )
9 stoweidlem23.9 
 |-  ( ph -> G e. A )
10 stoweidlem23.10 
 |-  ( ph -> ( G ` S ) =/= ( G ` Z ) )
11 9 ancli 
 |-  ( ph -> ( ph /\ G e. A ) )
12 eleq1 
 |-  ( f = G -> ( f e. A <-> G e. A ) )
13 12 anbi2d 
 |-  ( f = G -> ( ( ph /\ f e. A ) <-> ( ph /\ G e. A ) ) )
14 feq1 
 |-  ( f = G -> ( f : T --> RR <-> G : T --> RR ) )
15 13 14 imbi12d 
 |-  ( f = G -> ( ( ( ph /\ f e. A ) -> f : T --> RR ) <-> ( ( ph /\ G e. A ) -> G : T --> RR ) ) )
16 15 4 vtoclg 
 |-  ( G e. A -> ( ( ph /\ G e. A ) -> G : T --> RR ) )
17 9 11 16 sylc 
 |-  ( ph -> G : T --> RR )
18 17 ffvelrnda 
 |-  ( ( ph /\ t e. T ) -> ( G ` t ) e. RR )
19 18 recnd 
 |-  ( ( ph /\ t e. T ) -> ( G ` t ) e. CC )
20 17 8 ffvelrnd 
 |-  ( ph -> ( G ` Z ) e. RR )
21 20 adantr 
 |-  ( ( ph /\ t e. T ) -> ( G ` Z ) e. RR )
22 21 recnd 
 |-  ( ( ph /\ t e. T ) -> ( G ` Z ) e. CC )
23 19 22 negsubd 
 |-  ( ( ph /\ t e. T ) -> ( ( G ` t ) + -u ( G ` Z ) ) = ( ( G ` t ) - ( G ` Z ) ) )
24 1 23 mpteq2da 
 |-  ( ph -> ( t e. T |-> ( ( G ` t ) + -u ( G ` Z ) ) ) = ( t e. T |-> ( ( G ` t ) - ( G ` Z ) ) ) )
25 simpr 
 |-  ( ( ph /\ t e. T ) -> t e. T )
26 20 renegcld 
 |-  ( ph -> -u ( G ` Z ) e. RR )
27 26 adantr 
 |-  ( ( ph /\ t e. T ) -> -u ( G ` Z ) e. RR )
28 eqid 
 |-  ( t e. T |-> -u ( G ` Z ) ) = ( t e. T |-> -u ( G ` Z ) )
29 28 fvmpt2 
 |-  ( ( t e. T /\ -u ( G ` Z ) e. RR ) -> ( ( t e. T |-> -u ( G ` Z ) ) ` t ) = -u ( G ` Z ) )
30 25 27 29 syl2anc 
 |-  ( ( ph /\ t e. T ) -> ( ( t e. T |-> -u ( G ` Z ) ) ` t ) = -u ( G ` Z ) )
31 30 oveq2d 
 |-  ( ( ph /\ t e. T ) -> ( ( G ` t ) + ( ( t e. T |-> -u ( G ` Z ) ) ` t ) ) = ( ( G ` t ) + -u ( G ` Z ) ) )
32 1 31 mpteq2da 
 |-  ( ph -> ( t e. T |-> ( ( G ` t ) + ( ( t e. T |-> -u ( G ` Z ) ) ` t ) ) ) = ( t e. T |-> ( ( G ` t ) + -u ( G ` Z ) ) ) )
33 26 ancli 
 |-  ( ph -> ( ph /\ -u ( G ` Z ) e. RR ) )
34 eleq1 
 |-  ( x = -u ( G ` Z ) -> ( x e. RR <-> -u ( G ` Z ) e. RR ) )
35 34 anbi2d 
 |-  ( x = -u ( G ` Z ) -> ( ( ph /\ x e. RR ) <-> ( ph /\ -u ( G ` Z ) e. RR ) ) )
36 nfcv 
 |-  F/_ t Z
37 2 36 nffv 
 |-  F/_ t ( G ` Z )
38 37 nfneg 
 |-  F/_ t -u ( G ` Z )
39 38 nfeq2 
 |-  F/ t x = -u ( G ` Z )
40 simpl 
 |-  ( ( x = -u ( G ` Z ) /\ t e. T ) -> x = -u ( G ` Z ) )
41 39 40 mpteq2da 
 |-  ( x = -u ( G ` Z ) -> ( t e. T |-> x ) = ( t e. T |-> -u ( G ` Z ) ) )
42 41 eleq1d 
 |-  ( x = -u ( G ` Z ) -> ( ( t e. T |-> x ) e. A <-> ( t e. T |-> -u ( G ` Z ) ) e. A ) )
43 35 42 imbi12d 
 |-  ( x = -u ( G ` Z ) -> ( ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A ) <-> ( ( ph /\ -u ( G ` Z ) e. RR ) -> ( t e. T |-> -u ( G ` Z ) ) e. A ) ) )
44 43 6 vtoclg 
 |-  ( -u ( G ` Z ) e. RR -> ( ( ph /\ -u ( G ` Z ) e. RR ) -> ( t e. T |-> -u ( G ` Z ) ) e. A ) )
45 26 33 44 sylc 
 |-  ( ph -> ( t e. T |-> -u ( G ` Z ) ) e. A )
46 nfmpt1 
 |-  F/_ t ( t e. T |-> -u ( G ` Z ) )
47 5 2 46 stoweidlem8 
 |-  ( ( ph /\ G e. A /\ ( t e. T |-> -u ( G ` Z ) ) e. A ) -> ( t e. T |-> ( ( G ` t ) + ( ( t e. T |-> -u ( G ` Z ) ) ` t ) ) ) e. A )
48 9 45 47 mpd3an23 
 |-  ( ph -> ( t e. T |-> ( ( G ` t ) + ( ( t e. T |-> -u ( G ` Z ) ) ` t ) ) ) e. A )
49 32 48 eqeltrrd 
 |-  ( ph -> ( t e. T |-> ( ( G ` t ) + -u ( G ` Z ) ) ) e. A )
50 24 49 eqeltrrd 
 |-  ( ph -> ( t e. T |-> ( ( G ` t ) - ( G ` Z ) ) ) e. A )
51 3 50 eqeltrid 
 |-  ( ph -> H e. A )
52 17 7 ffvelrnd 
 |-  ( ph -> ( G ` S ) e. RR )
53 52 recnd 
 |-  ( ph -> ( G ` S ) e. CC )
54 20 recnd 
 |-  ( ph -> ( G ` Z ) e. CC )
55 53 54 10 subne0d 
 |-  ( ph -> ( ( G ` S ) - ( G ` Z ) ) =/= 0 )
56 52 20 resubcld 
 |-  ( ph -> ( ( G ` S ) - ( G ` Z ) ) e. RR )
57 nfcv 
 |-  F/_ t S
58 2 57 nffv 
 |-  F/_ t ( G ` S )
59 nfcv 
 |-  F/_ t -
60 58 59 37 nfov 
 |-  F/_ t ( ( G ` S ) - ( G ` Z ) )
61 fveq2 
 |-  ( t = S -> ( G ` t ) = ( G ` S ) )
62 61 oveq1d 
 |-  ( t = S -> ( ( G ` t ) - ( G ` Z ) ) = ( ( G ` S ) - ( G ` Z ) ) )
63 57 60 62 3 fvmptf 
 |-  ( ( S e. T /\ ( ( G ` S ) - ( G ` Z ) ) e. RR ) -> ( H ` S ) = ( ( G ` S ) - ( G ` Z ) ) )
64 7 56 63 syl2anc 
 |-  ( ph -> ( H ` S ) = ( ( G ` S ) - ( G ` Z ) ) )
65 20 20 resubcld 
 |-  ( ph -> ( ( G ` Z ) - ( G ` Z ) ) e. RR )
66 37 59 37 nfov 
 |-  F/_ t ( ( G ` Z ) - ( G ` Z ) )
67 fveq2 
 |-  ( t = Z -> ( G ` t ) = ( G ` Z ) )
68 67 oveq1d 
 |-  ( t = Z -> ( ( G ` t ) - ( G ` Z ) ) = ( ( G ` Z ) - ( G ` Z ) ) )
69 36 66 68 3 fvmptf 
 |-  ( ( Z e. T /\ ( ( G ` Z ) - ( G ` Z ) ) e. RR ) -> ( H ` Z ) = ( ( G ` Z ) - ( G ` Z ) ) )
70 8 65 69 syl2anc 
 |-  ( ph -> ( H ` Z ) = ( ( G ` Z ) - ( G ` Z ) ) )
71 54 subidd 
 |-  ( ph -> ( ( G ` Z ) - ( G ` Z ) ) = 0 )
72 70 71 eqtrd 
 |-  ( ph -> ( H ` Z ) = 0 )
73 55 64 72 3netr4d 
 |-  ( ph -> ( H ` S ) =/= ( H ` Z ) )
74 51 73 72 3jca 
 |-  ( ph -> ( H e. A /\ ( H ` S ) =/= ( H ` Z ) /\ ( H ` Z ) = 0 ) )