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 tφ
stoweidlem23.2 _tG
stoweidlem23.3 H=tTGtGZ
stoweidlem23.4 φfAf:T
stoweidlem23.5 φfAgAtTft+gtA
stoweidlem23.6 φxtTxA
stoweidlem23.7 φST
stoweidlem23.8 φZT
stoweidlem23.9 φGA
stoweidlem23.10 φGSGZ
Assertion stoweidlem23 φHAHSHZHZ=0

Proof

Step Hyp Ref Expression
1 stoweidlem23.1 tφ
2 stoweidlem23.2 _tG
3 stoweidlem23.3 H=tTGtGZ
4 stoweidlem23.4 φfAf:T
5 stoweidlem23.5 φfAgAtTft+gtA
6 stoweidlem23.6 φxtTxA
7 stoweidlem23.7 φST
8 stoweidlem23.8 φZT
9 stoweidlem23.9 φGA
10 stoweidlem23.10 φGSGZ
11 9 ancli φφGA
12 eleq1 f=GfAGA
13 12 anbi2d f=GφfAφGA
14 feq1 f=Gf:TG:T
15 13 14 imbi12d f=GφfAf:TφGAG:T
16 15 4 vtoclg GAφGAG:T
17 9 11 16 sylc φG:T
18 17 ffvelrnda φtTGt
19 18 recnd φtTGt
20 17 8 ffvelrnd φGZ
21 20 adantr φtTGZ
22 21 recnd φtTGZ
23 19 22 negsubd φtTGt+GZ=GtGZ
24 1 23 mpteq2da φtTGt+GZ=tTGtGZ
25 simpr φtTtT
26 20 renegcld φGZ
27 26 adantr φtTGZ
28 eqid tTGZ=tTGZ
29 28 fvmpt2 tTGZtTGZt=GZ
30 25 27 29 syl2anc φtTtTGZt=GZ
31 30 oveq2d φtTGt+tTGZt=Gt+GZ
32 1 31 mpteq2da φtTGt+tTGZt=tTGt+GZ
33 26 ancli φφGZ
34 eleq1 x=GZxGZ
35 34 anbi2d x=GZφxφGZ
36 nfcv _tZ
37 2 36 nffv _tGZ
38 37 nfneg _tGZ
39 38 nfeq2 tx=GZ
40 simpl x=GZtTx=GZ
41 39 40 mpteq2da x=GZtTx=tTGZ
42 41 eleq1d x=GZtTxAtTGZA
43 35 42 imbi12d x=GZφxtTxAφGZtTGZA
44 43 6 vtoclg GZφGZtTGZA
45 26 33 44 sylc φtTGZA
46 nfmpt1 _ttTGZ
47 5 2 46 stoweidlem8 φGAtTGZAtTGt+tTGZtA
48 9 45 47 mpd3an23 φtTGt+tTGZtA
49 32 48 eqeltrrd φtTGt+GZA
50 24 49 eqeltrrd φtTGtGZA
51 3 50 eqeltrid φHA
52 17 7 ffvelrnd φGS
53 52 recnd φGS
54 20 recnd φGZ
55 53 54 10 subne0d φGSGZ0
56 52 20 resubcld φGSGZ
57 nfcv _tS
58 2 57 nffv _tGS
59 nfcv _t
60 58 59 37 nfov _tGSGZ
61 fveq2 t=SGt=GS
62 61 oveq1d t=SGtGZ=GSGZ
63 57 60 62 3 fvmptf STGSGZHS=GSGZ
64 7 56 63 syl2anc φHS=GSGZ
65 20 20 resubcld φGZGZ
66 37 59 37 nfov _tGZGZ
67 fveq2 t=ZGt=GZ
68 67 oveq1d t=ZGtGZ=GZGZ
69 36 66 68 3 fvmptf ZTGZGZHZ=GZGZ
70 8 65 69 syl2anc φHZ=GZGZ
71 54 subidd φGZGZ=0
72 70 71 eqtrd φHZ=0
73 55 64 72 3netr4d φHSHZ
74 51 73 72 3jca φHAHSHZHZ=0