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 = ( 0 ..^ 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 ` 0 ) ^ 2 ) + ( ( p ` 1 ) ^ 2 ) ) = ( R ^ 2 ) }
Assertion 2sphere0 
|- ( R e. ( 0 [,) +oo ) -> ( .0. S R ) = C )

Proof

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