Theorem inlinecirc02preu

Description: Intersection of a line with a circle: A line passing through a point within a circle around the origin intersects the circle at exactly two different points, expressed with restricted uniqueness (and without the definition of proper pairs). (Contributed by AV, 16-May-2023)

	Ref	Expression
Hypotheses	inlinecirc02p.i	$$⊢I=\left\{1,2\right\}$$
	inlinecirc02p.e
	inlinecirc02p.p	$$⊢P={ℝ}^I$$
	inlinecirc02p.s	$$⊢S=Sphere\left(E\right)$$
	inlinecirc02p.0	$$⊢\underset{\dot{}}{0}=I\times \left\{0\right\}$$
	inlinecirc02p.l	$$⊢L={Line}_M\left(E\right)$$
	inlinecirc02p.d	$$⊢D=\mathrm{dist}\left(E\right)$$
Assertion	inlinecirc02preu	$$⊢\left(\left(X\in P\wedge Y\in P\wedge X\ne Y\right)\wedge \left(R\in {ℝ}^{+}\wedge XD\underset{\dot{}}{0}<R\right)\right)\to \exists !p\in 𝒫P\left(\left|p\right|=2\wedge p=\left(\underset{\dot{}}{0}SR\right)\cap \left(XLY\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		inlinecirc02p.i	$$⊢I=\left\{1,2\right\}$$
2		inlinecirc02p.e
3		inlinecirc02p.p	$$⊢P={ℝ}^I$$
4		inlinecirc02p.s	$$⊢S=Sphere\left(E\right)$$
5		inlinecirc02p.0	$$⊢\underset{\dot{}}{0}=I\times \left\{0\right\}$$
6		inlinecirc02p.l	$$⊢L={Line}_M\left(E\right)$$
7		inlinecirc02p.d	$$⊢D=\mathrm{dist}\left(E\right)$$
8	1 2 3 4 5 6 7	inlinecirc02p	$$⊢\left(\left(X\in P\wedge Y\in P\wedge X\ne Y\right)\wedge \left(R\in {ℝ}^{+}\wedge XD\underset{\dot{}}{0}<R\right)\right)\to \left(\underset{\dot{}}{0}SR\right)\cap \left(XLY\right)\in \mathrm{PrPairs}\left(P\right)$$
9		reueq	$$⊢\left(\underset{\dot{}}{0}SR\right)\cap \left(XLY\right)\in \mathrm{PrPairs}\left(P\right)\leftrightarrow \exists !p\in \mathrm{PrPairs}\left(P\right)p=\left(\underset{\dot{}}{0}SR\right)\cap \left(XLY\right)$$
10	8 9	sylib	$$⊢\left(\left(X\in P\wedge Y\in P\wedge X\ne Y\right)\wedge \left(R\in {ℝ}^{+}\wedge XD\underset{\dot{}}{0}<R\right)\right)\to \exists !p\in \mathrm{PrPairs}\left(P\right)p=\left(\underset{\dot{}}{0}SR\right)\cap \left(XLY\right)$$
11	3	ovexi	$$⊢P\in \mathrm{V}$$
12		prprreueq	$$⊢P\in \mathrm{V}\to \left(\exists !p\in \mathrm{PrPairs}\left(P\right)p=\left(\underset{\dot{}}{0}SR\right)\cap \left(XLY\right)\leftrightarrow \exists !p\in 𝒫P\left(\left|p\right|=2\wedge p=\left(\underset{\dot{}}{0}SR\right)\cap \left(XLY\right)\right)\right)$$
13	11 12	mp1i	$$⊢\left(\left(X\in P\wedge Y\in P\wedge X\ne Y\right)\wedge \left(R\in {ℝ}^{+}\wedge XD\underset{\dot{}}{0}<R\right)\right)\to \left(\exists !p\in \mathrm{PrPairs}\left(P\right)p=\left(\underset{\dot{}}{0}SR\right)\cap \left(XLY\right)\leftrightarrow \exists !p\in 𝒫P\left(\left|p\right|=2\wedge p=\left(\underset{\dot{}}{0}SR\right)\cap \left(XLY\right)\right)\right)$$
14	10 13	mpbid	$$⊢\left(\left(X\in P\wedge Y\in P\wedge X\ne Y\right)\wedge \left(R\in {ℝ}^{+}\wedge XD\underset{\dot{}}{0}<R\right)\right)\to \exists !p\in 𝒫P\left(\left|p\right|=2\wedge p=\left(\underset{\dot{}}{0}SR\right)\cap \left(XLY\right)\right)$$