Metamath Proof Explorer


Theorem itsclinecirc0b

Description: The intersection points of a line through two different points and a circle around the origin, using the definition of a line in a two dimensional Euclidean space. (Contributed by AV, 2-May-2023) (Revised by AV, 14-May-2023)

Ref Expression
Hypotheses itsclinecirc0b.i 𝐼 = { 1 , 2 }
itsclinecirc0b.e 𝐸 = ( ℝ^ ‘ 𝐼 )
itsclinecirc0b.p 𝑃 = ( ℝ ↑m 𝐼 )
itsclinecirc0b.s 𝑆 = ( Sphere ‘ 𝐸 )
itsclinecirc0b.0 0 = ( 𝐼 × { 0 } )
itsclinecirc0b.q 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
itsclinecirc0b.d 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
itsclinecirc0b.l 𝐿 = ( LineM𝐸 )
itsclinecirc0b.a 𝐴 = ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) )
itsclinecirc0b.b 𝐵 = ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) )
itsclinecirc0b.c 𝐶 = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) )
Assertion itsclinecirc0b ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ) ↔ ( 𝑍𝑃 ∧ ( ( ( 𝑍 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑍 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑍 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑍 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 itsclinecirc0b.i 𝐼 = { 1 , 2 }
2 itsclinecirc0b.e 𝐸 = ( ℝ^ ‘ 𝐼 )
3 itsclinecirc0b.p 𝑃 = ( ℝ ↑m 𝐼 )
4 itsclinecirc0b.s 𝑆 = ( Sphere ‘ 𝐸 )
5 itsclinecirc0b.0 0 = ( 𝐼 × { 0 } )
6 itsclinecirc0b.q 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
7 itsclinecirc0b.d 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
8 itsclinecirc0b.l 𝐿 = ( LineM𝐸 )
9 itsclinecirc0b.a 𝐴 = ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) )
10 itsclinecirc0b.b 𝐵 = ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) )
11 itsclinecirc0b.c 𝐶 = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) )
12 eqid ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) )
13 1 2 3 8 10 12 11 rrx2linest ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝𝑃 ∣ ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) } )
14 13 adantr ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝𝑃 ∣ ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) } )
15 eqcom ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) ↔ ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) = ( 𝐵 · ( 𝑝 ‘ 2 ) ) )
16 1 3 rrx2pxel ( 𝑌𝑃 → ( 𝑌 ‘ 1 ) ∈ ℝ )
17 16 adantl ( ( 𝑋𝑃𝑌𝑃 ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
18 1 3 rrx2pxel ( 𝑋𝑃 → ( 𝑋 ‘ 1 ) ∈ ℝ )
19 18 adantr ( ( 𝑋𝑃𝑌𝑃 ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
20 17 19 resubcld ( ( 𝑋𝑃𝑌𝑃 ) → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ∈ ℝ )
21 10 20 eqeltrid ( ( 𝑋𝑃𝑌𝑃 ) → 𝐵 ∈ ℝ )
22 21 3adant3 ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → 𝐵 ∈ ℝ )
23 22 ad2antrr ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → 𝐵 ∈ ℝ )
24 1 3 rrx2pyel ( 𝑝𝑃 → ( 𝑝 ‘ 2 ) ∈ ℝ )
25 24 adantl ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( 𝑝 ‘ 2 ) ∈ ℝ )
26 23 25 remulcld ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( 𝐵 · ( 𝑝 ‘ 2 ) ) ∈ ℝ )
27 26 recnd ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( 𝐵 · ( 𝑝 ‘ 2 ) ) ∈ ℂ )
28 1 3 rrx2pyel ( 𝑌𝑃 → ( 𝑌 ‘ 2 ) ∈ ℝ )
29 28 adantl ( ( 𝑋𝑃𝑌𝑃 ) → ( 𝑌 ‘ 2 ) ∈ ℝ )
30 1 3 rrx2pyel ( 𝑋𝑃 → ( 𝑋 ‘ 2 ) ∈ ℝ )
31 30 adantr ( ( 𝑋𝑃𝑌𝑃 ) → ( 𝑋 ‘ 2 ) ∈ ℝ )
32 29 31 resubcld ( ( 𝑋𝑃𝑌𝑃 ) → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ∈ ℝ )
33 32 3adant3 ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ∈ ℝ )
34 33 ad2antrr ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ∈ ℝ )
35 1 3 rrx2pxel ( 𝑝𝑃 → ( 𝑝 ‘ 1 ) ∈ ℝ )
36 35 adantl ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( 𝑝 ‘ 1 ) ∈ ℝ )
37 34 36 remulcld ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ∈ ℝ )
38 37 recnd ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ∈ ℂ )
39 31 17 remulcld ( ( 𝑋𝑃𝑌𝑃 ) → ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) ∈ ℝ )
40 19 29 remulcld ( ( 𝑋𝑃𝑌𝑃 ) → ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ∈ ℝ )
41 39 40 resubcld ( ( 𝑋𝑃𝑌𝑃 ) → ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ∈ ℝ )
42 11 41 eqeltrid ( ( 𝑋𝑃𝑌𝑃 ) → 𝐶 ∈ ℝ )
43 42 recnd ( ( 𝑋𝑃𝑌𝑃 ) → 𝐶 ∈ ℂ )
44 43 3adant3 ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → 𝐶 ∈ ℂ )
45 44 ad2antrr ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → 𝐶 ∈ ℂ )
46 27 38 45 subaddd ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) − ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) = ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) )
47 15 46 bitr4id ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) ↔ ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) − ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ) )
48 31 29 resubcld ( ( 𝑋𝑃𝑌𝑃 ) → ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ∈ ℝ )
49 9 48 eqeltrid ( ( 𝑋𝑃𝑌𝑃 ) → 𝐴 ∈ ℝ )
50 49 3adant3 ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → 𝐴 ∈ ℝ )
51 50 ad2antrr ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → 𝐴 ∈ ℝ )
52 51 36 remulcld ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( 𝐴 · ( 𝑝 ‘ 1 ) ) ∈ ℝ )
53 52 recnd ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( 𝐴 · ( 𝑝 ‘ 1 ) ) ∈ ℂ )
54 53 27 addcomd ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) + ( 𝐴 · ( 𝑝 ‘ 1 ) ) ) )
55 29 3adant3 ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( 𝑌 ‘ 2 ) ∈ ℝ )
56 55 ad2antrr ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( 𝑌 ‘ 2 ) ∈ ℝ )
57 56 recnd ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( 𝑌 ‘ 2 ) ∈ ℂ )
58 31 3adant3 ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( 𝑋 ‘ 2 ) ∈ ℝ )
59 58 ad2antrr ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( 𝑋 ‘ 2 ) ∈ ℝ )
60 59 recnd ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( 𝑋 ‘ 2 ) ∈ ℂ )
61 57 60 negsubdi2d ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → - ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) )
62 9 61 eqtr4id ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → 𝐴 = - ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) )
63 62 oveq1d ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( 𝐴 · ( 𝑝 ‘ 1 ) ) = ( - ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) )
64 32 recnd ( ( 𝑋𝑃𝑌𝑃 ) → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ∈ ℂ )
65 64 3adant3 ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ∈ ℂ )
66 65 ad2antrr ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ∈ ℂ )
67 36 recnd ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( 𝑝 ‘ 1 ) ∈ ℂ )
68 66 67 mulneg1d ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( - ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) = - ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) )
69 63 68 eqtr2d ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → - ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) = ( 𝐴 · ( 𝑝 ‘ 1 ) ) )
70 69 oveq2d ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) + - ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) = ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) + ( 𝐴 · ( 𝑝 ‘ 1 ) ) ) )
71 27 38 negsubd ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) + - ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) = ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) − ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) )
72 54 70 71 3eqtr2rd ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) − ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) = ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) )
73 72 eqeq1d ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) − ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ) )
74 47 73 bitrd ( ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝𝑃 ) → ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) ↔ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ) )
75 74 rabbidva ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → { 𝑝𝑃 ∣ ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) } = { 𝑝𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } )
76 14 75 eqtrd ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } )
77 76 eleq2d ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ↔ 𝑍 ∈ { 𝑝𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } ) )
78 77 anbi2d ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ) ↔ ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑍 ∈ { 𝑝𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } ) ) )
79 50 adantr ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐴 ∈ ℝ )
80 22 adantr ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐵 ∈ ℝ )
81 42 3adant3 ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → 𝐶 ∈ ℝ )
82 81 adantr ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐶 ∈ ℝ )
83 1 3 10 9 rrx2pnedifcoorneorr ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( 𝐵 ≠ 0 ∨ 𝐴 ≠ 0 ) )
84 83 orcomd ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) )
85 84 adantr ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) )
86 simpr ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) )
87 eqid { 𝑝𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } = { 𝑝𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 }
88 1 2 3 4 5 6 7 87 itsclc0b ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑍 ∈ { 𝑝𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } ) ↔ ( 𝑍𝑃 ∧ ( ( ( 𝑍 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑍 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑍 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑍 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )
89 79 80 82 85 86 88 syl311anc ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑍 ∈ { 𝑝𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } ) ↔ ( 𝑍𝑃 ∧ ( ( ( 𝑍 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑍 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑍 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑍 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )
90 78 89 bitrd ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ) ↔ ( 𝑍𝑃 ∧ ( ( ( 𝑍 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑍 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑍 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑍 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )