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	biimpi	$$⊢f\in \underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)\to f\in \underset{j\in X}{⨉}\left(A\left(j\right),B\left(j\right)\right)$$
26	25	adantl	$$⊢\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)$$
27	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}$$
28	24 27	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}$$
29		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$$
30	24 29	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$$
31	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⟶ℝ$$
32	24 31	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⟶ℝ$$
33	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⟶ℝ$$
34	24 33	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⟶ℝ$$
35		simpr	$$⊢\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{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)$$
36	24 35	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 f\in \underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)$$
37		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)$$
38		fveq2	$$⊢j=i\to B\left(j\right)=B\left(i\right)$$
39		fveq2	$$⊢j=i\to f\left(j\right)=f\left(i\right)$$
40	38 39	oveq12d	$$⊢j=i\to B\left(j\right)-f\left(j\right)=B\left(i\right)-f\left(i\right)$$
41		fveq2	$$⊢j=i\to A\left(j\right)=A\left(i\right)$$
42	39 41	oveq12d	$$⊢j=i\to f\left(j\right)-A\left(j\right)=f\left(i\right)-A\left(i\right)$$
43	40 42	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)$$
44	43 40 42	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)$$
45	44	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)$$
46	45	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)$$
47	46	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)$$
48		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)$$
49		fveq1	$$⊢a=g\to a\left(k\right)=g\left(k\right)$$
50	49	oveq1d	$$⊢a=g\to a\left(k\right)-b\left(k\right)=g\left(k\right)-b\left(k\right)$$
51	50	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$$
52	51	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$$
53	52	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}$$
54		fveq1	$$⊢b=h\to b\left(k\right)=h\left(k\right)$$
55	54	oveq2d	$$⊢b=h\to g\left(k\right)-b\left(k\right)=g\left(k\right)-h\left(k\right)$$
56	55	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$$
57	56	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$$
58	57	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}$$
59	53 58	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)$$
60	28 30 32 34 36 37 47 48 59	ioorrnopnlem
61	26 60	syldan
62	61	ralrimiva
63		eqid
64	63	rrxtop
65	1 64	syl
66	65	adantr
67		eltop2
68	66 67	syl
69	62 68	mpbird
70	19 69	syldan
71	17 70	pm2.61dan