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. = <" 0 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. = <" 0 0 ">
6 2sphere0.c 
 |-  C = { p e. P | ( ( ( p ` 0 ) ^ 2 ) + ( ( p ` 1 ) ^ 2 ) ) = ( R ^ 2 ) }
7 0re 
 |-  0 e. RR
8 1 3 prelrrx2 
 |-  ( ( 0 e. RR /\ 0 e. RR ) -> <" 0 0 "> e. P )
9 7 7 8 mp2an 
 |-  <" 0 0 "> e. P
10 5 9 eqeltri 
 |-  .0. e. P
11 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 ) }
12 1 2 3 4 11 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 ) } )
13 10 12 mpan 
 |-  ( R e. ( 0 [,) +oo ) -> ( .0. S R ) = { p e. P | ( ( ( ( p ` 0 ) - ( .0. ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( .0. ` 1 ) ) ^ 2 ) ) = ( R ^ 2 ) } )
14 5 fveq1i 
 |-  ( .0. ` 0 ) = ( <" 0 0 "> ` 0 )
15 c0ex 
 |-  0 e. _V
16 s2fv0 
 |-  ( 0 e. _V -> ( <" 0 0 "> ` 0 ) = 0 )
17 15 16 ax-mp 
 |-  ( <" 0 0 "> ` 0 ) = 0
18 14 17 eqtri 
 |-  ( .0. ` 0 ) = 0
19 18 a1i 
 |-  ( p e. P -> ( .0. ` 0 ) = 0 )
20 19 oveq2d 
 |-  ( p e. P -> ( ( p ` 0 ) - ( .0. ` 0 ) ) = ( ( p ` 0 ) - 0 ) )
21 1 3 rrx2pxel 
 |-  ( p e. P -> ( p ` 0 ) e. RR )
22 21 recnd 
 |-  ( p e. P -> ( p ` 0 ) e. CC )
23 22 subid1d 
 |-  ( p e. P -> ( ( p ` 0 ) - 0 ) = ( p ` 0 ) )
24 20 23 eqtrd 
 |-  ( p e. P -> ( ( p ` 0 ) - ( .0. ` 0 ) ) = ( p ` 0 ) )
25 24 oveq1d 
 |-  ( p e. P -> ( ( ( p ` 0 ) - ( .0. ` 0 ) ) ^ 2 ) = ( ( p ` 0 ) ^ 2 ) )
26 5 fveq1i 
 |-  ( .0. ` 1 ) = ( <" 0 0 "> ` 1 )
27 s2fv1 
 |-  ( 0 e. _V -> ( <" 0 0 "> ` 1 ) = 0 )
28 15 27 ax-mp 
 |-  ( <" 0 0 "> ` 1 ) = 0
29 26 28 eqtri 
 |-  ( .0. ` 1 ) = 0
30 29 a1i 
 |-  ( p e. P -> ( .0. ` 1 ) = 0 )
31 30 oveq2d 
 |-  ( p e. P -> ( ( p ` 1 ) - ( .0. ` 1 ) ) = ( ( p ` 1 ) - 0 ) )
32 1 3 rrx2pyel 
 |-  ( p e. P -> ( p ` 1 ) e. RR )
33 32 recnd 
 |-  ( p e. P -> ( p ` 1 ) e. CC )
34 33 subid1d 
 |-  ( p e. P -> ( ( p ` 1 ) - 0 ) = ( p ` 1 ) )
35 31 34 eqtrd 
 |-  ( p e. P -> ( ( p ` 1 ) - ( .0. ` 1 ) ) = ( p ` 1 ) )
36 35 oveq1d 
 |-  ( p e. P -> ( ( ( p ` 1 ) - ( .0. ` 1 ) ) ^ 2 ) = ( ( p ` 1 ) ^ 2 ) )
37 25 36 oveq12d 
 |-  ( p e. P -> ( ( ( ( p ` 0 ) - ( .0. ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( .0. ` 1 ) ) ^ 2 ) ) = ( ( ( p ` 0 ) ^ 2 ) + ( ( p ` 1 ) ^ 2 ) ) )
38 37 eqeq1d 
 |-  ( p e. P -> ( ( ( ( ( p ` 0 ) - ( .0. ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( .0. ` 1 ) ) ^ 2 ) ) = ( R ^ 2 ) <-> ( ( ( p ` 0 ) ^ 2 ) + ( ( p ` 1 ) ^ 2 ) ) = ( R ^ 2 ) ) )
39 38 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 ) ) )
40 39 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 ) } )
41 40 6 eqtr4di 
 |-  ( R e. ( 0 [,) +oo ) -> { p e. P | ( ( ( ( p ` 0 ) - ( .0. ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( .0. ` 1 ) ) ^ 2 ) ) = ( R ^ 2 ) } = C )
42 13 41 eqtrd 
 |-  ( R e. ( 0 [,) +oo ) -> ( .0. S R ) = C )