Theorem ipasslem8

Description: Lemma for ipassi . By ipasslem5 , F is 0 for all QQ ; since it is continuous and QQ is dense in RR by qdensere2 , we conclude F is 0 for all RR . (Contributed by NM, 24-Aug-2007) (Revised by Mario Carneiro, 6-May-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ip1i.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	ip1i.2	$$⊢G={+}_v\left(U\right)$$
	ip1i.4	$$⊢S={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
	ip1i.7	$$⊢P={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
	ip1i.9	$$⊢U\in {CPreHil}_{\mathrm{OLD}}$$
	ipasslem7.a	$$⊢A\in X$$
	ipasslem7.b	$$⊢B\in X$$
	ipasslem7.f	$$⊢F=\left(w\in ℝ⟼\left(\left(wSA\right)PB\right)-w\left(APB\right)\right)$$
Assertion	ipasslem8	$$⊢F:ℝ⟶\left\{0\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ip1i.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		ip1i.2	$$⊢G={+}_v\left(U\right)$$
3		ip1i.4	$$⊢S={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
4		ip1i.7	$$⊢P={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
5		ip1i.9	$$⊢U\in {CPreHil}_{\mathrm{OLD}}$$
6		ipasslem7.a	$$⊢A\in X$$
7		ipasslem7.b	$$⊢B\in X$$
8		ipasslem7.f	$$⊢F=\left(w\in ℝ⟼\left(\left(wSA\right)PB\right)-w\left(APB\right)\right)$$
9		0cn	$$⊢0\in ℂ$$
10		qre	$$⊢x\in \mathbb{Q}\to x\in ℝ$$
11		oveq1	$$⊢w=x\to wSA=xSA$$
12	11	oveq1d	$$⊢w=x\to \left(wSA\right)PB=\left(xSA\right)PB$$
13		oveq1	$$⊢w=x\to w\left(APB\right)=x\left(APB\right)$$
14	12 13	oveq12d	$$⊢w=x\to \left(\left(wSA\right)PB\right)-w\left(APB\right)=\left(\left(xSA\right)PB\right)-x\left(APB\right)$$
15		ovex	$$⊢\left(\left(xSA\right)PB\right)-x\left(APB\right)\in \mathrm{V}$$
16	14 8 15	fvmpt	$$⊢x\in ℝ\to F\left(x\right)=\left(\left(xSA\right)PB\right)-x\left(APB\right)$$
17	10 16	syl	$$⊢x\in \mathbb{Q}\to F\left(x\right)=\left(\left(xSA\right)PB\right)-x\left(APB\right)$$
18		qcn	$$⊢x\in \mathbb{Q}\to x\in ℂ$$
19	5	phnvi	$$⊢U\in \mathrm{NrmCVec}$$
20	1 3	nvscl	$$⊢\left(U\in \mathrm{NrmCVec}\wedge x\in ℂ\wedge A\in X\right)\to xSA\in X$$
21	19 20	mp3an1	$$⊢\left(x\in ℂ\wedge A\in X\right)\to xSA\in X$$
22	18 21	sylan	$$⊢\left(x\in \mathbb{Q}\wedge A\in X\right)\to xSA\in X$$
23	1 4	dipcl	$$⊢\left(U\in \mathrm{NrmCVec}\wedge xSA\in X\wedge B\in X\right)\to \left(xSA\right)PB\in ℂ$$
24	19 7 23	mp3an13	$$⊢xSA\in X\to \left(xSA\right)PB\in ℂ$$
25	22 24	syl	$$⊢\left(x\in \mathbb{Q}\wedge A\in X\right)\to \left(xSA\right)PB\in ℂ$$
26	1 2 3 4 5 7	ipasslem5	$$⊢\left(x\in \mathbb{Q}\wedge A\in X\right)\to \left(xSA\right)PB=x\left(APB\right)$$
27	25 26	subeq0bd	$$⊢\left(x\in \mathbb{Q}\wedge A\in X\right)\to \left(\left(xSA\right)PB\right)-x\left(APB\right)=0$$
28	6 27	mpan2	$$⊢x\in \mathbb{Q}\to \left(\left(xSA\right)PB\right)-x\left(APB\right)=0$$
29	17 28	eqtrd	$$⊢x\in \mathbb{Q}\to F\left(x\right)=0$$
30	29	rgen	$$⊢\forall x\in \mathbb{Q}F\left(x\right)=0$$
31	8	funmpt2	$$⊢\mathrm{Fun}F$$
32		qssre	$$⊢\mathbb{Q}\subseteq ℝ$$
33		ovex	$$⊢\left(\left(wSA\right)PB\right)-w\left(APB\right)\in \mathrm{V}$$
34	33 8	dmmpti	$$⊢\mathrm{dom}F=ℝ$$
35	32 34	sseqtrri	$$⊢\mathbb{Q}\subseteq \mathrm{dom}F$$
36		funconstss	$$⊢\left(\mathrm{Fun}F\wedge \mathbb{Q}\subseteq \mathrm{dom}F\right)\to \left(\forall x\in \mathbb{Q}F\left(x\right)=0\leftrightarrow \mathbb{Q}\subseteq F^{-1}\left[\left\{0\right\}\right]\right)$$
37	31 35 36	mp2an	$$⊢\forall x\in \mathbb{Q}F\left(x\right)=0\leftrightarrow \mathbb{Q}\subseteq F^{-1}\left[\left\{0\right\}\right]$$
38	30 37	mpbi	$$⊢\mathbb{Q}\subseteq F^{-1}\left[\left\{0\right\}\right]$$
39		qdensere	$$⊢\mathrm{cls}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\mathbb{Q}\right)=ℝ$$
40		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
41	40	cnfldhaus	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Haus}$$
42		haust1	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Haus}\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Fre}$$
43	41 42	ax-mp	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Fre}$$
44		eqid	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
45	1 2 3 4 5 6 7 8 44 40	ipasslem7	$$⊢F\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
46		uniretop	$$⊢ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
47	40	cnfldtopon	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
48	47	toponunii	$$⊢ℂ=\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
49	46 48	dnsconst	$$⊢\left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Fre}\wedge F\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\right)\wedge \left(0\in ℂ\wedge \mathbb{Q}\subseteq F^{-1}\left[\left\{0\right\}\right]\wedge \mathrm{cls}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\mathbb{Q}\right)=ℝ\right)\right)\to F:ℝ⟶\left\{0\right\}$$
50	43 45 49	mpanl12	$$⊢\left(0\in ℂ\wedge \mathbb{Q}\subseteq F^{-1}\left[\left\{0\right\}\right]\wedge \mathrm{cls}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\mathbb{Q}\right)=ℝ\right)\to F:ℝ⟶\left\{0\right\}$$
51	9 38 39 50	mp3an	$$⊢F:ℝ⟶\left\{0\right\}$$