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 = 1 2
2sphere.e E = I
2sphere.p P = I
2sphere.s S = Sphere E
2sphere0.0 0 ˙ = I × 0
2sphere0.c C = p P | p 1 2 + p 2 2 = R 2
Assertion 2sphere0 R 0 +∞ 0 ˙ S R = C

Proof

Step Hyp Ref Expression
1 2sphere.i I = 1 2
2 2sphere.e E = I
3 2sphere.p P = I
4 2sphere.s S = Sphere E
5 2sphere0.0 0 ˙ = I × 0
6 2sphere0.c C = p P | p 1 2 + p 2 2 = R 2
7 prex 1 2 V
8 1 7 eqeltri I V
9 5 3 rrx0el I V 0 ˙ P
10 8 9 ax-mp 0 ˙ P
11 eqid p P | p 1 0 ˙ 1 2 + p 2 0 ˙ 2 2 = R 2 = p P | p 1 0 ˙ 1 2 + p 2 0 ˙ 2 2 = R 2
12 1 2 3 4 11 2sphere 0 ˙ P R 0 +∞ 0 ˙ S R = p P | p 1 0 ˙ 1 2 + p 2 0 ˙ 2 2 = R 2
13 10 12 mpan R 0 +∞ 0 ˙ S R = p P | p 1 0 ˙ 1 2 + p 2 0 ˙ 2 2 = R 2
14 5 fveq1i 0 ˙ 1 = I × 0 1
15 c0ex 0 V
16 1ex 1 V
17 16 prid1 1 1 2
18 17 1 eleqtrri 1 I
19 fvconst2g 0 V 1 I I × 0 1 = 0
20 15 18 19 mp2an I × 0 1 = 0
21 14 20 eqtri 0 ˙ 1 = 0
22 21 a1i p P 0 ˙ 1 = 0
23 22 oveq2d p P p 1 0 ˙ 1 = p 1 0
24 1 3 rrx2pxel p P p 1
25 24 recnd p P p 1
26 25 subid1d p P p 1 0 = p 1
27 23 26 eqtrd p P p 1 0 ˙ 1 = p 1
28 27 oveq1d p P p 1 0 ˙ 1 2 = p 1 2
29 5 fveq1i 0 ˙ 2 = I × 0 2
30 2ex 2 V
31 30 prid2 2 1 2
32 31 1 eleqtrri 2 I
33 fvconst2g 0 V 2 I I × 0 2 = 0
34 15 32 33 mp2an I × 0 2 = 0
35 29 34 eqtri 0 ˙ 2 = 0
36 35 a1i p P 0 ˙ 2 = 0
37 36 oveq2d p P p 2 0 ˙ 2 = p 2 0
38 1 3 rrx2pyel p P p 2
39 38 recnd p P p 2
40 39 subid1d p P p 2 0 = p 2
41 37 40 eqtrd p P p 2 0 ˙ 2 = p 2
42 41 oveq1d p P p 2 0 ˙ 2 2 = p 2 2
43 28 42 oveq12d p P p 1 0 ˙ 1 2 + p 2 0 ˙ 2 2 = p 1 2 + p 2 2
44 43 eqeq1d p P p 1 0 ˙ 1 2 + p 2 0 ˙ 2 2 = R 2 p 1 2 + p 2 2 = R 2
45 44 adantl R 0 +∞ p P p 1 0 ˙ 1 2 + p 2 0 ˙ 2 2 = R 2 p 1 2 + p 2 2 = R 2
46 45 rabbidva R 0 +∞ p P | p 1 0 ˙ 1 2 + p 2 0 ˙ 2 2 = R 2 = p P | p 1 2 + p 2 2 = R 2
47 46 6 eqtr4di R 0 +∞ p P | p 1 0 ˙ 1 2 + p 2 0 ˙ 2 2 = R 2 = C
48 13 47 eqtrd R 0 +∞ 0 ˙ S R = C