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 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 0 ”⟩
6		2sphere0.c	⊢ 𝐶 = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) }
7		0re	⊢ 0 ∈ ℝ
8	1 3	prelrrx2	⊢ ( ( 0 ∈ ℝ ∧ 0 ∈ ℝ ) → ⟨“ 0 0 ”⟩ ∈ 𝑃 )
9	7 7 8	mp2an	⊢ ⟨“ 0 0 ”⟩ ∈ 𝑃
10	5 9	eqeltri	⊢ 0 ∈ 𝑃
11		eqid	⊢ { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } = { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) }
12	1 2 3 4 11	2sphere	⊢ ( ( 0 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( 0 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } )
13	10 12	mpan	⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) → ( 0 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } )
14	5	fveq1i	⊢ ( 0 ‘ 0 ) = ( ⟨“ 0 0 ”⟩ ‘ 0 )
15		c0ex	⊢ 0 ∈ V
16		s2fv0	⊢ ( 0 ∈ V → ( ⟨“ 0 0 ”⟩ ‘ 0 ) = 0 )
17	15 16	ax-mp	⊢ ( ⟨“ 0 0 ”⟩ ‘ 0 ) = 0
18	14 17	eqtri	⊢ ( 0 ‘ 0 ) = 0
19	18	a1i	⊢ ( 𝑝 ∈ 𝑃 → ( 0 ‘ 0 ) = 0 )
20	19	oveq2d	⊢ ( 𝑝 ∈ 𝑃 → ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) = ( ( 𝑝 ‘ 0 ) − 0 ) )
21	1 3	rrx2pxel	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 0 ) ∈ ℝ )
22	21	recnd	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 0 ) ∈ ℂ )
23	22	subid1d	⊢ ( 𝑝 ∈ 𝑃 → ( ( 𝑝 ‘ 0 ) − 0 ) = ( 𝑝 ‘ 0 ) )
24	20 23	eqtrd	⊢ ( 𝑝 ∈ 𝑃 → ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) = ( 𝑝 ‘ 0 ) )
25	24	oveq1d	⊢ ( 𝑝 ∈ 𝑃 → ( ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) = ( ( 𝑝 ‘ 0 ) ↑ 2 ) )
26	5	fveq1i	⊢ ( 0 ‘ 1 ) = ( ⟨“ 0 0 ”⟩ ‘ 1 )
27		s2fv1	⊢ ( 0 ∈ V → ( ⟨“ 0 0 ”⟩ ‘ 1 ) = 0 )
28	15 27	ax-mp	⊢ ( ⟨“ 0 0 ”⟩ ‘ 1 ) = 0
29	26 28	eqtri	⊢ ( 0 ‘ 1 ) = 0
30	29	a1i	⊢ ( 𝑝 ∈ 𝑃 → ( 0 ‘ 1 ) = 0 )
31	30	oveq2d	⊢ ( 𝑝 ∈ 𝑃 → ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) = ( ( 𝑝 ‘ 1 ) − 0 ) )
32	1 3	rrx2pyel	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℝ )
33	32	recnd	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℂ )
34	33	subid1d	⊢ ( 𝑝 ∈ 𝑃 → ( ( 𝑝 ‘ 1 ) − 0 ) = ( 𝑝 ‘ 1 ) )
35	31 34	eqtrd	⊢ ( 𝑝 ∈ 𝑃 → ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) = ( 𝑝 ‘ 1 ) )
36	35	oveq1d	⊢ ( 𝑝 ∈ 𝑃 → ( ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) = ( ( 𝑝 ‘ 1 ) ↑ 2 ) )
37	25 36	oveq12d	⊢ ( 𝑝 ∈ 𝑃 → ( ( ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) = ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) )
38	37	eqeq1d	⊢ ( 𝑝 ∈ 𝑃 → ( ( ( ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ↔ ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
39	38	adantl	⊢ ( ( 𝑅 ∈ ( 0 [,) +∞ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ↔ ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
40	39	rabbidva	⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) → { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } )
41	40 6	eqtr4di	⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) → { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑝 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } = 𝐶 )
42	13 41	eqtrd	⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) → ( 0 𝑆 𝑅 ) = 𝐶 )