# 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}\phantom{\rule{.4em}{0ex}}{\phi }$
stoweidlem23.2 ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}{G}$
stoweidlem23.3 ${⊢}{H}=\left({t}\in {T}⟼{G}\left({t}\right)-{G}\left({Z}\right)\right)$
stoweidlem23.4 ${⊢}\left({\phi }\wedge {f}\in {A}\right)\to {f}:{T}⟶ℝ$
stoweidlem23.5 ${⊢}\left({\phi }\wedge {f}\in {A}\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right)+{g}\left({t}\right)\right)\in {A}$
stoweidlem23.6 ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({t}\in {T}⟼{x}\right)\in {A}$
stoweidlem23.7 ${⊢}{\phi }\to {S}\in {T}$
stoweidlem23.8 ${⊢}{\phi }\to {Z}\in {T}$
stoweidlem23.9 ${⊢}{\phi }\to {G}\in {A}$
stoweidlem23.10 ${⊢}{\phi }\to {G}\left({S}\right)\ne {G}\left({Z}\right)$
Assertion stoweidlem23 ${⊢}{\phi }\to \left({H}\in {A}\wedge {H}\left({S}\right)\ne {H}\left({Z}\right)\wedge {H}\left({Z}\right)=0\right)$

### Proof

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