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

Proof

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