Theorem 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 = ( RR^ ` I )
	rrxspheres.p	|- P = ( RR ^m I )
	rrxspheres.d	|- D = ( dist ` E )
	rrxspheres.s	|- S = ( Sphere ` E )
Assertion	rrxsphere	|- ( ( I e. Fin /\ M e. P /\ R e. RR ) -> ( M S R ) = { p e. P | ( p D M ) = R } )

Proof

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