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 I = 1 2
itsclc0.e E = I
itsclc0.p P = I
itsclc0.s S = Sphere E
itsclc0.0 0 ˙ = I × 0
itsclc0.q Q = A 2 + B 2
itsclc0.d D = R 2 Q C 2
itsclinecirc0.l L = Line M E
itsclinecirc0.a A = Y 2 Z 2
itsclinecirc0.b B = Z 1 Y 1
itsclinecirc0.c C = Y 2 Z 1 Y 1 Z 2
Assertion itsclinecirc0 Y P Z P Y Z R + 0 D X 0 ˙ S R X Y L Z X 1 = A C + B D Q X 2 = B C A D Q X 1 = A C B D Q X 2 = B C + A D Q

Proof

Step Hyp Ref Expression
1 itsclc0.i I = 1 2
2 itsclc0.e E = I
3 itsclc0.p P = I
4 itsclc0.s S = Sphere E
5 itsclc0.0 0 ˙ = I × 0
6 itsclc0.q Q = A 2 + B 2
7 itsclc0.d D = R 2 Q C 2
8 itsclinecirc0.l L = Line M E
9 itsclinecirc0.a A = Y 2 Z 2
10 itsclinecirc0.b B = Z 1 Y 1
11 itsclinecirc0.c C = Y 2 Z 1 Y 1 Z 2
12 1 2 3 8 9 10 11 rrx2linest2 Y P Z P Y Z Y L Z = p P | A p 1 + B p 2 = C
13 12 adantr Y P Z P Y Z R + 0 D Y L Z = p P | A p 1 + B p 2 = C
14 13 eleq2d Y P Z P Y Z R + 0 D X Y L Z X p P | A p 1 + B p 2 = C
15 14 anbi2d Y P Z P Y Z R + 0 D X 0 ˙ S R X Y L Z X 0 ˙ S R X p P | A p 1 + B p 2 = C
16 1 3 rrx2pyel Y P Y 2
17 16 3ad2ant1 Y P Z P Y Z Y 2
18 1 3 rrx2pyel Z P Z 2
19 18 3ad2ant2 Y P Z P Y Z Z 2
20 17 19 resubcld Y P Z P Y Z Y 2 Z 2
21 9 20 eqeltrid Y P Z P Y Z A
22 21 adantr Y P Z P Y Z R + 0 D A
23 1 3 rrx2pxel Z P Z 1
24 23 3ad2ant2 Y P Z P Y Z Z 1
25 1 3 rrx2pxel Y P Y 1
26 25 3ad2ant1 Y P Z P Y Z Y 1
27 24 26 resubcld Y P Z P Y Z Z 1 Y 1
28 10 27 eqeltrid Y P Z P Y Z B
29 28 adantr Y P Z P Y Z R + 0 D B
30 17 24 remulcld Y P Z P Y Z Y 2 Z 1
31 26 19 remulcld Y P Z P Y Z Y 1 Z 2
32 30 31 resubcld Y P Z P Y Z Y 2 Z 1 Y 1 Z 2
33 11 32 eqeltrid Y P Z P Y Z C
34 33 adantr Y P Z P Y Z R + 0 D C
35 1 3 10 9 rrx2pnedifcoorneorr Y P Z P Y Z B 0 A 0
36 35 orcomd Y P Z P Y Z A 0 B 0
37 36 adantr Y P Z P Y Z R + 0 D A 0 B 0
38 simpr Y P Z P Y Z R + 0 D R + 0 D
39 eqid p P | A p 1 + B p 2 = C = p P | A p 1 + B p 2 = C
40 1 2 3 4 5 6 7 39 itsclc0 A B C A 0 B 0 R + 0 D X 0 ˙ S R X p P | A p 1 + B p 2 = C X 1 = A C + B D Q X 2 = B C A D Q X 1 = A C B D Q X 2 = B C + A D Q
41 22 29 34 37 38 40 syl311anc Y P Z P Y Z R + 0 D X 0 ˙ S R X p P | A p 1 + B p 2 = C X 1 = A C + B D Q X 2 = B C A D Q X 1 = A C B D Q X 2 = B C + A D Q
42 15 41 sylbid Y P Z P Y Z R + 0 D X 0 ˙ S R X Y L Z X 1 = A C + B D Q X 2 = B C A D Q X 1 = A C B D Q X 2 = B C + A D Q