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 = (0 ..^2)$
	2sphere.e	$⊢ E = I$
	2sphere.p	$⊢ P = ℝ^{I}$
	2sphere.s	$⊢ S = Sphere (E)$
	2sphere0.0	$⊢ \underset{˙}{0} = I \times \{0\}$
	2sphere0.c	$⊢ C = \{p \in P \| {p (0)}^{2} + {p (1)}^{2} = R^{2}\}$
Assertion	2sphere0	$⊢ R \in [0, +∞) \to \underset{˙}{0} S R = C$

Proof

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

Metamath Proof Explorer

Theorem 2sphere0

Proof