Metamath Proof Explorer


Theorem 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=12
2sphere.e E=msup
2sphere.p P=I
2sphere.s S=SphereE
2sphere0.0 0˙=I×0
2sphere0.c C=pP|p12+p22=R2
Assertion 2sphere0 R0+∞0˙SR=C

Proof

Step Hyp Ref Expression
1 2sphere.i I=12
2 2sphere.e E=msup
3 2sphere.p P=I
4 2sphere.s S=SphereE
5 2sphere0.0 0˙=I×0
6 2sphere0.c C=pP|p12+p22=R2
7 prex 12V
8 1 7 eqeltri IV
9 5 3 rrx0el IV0˙P
10 8 9 ax-mp 0˙P
11 eqid pP|p10˙12+p20˙22=R2=pP|p10˙12+p20˙22=R2
12 1 2 3 4 11 2sphere 0˙PR0+∞0˙SR=pP|p10˙12+p20˙22=R2
13 10 12 mpan R0+∞0˙SR=pP|p10˙12+p20˙22=R2
14 5 fveq1i 0˙1=I×01
15 c0ex 0V
16 1ex 1V
17 16 prid1 112
18 17 1 eleqtrri 1I
19 fvconst2g 0V1II×01=0
20 15 18 19 mp2an I×01=0
21 14 20 eqtri 0˙1=0
22 21 a1i pP0˙1=0
23 22 oveq2d pPp10˙1=p10
24 1 3 rrx2pxel pPp1
25 24 recnd pPp1
26 25 subid1d pPp10=p1
27 23 26 eqtrd pPp10˙1=p1
28 27 oveq1d pPp10˙12=p12
29 5 fveq1i 0˙2=I×02
30 2ex 2V
31 30 prid2 212
32 31 1 eleqtrri 2I
33 fvconst2g 0V2II×02=0
34 15 32 33 mp2an I×02=0
35 29 34 eqtri 0˙2=0
36 35 a1i pP0˙2=0
37 36 oveq2d pPp20˙2=p20
38 1 3 rrx2pyel pPp2
39 38 recnd pPp2
40 39 subid1d pPp20=p2
41 37 40 eqtrd pPp20˙2=p2
42 41 oveq1d pPp20˙22=p22
43 28 42 oveq12d pPp10˙12+p20˙22=p12+p22
44 43 eqeq1d pPp10˙12+p20˙22=R2p12+p22=R2
45 44 adantl R0+∞pPp10˙12+p20˙22=R2p12+p22=R2
46 45 rabbidva R0+∞pP|p10˙12+p20˙22=R2=pP|p12+p22=R2
47 46 6 eqtr4di R0+∞pP|p10˙12+p20˙22=R2=C
48 13 47 eqtrd R0+∞0˙SR=C