rrxsphere

Description: The sphere with center M and radius R in a generalized real Euclidean space of finite dimension. Remark: this theorem holds also for the degenerate case R < 0 (negative radius): in this case, ( M S R ) is empty. (Contributed by AV, 5-Feb-2023)

	Ref	Expression
Hypotheses	rrxspheres.e	$⊢ E = I$
	rrxspheres.p	$⊢ P = ℝ^{I}$
	rrxspheres.d	$⊢ D = dist (E)$
	rrxspheres.s	$⊢ S = Sphere (E)$
Assertion	rrxsphere	$⊢ (I \in Fin \land M \in P \land R \in ℝ) \to M S R = \{p \in P \| p D M = R\}$

Proof

Step	Hyp	Ref	Expression
1		rrxspheres.e	$⊢ E = I$
2		rrxspheres.p	$⊢ P = ℝ^{I}$
3		rrxspheres.d	$⊢ D = dist (E)$
4		rrxspheres.s	$⊢ S = Sphere (E)$
5	1	fvexi	$⊢ E \in V$
6		id	$⊢ I \in Fin \to I \in Fin$
7		eqid	$⊢ {Base}_{E} = {Base}_{E}$
8	6 1 7	rrxbasefi	$⊢ I \in Fin \to {Base}_{E} = ℝ^{I}$
9	2 8	eqtr4id	$⊢ I \in Fin \to P = {Base}_{E}$
10	9	eleq2d	$⊢ I \in Fin \to (M \in P \leftrightarrow M \in {Base}_{E})$
11	10	biimpa	$⊢ (I \in Fin \land M \in P) \to M \in {Base}_{E}$
12	11	3adant3	$⊢ (I \in Fin \land M \in P \land R \in ℝ) \to M \in {Base}_{E}$
13	12	adantl	$⊢ (0 \leq R \land (I \in Fin \land M \in P \land R \in ℝ)) \to M \in {Base}_{E}$
14		rexr	$⊢ R \in ℝ \to R \in ℝ^{*}$
15	14	3ad2ant3	$⊢ (I \in Fin \land M \in P \land R \in ℝ) \to R \in ℝ^{*}$
16	15	anim2i	$⊢ (0 \leq R \land (I \in Fin \land M \in P \land R \in ℝ)) \to (0 \leq R \land R \in ℝ^{*})$
17	16	ancomd	$⊢ (0 \leq R \land (I \in Fin \land M \in P \land R \in ℝ)) \to (R \in ℝ^{*} \land 0 \leq R)$
18		elxrge0	$⊢ R \in [0, +∞] \leftrightarrow (R \in ℝ^{*} \land 0 \leq R)$
19	17 18	sylibr	$⊢ (0 \leq R \land (I \in Fin \land M \in P \land R \in ℝ)) \to R \in [0, +∞]$
20	7 4 3	sphere	$⊢ (E \in V \land M \in {Base}_{E} \land R \in [0, +∞]) \to M S R = \{p \in {Base}_{E} \| p D M = R\}$
21	5 13 19 20	mp3an2i	$⊢ (0 \leq R \land (I \in Fin \land M \in P \land R \in ℝ)) \to M S R = \{p \in {Base}_{E} \| p D M = R\}$
22		simp1	$⊢ (I \in Fin \land M \in P \land R \in ℝ) \to I \in Fin$
23	22 1 7	rrxbasefi	$⊢ (I \in Fin \land M \in P \land R \in ℝ) \to {Base}_{E} = ℝ^{I}$
24	23 2	eqtr4di	$⊢ (I \in Fin \land M \in P \land R \in ℝ) \to {Base}_{E} = P$
25	24	adantl	$⊢ (0 \leq R \land (I \in Fin \land M \in P \land R \in ℝ)) \to {Base}_{E} = P$
26	25	rabeqdv	$⊢ (0 \leq R \land (I \in Fin \land M \in P \land R \in ℝ)) \to \{p \in {Base}_{E} \| p D M = R\} = \{p \in P \| p D M = R\}$
27	21 26	eqtrd	$⊢ (0 \leq R \land (I \in Fin \land M \in P \land R \in ℝ)) \to M S R = \{p \in P \| p D M = R\}$
28	27	ex	$⊢ 0 \leq R \to ((I \in Fin \land M \in P \land R \in ℝ) \to M S R = \{p \in P \| p D M = R\})$
29	7 4 3	spheres	$⊢ E \in V \to S = (x \in {Base}_{E}, r \in [0, +∞] ⟼ \{p \in {Base}_{E} \| p D x = r\})$
30	5 29	ax-mp	$⊢ S = (x \in {Base}_{E}, r \in [0, +∞] ⟼ \{p \in {Base}_{E} \| p D x = r\})$
31		fvex	$⊢ {Base}_{E} \in V$
32	31	rabex	$⊢ \{p \in {Base}_{E} \| p D x = r\} \in V$
33	30 32	dmmpo	$⊢ dom S = {Base}_{E} \times [0, +∞]$
34		0xr	$⊢ 0 \in ℝ^{*}$
35		pnfxr	$⊢ +∞ \in ℝ^{*}$
36	34 35	pm3.2i	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{})$
37		elicc1	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{}) \to (R \in [0, +∞] \leftrightarrow (R \in ℝ^{*} \land 0 \leq R \land R \leq +∞))$
38	36 37	mp1i	$⊢ (I \in Fin \land M \in P \land R \in ℝ) \to (R \in [0, +∞] \leftrightarrow (R \in ℝ^{*} \land 0 \leq R \land R \leq +∞))$
39		simp2	$⊢ (R \in ℝ^{*} \land 0 \leq R \land R \leq +∞) \to 0 \leq R$
40	38 39	biimtrdi	$⊢ (I \in Fin \land M \in P \land R \in ℝ) \to (R \in [0, +∞] \to 0 \leq R)$
41	40	con3d	$⊢ (I \in Fin \land M \in P \land R \in ℝ) \to (\neg 0 \leq R \to \neg R \in [0, +∞])$
42	41	imp	$⊢ ((I \in Fin \land M \in P \land R \in ℝ) \land \neg 0 \leq R) \to \neg R \in [0, +∞]$
43	42	intnand	$⊢ ((I \in Fin \land M \in P \land R \in ℝ) \land \neg 0 \leq R) \to \neg (M \in {Base}_{E} \land R \in [0, +∞])$
44		ndmovg	$⊢ (dom S = {Base}_{E} \times [0, +∞] \land \neg (M \in {Base}_{E} \land R \in [0, +∞])) \to M S R = \emptyset$
45	33 43 44	sylancr	$⊢ ((I \in Fin \land M \in P \land R \in ℝ) \land \neg 0 \leq R) \to M S R = \emptyset$
46	1	fveq2i	$⊢ dist (E) = dist (I)$
47	3 46	eqtri	$⊢ D = dist (I)$
48	47	rrxmetfi	$⊢ I \in Fin \to D \in Met (ℝ^{I})$
49	48	3ad2ant1	$⊢ (I \in Fin \land M \in P \land R \in ℝ) \to D \in Met (ℝ^{I})$
50	49	adantr	$⊢ ((I \in Fin \land M \in P \land R \in ℝ) \land p \in P) \to D \in Met (ℝ^{I})$
51	2	fveq2i	$⊢ Met (P) = Met (ℝ^{I})$
52	50 51	eleqtrrdi	$⊢ ((I \in Fin \land M \in P \land R \in ℝ) \land p \in P) \to D \in Met (P)$
53		simpr	$⊢ ((I \in Fin \land M \in P \land R \in ℝ) \land p \in P) \to p \in P$
54		simp2	$⊢ (I \in Fin \land M \in P \land R \in ℝ) \to M \in P$
55	54	adantr	$⊢ ((I \in Fin \land M \in P \land R \in ℝ) \land p \in P) \to M \in P$
56		metge0	$⊢ (D \in Met (P) \land p \in P \land M \in P) \to 0 \leq p D M$
57	52 53 55 56	syl3anc	$⊢ ((I \in Fin \land M \in P \land R \in ℝ) \land p \in P) \to 0 \leq p D M$
58		breq2	$⊢ p D M = R \to (0 \leq p D M \leftrightarrow 0 \leq R)$
59	57 58	syl5ibcom	$⊢ ((I \in Fin \land M \in P \land R \in ℝ) \land p \in P) \to (p D M = R \to 0 \leq R)$
60	59	con3d	$⊢ ((I \in Fin \land M \in P \land R \in ℝ) \land p \in P) \to (\neg 0 \leq R \to \neg p D M = R)$
61	60	impancom	$⊢ ((I \in Fin \land M \in P \land R \in ℝ) \land \neg 0 \leq R) \to (p \in P \to \neg p D M = R)$
62	61	imp	$⊢ (((I \in Fin \land M \in P \land R \in ℝ) \land \neg 0 \leq R) \land p \in P) \to \neg p D M = R$
63	62	ralrimiva	$⊢ ((I \in Fin \land M \in P \land R \in ℝ) \land \neg 0 \leq R) \to \forall p \in P \neg p D M = R$
64		eqcom	$⊢ \emptyset = \{p \in P \| p D M = R\} \leftrightarrow \{p \in P \| p D M = R\} = \emptyset$
65		rabeq0	$⊢ \{p \in P \| p D M = R\} = \emptyset \leftrightarrow \forall p \in P \neg p D M = R$
66	64 65	bitri	$⊢ \emptyset = \{p \in P \| p D M = R\} \leftrightarrow \forall p \in P \neg p D M = R$
67	63 66	sylibr	$⊢ ((I \in Fin \land M \in P \land R \in ℝ) \land \neg 0 \leq R) \to \emptyset = \{p \in P \| p D M = R\}$
68	45 67	eqtrd	$⊢ ((I \in Fin \land M \in P \land R \in ℝ) \land \neg 0 \leq R) \to M S R = \{p \in P \| p D M = R\}$
69	68	expcom	$⊢ \neg 0 \leq R \to ((I \in Fin \land M \in P \land R \in ℝ) \to M S R = \{p \in P \| p D M = R\})$
70	28 69	pm2.61i	$⊢ (I \in Fin \land M \in P \land R \in ℝ) \to M S R = \{p \in P \| p D M = R\}$

Metamath Proof Explorer

Theorem rrxsphere

Proof