Metamath Proof Explorer

Theorem itsclinecirc0

Description: The intersection points of a line through two different points Y and Z and a circle around the origin, using the definition of a line in a two dimensional Euclidean space. (Contributed by AV, 25-Feb-2023) (Proof shortened by AV, 16-May-2023)

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

Proof

Step Hyp Ref Expression
1 itsclc0.i ⊢ 𝐼 = { 1 , 2 }
2 itsclc0.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3 itsclc0.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
4 itsclc0.s ⊢ 𝑆 = ( Sphere ‘ 𝐸 )
5 itsclc0.0 ⊢ 0 = ( 𝐼 × { 0 } )
6 itsclc0.q ⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
7 itsclc0.d ⊢ 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
8 itsclinecirc0.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
9 itsclinecirc0.a ⊢ 𝐴 = ( ( 𝑌 ‘ 2 ) − ( 𝑍 ‘ 2 ) )
10 itsclinecirc0.b ⊢ 𝐵 = ( ( 𝑍 ‘ 1 ) − ( 𝑌 ‘ 1 ) )
11 itsclinecirc0.c ⊢ 𝐶 = ( ( ( 𝑌 ‘ 2 ) · ( 𝑍 ‘ 1 ) ) − ( ( 𝑌 ‘ 1 ) · ( 𝑍 ‘ 2 ) ) )
12 1 2 3 8 9 10 11 rrx2linest2 ⊢ ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) → ( 𝑌 𝐿 𝑍 ) = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } )
13 12 adantr ⊢ ( ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑌 𝐿 𝑍 ) = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } )
14 13 eleq2d ⊢ ( ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ↔ 𝑋 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } ) )
15 14 anbi2d ⊢ ( ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑋 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ) ↔ ( 𝑋 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑋 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } ) ) )
16 1 3 rrx2pyel ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 2 ) ∈ ℝ )
17 16 3ad2ant1 ⊢ ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) → ( 𝑌 ‘ 2 ) ∈ ℝ )
18 1 3 rrx2pyel ⊢ ( 𝑍 ∈ 𝑃 → ( 𝑍 ‘ 2 ) ∈ ℝ )
19 18 3ad2ant2 ⊢ ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) → ( 𝑍 ‘ 2 ) ∈ ℝ )
20 17 19 resubcld ⊢ ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) → ( ( 𝑌 ‘ 2 ) − ( 𝑍 ‘ 2 ) ) ∈ ℝ )
21 9 20 eqeltrid ⊢ ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) → 𝐴 ∈ ℝ )
22 21 adantr ⊢ ( ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐴 ∈ ℝ )
23 1 3 rrx2pxel ⊢ ( 𝑍 ∈ 𝑃 → ( 𝑍 ‘ 1 ) ∈ ℝ )
24 23 3ad2ant2 ⊢ ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) → ( 𝑍 ‘ 1 ) ∈ ℝ )
25 1 3 rrx2pxel ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 1 ) ∈ ℝ )
26 25 3ad2ant1 ⊢ ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
27 24 26 resubcld ⊢ ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) → ( ( 𝑍 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ∈ ℝ )
28 10 27 eqeltrid ⊢ ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) → 𝐵 ∈ ℝ )
29 28 adantr ⊢ ( ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐵 ∈ ℝ )
30 17 24 remulcld ⊢ ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) → ( ( 𝑌 ‘ 2 ) · ( 𝑍 ‘ 1 ) ) ∈ ℝ )
31 26 19 remulcld ⊢ ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) → ( ( 𝑌 ‘ 1 ) · ( 𝑍 ‘ 2 ) ) ∈ ℝ )
32 30 31 resubcld ⊢ ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) → ( ( ( 𝑌 ‘ 2 ) · ( 𝑍 ‘ 1 ) ) − ( ( 𝑌 ‘ 1 ) · ( 𝑍 ‘ 2 ) ) ) ∈ ℝ )
33 11 32 eqeltrid ⊢ ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) → 𝐶 ∈ ℝ )
34 33 adantr ⊢ ( ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐶 ∈ ℝ )
35 1 3 10 9 rrx2pnedifcoorneorr ⊢ ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) → ( 𝐵 ≠ 0 ∨ 𝐴 ≠ 0 ) )
36 35 orcomd ⊢ ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) → ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) )
37 36 adantr ⊢ ( ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) )
38 simpr ⊢ ( ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) )
39 eqid ⊢ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 }
40 1 2 3 4 5 6 7 39 itsclc0 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑋 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑋 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } ) → ( ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) )
41 22 29 34 37 38 40 syl311anc ⊢ ( ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑋 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑋 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } ) → ( ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) )
42 15 41 sylbid ⊢ ( ( ( 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑋 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ) → ( ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) )