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 = ( RR^ ` I )
2sphere.p 
|- P = ( RR ^m I )
2sphere.s 
|- S = ( Sphere ` E )
2sphere0.0 
|- .0. = ( I X. { 0 } )
2sphere0.c 
|- C = { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) }
Assertion 2sphere0 
|- ( R e. ( 0 [,) +oo ) -> ( .0. S R ) = C )

Proof

Step Hyp Ref Expression
1 2sphere.i 
 |-  I = { 1 , 2 }
2 2sphere.e 
 |-  E = ( RR^ ` I )
3 2sphere.p 
 |-  P = ( RR ^m I )
4 2sphere.s 
 |-  S = ( Sphere ` E )
5 2sphere0.0 
 |-  .0. = ( I X. { 0 } )
6 2sphere0.c 
 |-  C = { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) }
7 prex 
 |-  { 1 , 2 } e. _V
8 1 7 eqeltri 
 |-  I e. _V
9 5 3 rrx0el 
 |-  ( I e. _V -> .0. e. P )
10 8 9 ax-mp 
 |-  .0. e. P
11 eqid 
 |-  { p e. P | ( ( ( ( p ` 1 ) - ( .0. ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( .0. ` 2 ) ) ^ 2 ) ) = ( R ^ 2 ) } = { p e. P | ( ( ( ( p ` 1 ) - ( .0. ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( .0. ` 2 ) ) ^ 2 ) ) = ( R ^ 2 ) }
12 1 2 3 4 11 2sphere 
 |-  ( ( .0. e. P /\ R e. ( 0 [,) +oo ) ) -> ( .0. S R ) = { p e. P | ( ( ( ( p ` 1 ) - ( .0. ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( .0. ` 2 ) ) ^ 2 ) ) = ( R ^ 2 ) } )
13 10 12 mpan 
 |-  ( R e. ( 0 [,) +oo ) -> ( .0. S R ) = { p e. P | ( ( ( ( p ` 1 ) - ( .0. ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( .0. ` 2 ) ) ^ 2 ) ) = ( R ^ 2 ) } )
14 5 fveq1i 
 |-  ( .0. ` 1 ) = ( ( I X. { 0 } ) ` 1 )
15 c0ex 
 |-  0 e. _V
16 1ex 
 |-  1 e. _V
17 16 prid1 
 |-  1 e. { 1 , 2 }
18 17 1 eleqtrri 
 |-  1 e. I
19 fvconst2g 
 |-  ( ( 0 e. _V /\ 1 e. I ) -> ( ( I X. { 0 } ) ` 1 ) = 0 )
20 15 18 19 mp2an 
 |-  ( ( I X. { 0 } ) ` 1 ) = 0
21 14 20 eqtri 
 |-  ( .0. ` 1 ) = 0
22 21 a1i 
 |-  ( p e. P -> ( .0. ` 1 ) = 0 )
23 22 oveq2d 
 |-  ( p e. P -> ( ( p ` 1 ) - ( .0. ` 1 ) ) = ( ( p ` 1 ) - 0 ) )
24 1 3 rrx2pxel 
 |-  ( p e. P -> ( p ` 1 ) e. RR )
25 24 recnd 
 |-  ( p e. P -> ( p ` 1 ) e. CC )
26 25 subid1d 
 |-  ( p e. P -> ( ( p ` 1 ) - 0 ) = ( p ` 1 ) )
27 23 26 eqtrd 
 |-  ( p e. P -> ( ( p ` 1 ) - ( .0. ` 1 ) ) = ( p ` 1 ) )
28 27 oveq1d 
 |-  ( p e. P -> ( ( ( p ` 1 ) - ( .0. ` 1 ) ) ^ 2 ) = ( ( p ` 1 ) ^ 2 ) )
29 5 fveq1i 
 |-  ( .0. ` 2 ) = ( ( I X. { 0 } ) ` 2 )
30 2ex 
 |-  2 e. _V
31 30 prid2 
 |-  2 e. { 1 , 2 }
32 31 1 eleqtrri 
 |-  2 e. I
33 fvconst2g 
 |-  ( ( 0 e. _V /\ 2 e. I ) -> ( ( I X. { 0 } ) ` 2 ) = 0 )
34 15 32 33 mp2an 
 |-  ( ( I X. { 0 } ) ` 2 ) = 0
35 29 34 eqtri 
 |-  ( .0. ` 2 ) = 0
36 35 a1i 
 |-  ( p e. P -> ( .0. ` 2 ) = 0 )
37 36 oveq2d 
 |-  ( p e. P -> ( ( p ` 2 ) - ( .0. ` 2 ) ) = ( ( p ` 2 ) - 0 ) )
38 1 3 rrx2pyel 
 |-  ( p e. P -> ( p ` 2 ) e. RR )
39 38 recnd 
 |-  ( p e. P -> ( p ` 2 ) e. CC )
40 39 subid1d 
 |-  ( p e. P -> ( ( p ` 2 ) - 0 ) = ( p ` 2 ) )
41 37 40 eqtrd 
 |-  ( p e. P -> ( ( p ` 2 ) - ( .0. ` 2 ) ) = ( p ` 2 ) )
42 41 oveq1d 
 |-  ( p e. P -> ( ( ( p ` 2 ) - ( .0. ` 2 ) ) ^ 2 ) = ( ( p ` 2 ) ^ 2 ) )
43 28 42 oveq12d 
 |-  ( p e. P -> ( ( ( ( p ` 1 ) - ( .0. ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( .0. ` 2 ) ) ^ 2 ) ) = ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) )
44 43 eqeq1d 
 |-  ( p e. 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 e. ( 0 [,) +oo ) /\ p e. 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 e. ( 0 [,) +oo ) -> { p e. P | ( ( ( ( p ` 1 ) - ( .0. ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( .0. ` 2 ) ) ^ 2 ) ) = ( R ^ 2 ) } = { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) } )
47 46 6 eqtr4di 
 |-  ( R e. ( 0 [,) +oo ) -> { p e. P | ( ( ( ( p ` 1 ) - ( .0. ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( .0. ` 2 ) ) ^ 2 ) ) = ( R ^ 2 ) } = C )
48 13 47 eqtrd 
 |-  ( R e. ( 0 [,) +oo ) -> ( .0. S R ) = C )