Theorem 2sphere0

Description: The sphere around the origin .0. (see rrx0 ) with radius R in a two dimensional Euclidean space is a circle. (Contributed by AV, 5-Feb-2023)

	Ref	Expression
Hypotheses	2sphere.i	$$⊢I=\left\{1,2\right\}$$
	2sphere.e
	2sphere.p	$$⊢P={ℝ}^I$$
	2sphere.s	$$⊢S=Sphere\left(E\right)$$
	2sphere0.0	$$⊢\underset{\dot{}}{0}=I\times \left\{0\right\}$$
	2sphere0.c	$$⊢C=\left\{p\in P|{p\left(1\right)}^2+{p\left(2\right)}^2=R^2\right\}$$
Assertion	2sphere0	$$⊢R\in \left[0,\mathrm{+\infty }\right)\to \underset{\dot{}}{0}SR=C$$

Proof

Step	Hyp	Ref	Expression
1		2sphere.i	$$⊢I=\left\{1,2\right\}$$
2		2sphere.e
3		2sphere.p	$$⊢P={ℝ}^I$$
4		2sphere.s	$$⊢S=Sphere\left(E\right)$$
5		2sphere0.0	$$⊢\underset{\dot{}}{0}=I\times \left\{0\right\}$$
6		2sphere0.c	$$⊢C=\left\{p\in P|{p\left(1\right)}^2+{p\left(2\right)}^2=R^2\right\}$$
7		prex	$$⊢\left\{1,2\right\}\in \mathrm{V}$$
8	1 7	eqeltri	$$⊢I\in \mathrm{V}$$
9	5 3	rrx0el	$$⊢I\in \mathrm{V}\to \underset{\dot{}}{0}\in P$$
10	8 9	ax-mp	$$⊢\underset{\dot{}}{0}\in P$$
11		eqid	$$⊢\left\{p\in P|{\left(p\left(1\right)-\underset{\dot{}}{0}\left(1\right)\right)}^2+{\left(p\left(2\right)-\underset{\dot{}}{0}\left(2\right)\right)}^2=R^2\right\}=\left\{p\in P|{\left(p\left(1\right)-\underset{\dot{}}{0}\left(1\right)\right)}^2+{\left(p\left(2\right)-\underset{\dot{}}{0}\left(2\right)\right)}^2=R^2\right\}$$
12	1 2 3 4 11	2sphere	$$⊢\left(\underset{\dot{}}{0}\in P\wedge R\in \left[0,\mathrm{+\infty }\right)\right)\to \underset{\dot{}}{0}SR=\left\{p\in P|{\left(p\left(1\right)-\underset{\dot{}}{0}\left(1\right)\right)}^2+{\left(p\left(2\right)-\underset{\dot{}}{0}\left(2\right)\right)}^2=R^2\right\}$$
13	10 12	mpan	$$⊢R\in \left[0,\mathrm{+\infty }\right)\to \underset{\dot{}}{0}SR=\left\{p\in P|{\left(p\left(1\right)-\underset{\dot{}}{0}\left(1\right)\right)}^2+{\left(p\left(2\right)-\underset{\dot{}}{0}\left(2\right)\right)}^2=R^2\right\}$$
14	5	fveq1i	$$⊢\underset{\dot{}}{0}\left(1\right)=\left(I\times \left\{0\right\}\right)\left(1\right)$$
15		c0ex	$$⊢0\in \mathrm{V}$$
16		1ex	$$⊢1\in \mathrm{V}$$
17	16	prid1	$$⊢1\in \left\{1,2\right\}$$
18	17 1	eleqtrri	$$⊢1\in I$$
19		fvconst2g	$$⊢\left(0\in \mathrm{V}\wedge 1\in I\right)\to \left(I\times \left\{0\right\}\right)\left(1\right)=0$$
20	15 18 19	mp2an	$$⊢\left(I\times \left\{0\right\}\right)\left(1\right)=0$$
21	14 20	eqtri	$$⊢\underset{\dot{}}{0}\left(1\right)=0$$
22	21	a1i	$$⊢p\in P\to \underset{\dot{}}{0}\left(1\right)=0$$
23	22	oveq2d	$$⊢p\in P\to p\left(1\right)-\underset{\dot{}}{0}\left(1\right)=p\left(1\right)-0$$
24	1 3	rrx2pxel	$$⊢p\in P\to p\left(1\right)\in ℝ$$
25	24	recnd	$$⊢p\in P\to p\left(1\right)\in ℂ$$
26	25	subid1d	$$⊢p\in P\to p\left(1\right)-0=p\left(1\right)$$
27	23 26	eqtrd	$$⊢p\in P\to p\left(1\right)-\underset{\dot{}}{0}\left(1\right)=p\left(1\right)$$
28	27	oveq1d	$$⊢p\in P\to {\left(p\left(1\right)-\underset{\dot{}}{0}\left(1\right)\right)}^2={p\left(1\right)}^2$$
29	5	fveq1i	$$⊢\underset{\dot{}}{0}\left(2\right)=\left(I\times \left\{0\right\}\right)\left(2\right)$$
30		2ex	$$⊢2\in \mathrm{V}$$
31	30	prid2	$$⊢2\in \left\{1,2\right\}$$
32	31 1	eleqtrri	$$⊢2\in I$$
33		fvconst2g	$$⊢\left(0\in \mathrm{V}\wedge 2\in I\right)\to \left(I\times \left\{0\right\}\right)\left(2\right)=0$$
34	15 32 33	mp2an	$$⊢\left(I\times \left\{0\right\}\right)\left(2\right)=0$$
35	29 34	eqtri	$$⊢\underset{\dot{}}{0}\left(2\right)=0$$
36	35	a1i	$$⊢p\in P\to \underset{\dot{}}{0}\left(2\right)=0$$
37	36	oveq2d	$$⊢p\in P\to p\left(2\right)-\underset{\dot{}}{0}\left(2\right)=p\left(2\right)-0$$
38	1 3	rrx2pyel	$$⊢p\in P\to p\left(2\right)\in ℝ$$
39	38	recnd	$$⊢p\in P\to p\left(2\right)\in ℂ$$
40	39	subid1d	$$⊢p\in P\to p\left(2\right)-0=p\left(2\right)$$
41	37 40	eqtrd	$$⊢p\in P\to p\left(2\right)-\underset{\dot{}}{0}\left(2\right)=p\left(2\right)$$
42	41	oveq1d	$$⊢p\in P\to {\left(p\left(2\right)-\underset{\dot{}}{0}\left(2\right)\right)}^2={p\left(2\right)}^2$$
43	28 42	oveq12d	$$⊢p\in P\to {\left(p\left(1\right)-\underset{\dot{}}{0}\left(1\right)\right)}^2+{\left(p\left(2\right)-\underset{\dot{}}{0}\left(2\right)\right)}^2={p\left(1\right)}^2+{p\left(2\right)}^2$$
44	43	eqeq1d	$$⊢p\in P\to \left({\left(p\left(1\right)-\underset{\dot{}}{0}\left(1\right)\right)}^2+{\left(p\left(2\right)-\underset{\dot{}}{0}\left(2\right)\right)}^2=R^2\leftrightarrow {p\left(1\right)}^2+{p\left(2\right)}^2=R^2\right)$$
45	44	adantl	$$⊢\left(R\in \left[0,\mathrm{+\infty }\right)\wedge p\in P\right)\to \left({\left(p\left(1\right)-\underset{\dot{}}{0}\left(1\right)\right)}^2+{\left(p\left(2\right)-\underset{\dot{}}{0}\left(2\right)\right)}^2=R^2\leftrightarrow {p\left(1\right)}^2+{p\left(2\right)}^2=R^2\right)$$
46	45	rabbidva	$$⊢R\in \left[0,\mathrm{+\infty }\right)\to \left\{p\in P|{\left(p\left(1\right)-\underset{\dot{}}{0}\left(1\right)\right)}^2+{\left(p\left(2\right)-\underset{\dot{}}{0}\left(2\right)\right)}^2=R^2\right\}=\left\{p\in P|{p\left(1\right)}^2+{p\left(2\right)}^2=R^2\right\}$$
47	46 6	syl6eqr	$$⊢R\in \left[0,\mathrm{+\infty }\right)\to \left\{p\in P|{\left(p\left(1\right)-\underset{\dot{}}{0}\left(1\right)\right)}^2+{\left(p\left(2\right)-\underset{\dot{}}{0}\left(2\right)\right)}^2=R^2\right\}=C$$
48	13 47	eqtrd	$$⊢R\in \left[0,\mathrm{+\infty }\right)\to \underset{\dot{}}{0}SR=C$$