Metamath Proof Explorer


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=msup
rrxspheres.p P=I
rrxspheres.d D=distE
rrxspheres.s S=SphereE
Assertion rrxsphere IFinMPRMSR=pP|pDM=R

Proof

Step Hyp Ref Expression
1 rrxspheres.e E=msup
2 rrxspheres.p P=I
3 rrxspheres.d D=distE
4 rrxspheres.s S=SphereE
5 1 fvexi EV
6 id IFinIFin
7 eqid BaseE=BaseE
8 6 1 7 rrxbasefi IFinBaseE=I
9 2 8 eqtr4id IFinP=BaseE
10 9 eleq2d IFinMPMBaseE
11 10 biimpa IFinMPMBaseE
12 11 3adant3 IFinMPRMBaseE
13 12 adantl 0RIFinMPRMBaseE
14 rexr RR*
15 14 3ad2ant3 IFinMPRR*
16 15 anim2i 0RIFinMPR0RR*
17 16 ancomd 0RIFinMPRR*0R
18 elxrge0 R0+∞R*0R
19 17 18 sylibr 0RIFinMPRR0+∞
20 7 4 3 sphere EVMBaseER0+∞MSR=pBaseE|pDM=R
21 5 13 19 20 mp3an2i 0RIFinMPRMSR=pBaseE|pDM=R
22 simp1 IFinMPRIFin
23 22 1 7 rrxbasefi IFinMPRBaseE=I
24 23 2 eqtr4di IFinMPRBaseE=P
25 24 adantl 0RIFinMPRBaseE=P
26 25 rabeqdv 0RIFinMPRpBaseE|pDM=R=pP|pDM=R
27 21 26 eqtrd 0RIFinMPRMSR=pP|pDM=R
28 27 ex 0RIFinMPRMSR=pP|pDM=R
29 7 4 3 spheres EVS=xBaseE,r0+∞pBaseE|pDx=r
30 5 29 ax-mp S=xBaseE,r0+∞pBaseE|pDx=r
31 fvex BaseEV
32 31 rabex pBaseE|pDx=rV
33 30 32 dmmpo domS=BaseE×0+∞
34 0xr 0*
35 pnfxr +∞*
36 34 35 pm3.2i 0*+∞*
37 elicc1 0*+∞*R0+∞R*0RR+∞
38 36 37 mp1i IFinMPRR0+∞R*0RR+∞
39 simp2 R*0RR+∞0R
40 38 39 syl6bi IFinMPRR0+∞0R
41 40 con3d IFinMPR¬0R¬R0+∞
42 41 imp IFinMPR¬0R¬R0+∞
43 42 intnand IFinMPR¬0R¬MBaseER0+∞
44 ndmovg domS=BaseE×0+∞¬MBaseER0+∞MSR=
45 33 43 44 sylancr IFinMPR¬0RMSR=
46 1 fveq2i distE=distmsup
47 3 46 eqtri D=distmsup
48 47 rrxmetfi IFinDMetI
49 48 3ad2ant1 IFinMPRDMetI
50 49 adantr IFinMPRpPDMetI
51 2 fveq2i MetP=MetI
52 50 51 eleqtrrdi IFinMPRpPDMetP
53 simpr IFinMPRpPpP
54 simp2 IFinMPRMP
55 54 adantr IFinMPRpPMP
56 metge0 DMetPpPMP0pDM
57 52 53 55 56 syl3anc IFinMPRpP0pDM
58 breq2 pDM=R0pDM0R
59 57 58 syl5ibcom IFinMPRpPpDM=R0R
60 59 con3d IFinMPRpP¬0R¬pDM=R
61 60 impancom IFinMPR¬0RpP¬pDM=R
62 61 imp IFinMPR¬0RpP¬pDM=R
63 62 ralrimiva IFinMPR¬0RpP¬pDM=R
64 eqcom =pP|pDM=RpP|pDM=R=
65 rabeq0 pP|pDM=R=pP¬pDM=R
66 64 65 bitri =pP|pDM=RpP¬pDM=R
67 63 66 sylibr IFinMPR¬0R=pP|pDM=R
68 45 67 eqtrd IFinMPR¬0RMSR=pP|pDM=R
69 68 expcom ¬0RIFinMPRMSR=pP|pDM=R
70 28 69 pm2.61i IFinMPRMSR=pP|pDM=R