Theorem ioorrnopn

Description: The indexed product of open intervals is an open set in ( RR^X ) . (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	ioorrnopn.x	$$⊢\phi \to X\in \mathrm{Fin}$$
	ioorrnopn.a	$$⊢\phi \to A:X⟶ℝ$$
	ioorrnopn.b	$$⊢\phi \to B:X⟶ℝ$$
Assertion	ioorrnopn

Proof

Step	Hyp	Ref	Expression
1		ioorrnopn.x	$$⊢\phi \to X\in \mathrm{Fin}$$
2		ioorrnopn.a	$$⊢\phi \to A:X⟶ℝ$$
3		ioorrnopn.b	$$⊢\phi \to B:X⟶ℝ$$
4		p0ex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
5	4	prid2	$$⊢\left\{\varnothing \right\}\in \left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
6	5	a1i	$$⊢X=\varnothing \to \left\{\varnothing \right\}\in \left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
7		ixpeq1	$$⊢X=\varnothing \to \underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)=\underset{i\in \varnothing }{⨉}\left(A\left(i\right),B\left(i\right)\right)$$
8		ixp0x	$$⊢\underset{i\in \varnothing }{⨉}\left(A\left(i\right),B\left(i\right)\right)=\left\{\varnothing \right\}$$
9	8	a1i	$$⊢X=\varnothing \to \underset{i\in \varnothing }{⨉}\left(A\left(i\right),B\left(i\right)\right)=\left\{\varnothing \right\}$$
10	7 9	eqtrd	$$⊢X=\varnothing \to \underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)=\left\{\varnothing \right\}$$
11		2fveq3
12		rrxtopn0b
13	12	a1i
14	11 13	eqtrd
15	10 14	eleq12d
16	6 15	mpbird
17	16	adantl
18		neqne	$$⊢\neg X=\varnothing \to X\ne \varnothing$$
19	18	adantl	$$⊢\left(\phi \wedge \neg X=\varnothing \right)\to X\ne \varnothing$$
20		fveq2	$$⊢i=j\to A\left(i\right)=A\left(j\right)$$
21		fveq2	$$⊢i=j\to B\left(i\right)=B\left(j\right)$$
22	20 21	oveq12d	$$⊢i=j\to \left(A\left(i\right),B\left(i\right)\right)=\left(A\left(j\right),B\left(j\right)\right)$$
23	22	cbvixpv	$$⊢\underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)=\underset{j\in X}{⨉}\left(A\left(j\right),B\left(j\right)\right)$$
24	23	eleq2i	$$⊢f\in \underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)\leftrightarrow f\in \underset{j\in X}{⨉}\left(A\left(j\right),B\left(j\right)\right)$$
25	24	bilani	$$⊢\left(\left(\phi \wedge X\ne \varnothing \right)\wedge f\in \underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)\right)\to f\in \underset{j\in X}{⨉}\left(A\left(j\right),B\left(j\right)\right)$$
26	1	ad2antrr	$$⊢\left(\left(\phi \wedge X\ne \varnothing \right)\wedge f\in \underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)\right)\to X\in \mathrm{Fin}$$
27	24 26	sylan2br	$$⊢\left(\left(\phi \wedge X\ne \varnothing \right)\wedge f\in \underset{j\in X}{⨉}\left(A\left(j\right),B\left(j\right)\right)\right)\to X\in \mathrm{Fin}$$
28		simplr	$$⊢\left(\left(\phi \wedge X\ne \varnothing \right)\wedge f\in \underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)\right)\to X\ne \varnothing$$
29	24 28	sylan2br	$$⊢\left(\left(\phi \wedge X\ne \varnothing \right)\wedge f\in \underset{j\in X}{⨉}\left(A\left(j\right),B\left(j\right)\right)\right)\to X\ne \varnothing$$
30	2	ad2antrr	$$⊢\left(\left(\phi \wedge X\ne \varnothing \right)\wedge f\in \underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)\right)\to A:X⟶ℝ$$
31	24 30	sylan2br	$$⊢\left(\left(\phi \wedge X\ne \varnothing \right)\wedge f\in \underset{j\in X}{⨉}\left(A\left(j\right),B\left(j\right)\right)\right)\to A:X⟶ℝ$$
32	3	ad2antrr	$$⊢\left(\left(\phi \wedge X\ne \varnothing \right)\wedge f\in \underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)\right)\to B:X⟶ℝ$$
33	24 32	sylan2br	$$⊢\left(\left(\phi \wedge X\ne \varnothing \right)\wedge f\in \underset{j\in X}{⨉}\left(A\left(j\right),B\left(j\right)\right)\right)\to B:X⟶ℝ$$
34	24	bilanri	$$⊢\left(\left(\phi \wedge X\ne \varnothing \right)\wedge f\in \underset{j\in X}{⨉}\left(A\left(j\right),B\left(j\right)\right)\right)\to f\in \underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)$$
35		eqid	$$⊢\mathrm{ran}\left(i\in X⟼if\left(B\left(i\right)-f\left(i\right)\le f\left(i\right)-A\left(i\right),B\left(i\right)-f\left(i\right),f\left(i\right)-A\left(i\right)\right)\right)=\mathrm{ran}\left(i\in X⟼if\left(B\left(i\right)-f\left(i\right)\le f\left(i\right)-A\left(i\right),B\left(i\right)-f\left(i\right),f\left(i\right)-A\left(i\right)\right)\right)$$
36		fveq2	$$⊢j=i\to B\left(j\right)=B\left(i\right)$$
37		fveq2	$$⊢j=i\to f\left(j\right)=f\left(i\right)$$
38	36 37	oveq12d	$$⊢j=i\to B\left(j\right)-f\left(j\right)=B\left(i\right)-f\left(i\right)$$
39		fveq2	$$⊢j=i\to A\left(j\right)=A\left(i\right)$$
40	37 39	oveq12d	$$⊢j=i\to f\left(j\right)-A\left(j\right)=f\left(i\right)-A\left(i\right)$$
41	38 40	breq12d	$$⊢j=i\to \left(B\left(j\right)-f\left(j\right)\le f\left(j\right)-A\left(j\right)\leftrightarrow B\left(i\right)-f\left(i\right)\le f\left(i\right)-A\left(i\right)\right)$$
42	41 38 40	ifbieq12d	$$⊢j=i\to if\left(B\left(j\right)-f\left(j\right)\le f\left(j\right)-A\left(j\right),B\left(j\right)-f\left(j\right),f\left(j\right)-A\left(j\right)\right)=if\left(B\left(i\right)-f\left(i\right)\le f\left(i\right)-A\left(i\right),B\left(i\right)-f\left(i\right),f\left(i\right)-A\left(i\right)\right)$$
43	42	cbvmptv	$$⊢\left(j\in X⟼if\left(B\left(j\right)-f\left(j\right)\le f\left(j\right)-A\left(j\right),B\left(j\right)-f\left(j\right),f\left(j\right)-A\left(j\right)\right)\right)=\left(i\in X⟼if\left(B\left(i\right)-f\left(i\right)\le f\left(i\right)-A\left(i\right),B\left(i\right)-f\left(i\right),f\left(i\right)-A\left(i\right)\right)\right)$$
44	43	rneqi	$$⊢\mathrm{ran}\left(j\in X⟼if\left(B\left(j\right)-f\left(j\right)\le f\left(j\right)-A\left(j\right),B\left(j\right)-f\left(j\right),f\left(j\right)-A\left(j\right)\right)\right)=\mathrm{ran}\left(i\in X⟼if\left(B\left(i\right)-f\left(i\right)\le f\left(i\right)-A\left(i\right),B\left(i\right)-f\left(i\right),f\left(i\right)-A\left(i\right)\right)\right)$$
45	44	infeq1i	$$⊢inf\left(\mathrm{ran}\left(j\in X⟼if\left(B\left(j\right)-f\left(j\right)\le f\left(j\right)-A\left(j\right),B\left(j\right)-f\left(j\right),f\left(j\right)-A\left(j\right)\right)\right),ℝ,<\right)=inf\left(\mathrm{ran}\left(i\in X⟼if\left(B\left(i\right)-f\left(i\right)\le f\left(i\right)-A\left(i\right),B\left(i\right)-f\left(i\right),f\left(i\right)-A\left(i\right)\right)\right),ℝ,<\right)$$
46		eqid	$$⊢f\mathrm{ball}\left(\left(a\in \left({ℝ}^X\right),b\in \left({ℝ}^X\right)⟼\sqrt{\sum _{k\in X}{\left(a\left(k\right)-b\left(k\right)\right)}^2}\right)\right)inf\left(\mathrm{ran}\left(j\in X⟼if\left(B\left(j\right)-f\left(j\right)\le f\left(j\right)-A\left(j\right),B\left(j\right)-f\left(j\right),f\left(j\right)-A\left(j\right)\right)\right),ℝ,<\right)=f\mathrm{ball}\left(\left(a\in \left({ℝ}^X\right),b\in \left({ℝ}^X\right)⟼\sqrt{\sum _{k\in X}{\left(a\left(k\right)-b\left(k\right)\right)}^2}\right)\right)inf\left(\mathrm{ran}\left(j\in X⟼if\left(B\left(j\right)-f\left(j\right)\le f\left(j\right)-A\left(j\right),B\left(j\right)-f\left(j\right),f\left(j\right)-A\left(j\right)\right)\right),ℝ,<\right)$$
47		fveq1	$$⊢a=g\to a\left(k\right)=g\left(k\right)$$
48	47	oveq1d	$$⊢a=g\to a\left(k\right)-b\left(k\right)=g\left(k\right)-b\left(k\right)$$
49	48	oveq1d	$$⊢a=g\to {\left(a\left(k\right)-b\left(k\right)\right)}^2={\left(g\left(k\right)-b\left(k\right)\right)}^2$$
50	49	sumeq2sdv	$$⊢a=g\to \sum _{k\in X}{\left(a\left(k\right)-b\left(k\right)\right)}^2=\sum _{k\in X}{\left(g\left(k\right)-b\left(k\right)\right)}^2$$
51	50	fveq2d	$$⊢a=g\to \sqrt{\sum _{k\in X}{\left(a\left(k\right)-b\left(k\right)\right)}^2}=\sqrt{\sum _{k\in X}{\left(g\left(k\right)-b\left(k\right)\right)}^2}$$
52		fveq1	$$⊢b=h\to b\left(k\right)=h\left(k\right)$$
53	52	oveq2d	$$⊢b=h\to g\left(k\right)-b\left(k\right)=g\left(k\right)-h\left(k\right)$$
54	53	oveq1d	$$⊢b=h\to {\left(g\left(k\right)-b\left(k\right)\right)}^2={\left(g\left(k\right)-h\left(k\right)\right)}^2$$
55	54	sumeq2sdv	$$⊢b=h\to \sum _{k\in X}{\left(g\left(k\right)-b\left(k\right)\right)}^2=\sum _{k\in X}{\left(g\left(k\right)-h\left(k\right)\right)}^2$$
56	55	fveq2d	$$⊢b=h\to \sqrt{\sum _{k\in X}{\left(g\left(k\right)-b\left(k\right)\right)}^2}=\sqrt{\sum _{k\in X}{\left(g\left(k\right)-h\left(k\right)\right)}^2}$$
57	51 56	cbvmpov	$$⊢\left(a\in \left({ℝ}^X\right),b\in \left({ℝ}^X\right)⟼\sqrt{\sum _{k\in X}{\left(a\left(k\right)-b\left(k\right)\right)}^2}\right)=\left(g\in \left({ℝ}^X\right),h\in \left({ℝ}^X\right)⟼\sqrt{\sum _{k\in X}{\left(g\left(k\right)-h\left(k\right)\right)}^2}\right)$$
58	27 29 31 33 34 35 45 46 57	ioorrnopnlem
59	25 58	syldan
60	59	ralrimiva
61		eqid
62	61	rrxtop
63	1 62	syl
64	63	adantr
65		eltop2
66	64 65	syl
67	60 66	mpbird
68	19 67	syldan
69	17 68	pm2.61dan