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} = ⟨“ 00 ”⟩$
	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} = ⟨“ 00 ”⟩$
6		2sphere0.c	$⊢ C = \{p \in P \| {p (0)}^{2} + {p (1)}^{2} = R^{2}\}$
7		0re	$⊢ 0 \in ℝ$
8	1 3	prelrrx2	$⊢ (0 \in ℝ \land 0 \in ℝ) \to ⟨“ 00 ”⟩ \in P$
9	7 7 8	mp2an	$⊢ ⟨“ 00 ”⟩ \in P$
10	5 9	eqeltri	$⊢ \underset{˙}{0} \in P$
11		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}\}$
12	1 2 3 4 11	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}\}$
13	10 12	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}\}$
14	5	fveq1i	$⊢ \underset{˙}{0} (0) = ⟨“ 00 ”⟩ (0)$
15		c0ex	$⊢ 0 \in V$
16		s2fv0	$⊢ 0 \in V \to ⟨“ 00 ”⟩ (0) = 0$
17	15 16	ax-mp	$⊢ ⟨“ 00 ”⟩ (0) = 0$
18	14 17	eqtri	$⊢ \underset{˙}{0} (0) = 0$
19	18	a1i	$⊢ p \in P \to \underset{˙}{0} (0) = 0$
20	19	oveq2d	$⊢ p \in P \to p (0) - \underset{˙}{0} (0) = p (0) - 0$
21	1 3	rrx2pxel	$⊢ p \in P \to p (0) \in ℝ$
22	21	recnd	$⊢ p \in P \to p (0) \in ℂ$
23	22	subid1d	$⊢ p \in P \to p (0) - 0 = p (0)$
24	20 23	eqtrd	$⊢ p \in P \to p (0) - \underset{˙}{0} (0) = p (0)$
25	24	oveq1d	$⊢ p \in P \to {(p (0) - \underset{˙}{0} (0))}^{2} = {p (0)}^{2}$
26	5	fveq1i	$⊢ \underset{˙}{0} (1) = ⟨“ 00 ”⟩ (1)$
27		s2fv1	$⊢ 0 \in V \to ⟨“ 00 ”⟩ (1) = 0$
28	15 27	ax-mp	$⊢ ⟨“ 00 ”⟩ (1) = 0$
29	26 28	eqtri	$⊢ \underset{˙}{0} (1) = 0$
30	29	a1i	$⊢ p \in P \to \underset{˙}{0} (1) = 0$
31	30	oveq2d	$⊢ p \in P \to p (1) - \underset{˙}{0} (1) = p (1) - 0$
32	1 3	rrx2pyel	$⊢ p \in P \to p (1) \in ℝ$
33	32	recnd	$⊢ p \in P \to p (1) \in ℂ$
34	33	subid1d	$⊢ p \in P \to p (1) - 0 = p (1)$
35	31 34	eqtrd	$⊢ p \in P \to p (1) - \underset{˙}{0} (1) = p (1)$
36	35	oveq1d	$⊢ p \in P \to {(p (1) - \underset{˙}{0} (1))}^{2} = {p (1)}^{2}$
37	25 36	oveq12d	$⊢ p \in P \to {(p (0) - \underset{˙}{0} (0))}^{2} + {(p (1) - \underset{˙}{0} (1))}^{2} = {p (0)}^{2} + {p (1)}^{2}$
38	37	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})$
39	38	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})$
40	39	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}\}$
41	40 6	eqtr4di	$⊢ R \in [0, +∞) \to \{p \in P \| {(p (0) - \underset{˙}{0} (0))}^{2} + {(p (1) - \underset{˙}{0} (1))}^{2} = R^{2}\} = C$
42	13 41	eqtrd	$⊢ R \in [0, +∞) \to \underset{˙}{0} S R = C$

Metamath Proof Explorer

Theorem 2sphere0

Proof