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	⊢ 𝐼 = ( 0 ..^ 2 )
	2sphere.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
	2sphere.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
	2sphere.s	⊢ 𝑆 = ( Sphere ‘ 𝐸 )
	2sphere0.0	⊢ 0 = ( 𝐼 × { 0 } )
	2sphere0.c	⊢ 𝐶 = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) }
Assertion	2sphere0	⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) → ( 0 𝑆 𝑅 ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		2sphere.i	⊢ 𝐼 = ( 0 ..^ 2 )
2		2sphere.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3		2sphere.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
4		2sphere.s	⊢ 𝑆 = ( Sphere ‘ 𝐸 )
5		2sphere0.0	⊢ 0 = ( 𝐼 × { 0 } )
6		2sphere0.c	⊢ 𝐶 = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) }
7	1	ovexi	⊢ 𝐼 ∈ V
8	5 3	rrx0el	⊢ ( 𝐼 ∈ V → 0 ∈ 𝑃 )
9	7 8	ax-mp	⊢ 0 ∈ 𝑃
10		eqid	⊢ { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } = { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) }
11	1 2 3 4 10	2sphere	⊢ ( ( 0 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( 0 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } )
12	9 11	mpan	⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) → ( 0 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } )
13	5	fveq1i	⊢ ( 0 ‘ 0 ) = ( ( 𝐼 × { 0 } ) ‘ 0 )
14		c0ex	⊢ 0 ∈ V
15		0elpr01	⊢ 0 ∈ { 0 , 1 }
16		fzo0to2pr	⊢ ( 0 ..^ 2 ) = { 0 , 1 }
17	1 16	eqtri	⊢ 𝐼 = { 0 , 1 }
18	15 17	eleqtrri	⊢ 0 ∈ 𝐼
19		fvconst2g	⊢ ( ( 0 ∈ V ∧ 0 ∈ 𝐼 ) → ( ( 𝐼 × { 0 } ) ‘ 0 ) = 0 )
20	14 18 19	mp2an	⊢ ( ( 𝐼 × { 0 } ) ‘ 0 ) = 0
21	13 20	eqtri	⊢ ( 0 ‘ 0 ) = 0
22	21	a1i	⊢ ( 𝑝 ∈ 𝑃 → ( 0 ‘ 0 ) = 0 )
23	22	oveq2d	⊢ ( 𝑝 ∈ 𝑃 → ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) = ( ( 𝑝 ‘ 0 ) − 0 ) )
24	1 3	rrx2pxel	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 0 ) ∈ ℝ )
25	24	recnd	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 0 ) ∈ ℂ )
26	25	subid1d	⊢ ( 𝑝 ∈ 𝑃 → ( ( 𝑝 ‘ 0 ) − 0 ) = ( 𝑝 ‘ 0 ) )
27	23 26	eqtrd	⊢ ( 𝑝 ∈ 𝑃 → ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) = ( 𝑝 ‘ 0 ) )
28	27	oveq1d	⊢ ( 𝑝 ∈ 𝑃 → ( ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) = ( ( 𝑝 ‘ 0 ) ↑ 2 ) )
29	5	fveq1i	⊢ ( 0 ‘ 1 ) = ( ( 𝐼 × { 0 } ) ‘ 1 )
30		1elpr01	⊢ 1 ∈ { 0 , 1 }
31	30 17	eleqtrri	⊢ 1 ∈ 𝐼
32		fvconst2g	⊢ ( ( 0 ∈ V ∧ 1 ∈ 𝐼 ) → ( ( 𝐼 × { 0 } ) ‘ 1 ) = 0 )
33	14 31 32	mp2an	⊢ ( ( 𝐼 × { 0 } ) ‘ 1 ) = 0
34	29 33	eqtri	⊢ ( 0 ‘ 1 ) = 0
35	34	a1i	⊢ ( 𝑝 ∈ 𝑃 → ( 0 ‘ 1 ) = 0 )
36	35	oveq2d	⊢ ( 𝑝 ∈ 𝑃 → ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) = ( ( 𝑝 ‘ 1 ) − 0 ) )
37	1 3	rrx2pyel	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℝ )
38	37	recnd	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℂ )
39	38	subid1d	⊢ ( 𝑝 ∈ 𝑃 → ( ( 𝑝 ‘ 1 ) − 0 ) = ( 𝑝 ‘ 1 ) )
40	36 39	eqtrd	⊢ ( 𝑝 ∈ 𝑃 → ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) = ( 𝑝 ‘ 1 ) )
41	40	oveq1d	⊢ ( 𝑝 ∈ 𝑃 → ( ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) = ( ( 𝑝 ‘ 1 ) ↑ 2 ) )
42	28 41	oveq12d	⊢ ( 𝑝 ∈ 𝑃 → ( ( ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) = ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) )
43	42	eqeq1d	⊢ ( 𝑝 ∈ 𝑃 → ( ( ( ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ↔ ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
44	43	adantl	⊢ ( ( 𝑅 ∈ ( 0 [,) +∞ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ↔ ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
45	44	rabbidva	⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) → { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } )
46	45 6	eqtr4di	⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) → { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } = 𝐶 )
47	12 46	eqtrd	⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) → ( 0 𝑆 𝑅 ) = 𝐶 )