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

Proof

Step Hyp Ref Expression
1 itsclinecirc0b.i I = 1 2
2 itsclinecirc0b.e E = I
3 itsclinecirc0b.p P = I
4 itsclinecirc0b.s S = Sphere E
5 itsclinecirc0b.0 0 ˙ = I × 0
6 itsclinecirc0b.q Q = A 2 + B 2
7 itsclinecirc0b.d D = R 2 Q C 2
8 itsclinecirc0b.l L = Line M E
9 itsclinecirc0b.a A = X 2 Y 2
10 itsclinecirc0b.b B = Y 1 X 1
11 itsclinecirc0b.c C = X 2 Y 1 X 1 Y 2
12 eqid Y 2 X 2 = Y 2 X 2
13 1 2 3 8 10 12 11 rrx2linest X P Y P X Y X L Y = p P | B p 2 = Y 2 X 2 p 1 + C
14 13 adantr X P Y P X Y R + 0 D X L Y = p P | B p 2 = Y 2 X 2 p 1 + C
15 eqcom B p 2 = Y 2 X 2 p 1 + C Y 2 X 2 p 1 + C = B p 2
16 1 3 rrx2pxel Y P Y 1
17 16 adantl X P Y P Y 1
18 1 3 rrx2pxel X P X 1
19 18 adantr X P Y P X 1
20 17 19 resubcld X P Y P Y 1 X 1
21 10 20 eqeltrid X P Y P B
22 21 3adant3 X P Y P X Y B
23 22 ad2antrr X P Y P X Y R + 0 D p P B
24 1 3 rrx2pyel p P p 2
25 24 adantl X P Y P X Y R + 0 D p P p 2
26 23 25 remulcld X P Y P X Y R + 0 D p P B p 2
27 26 recnd X P Y P X Y R + 0 D p P B p 2
28 1 3 rrx2pyel Y P Y 2
29 28 adantl X P Y P Y 2
30 1 3 rrx2pyel X P X 2
31 30 adantr X P Y P X 2
32 29 31 resubcld X P Y P Y 2 X 2
33 32 3adant3 X P Y P X Y Y 2 X 2
34 33 ad2antrr X P Y P X Y R + 0 D p P Y 2 X 2
35 1 3 rrx2pxel p P p 1
36 35 adantl X P Y P X Y R + 0 D p P p 1
37 34 36 remulcld X P Y P X Y R + 0 D p P Y 2 X 2 p 1
38 37 recnd X P Y P X Y R + 0 D p P Y 2 X 2 p 1
39 31 17 remulcld X P Y P X 2 Y 1
40 19 29 remulcld X P Y P X 1 Y 2
41 39 40 resubcld X P Y P X 2 Y 1 X 1 Y 2
42 11 41 eqeltrid X P Y P C
43 42 recnd X P Y P C
44 43 3adant3 X P Y P X Y C
45 44 ad2antrr X P Y P X Y R + 0 D p P C
46 27 38 45 subaddd X P Y P X Y R + 0 D p P B p 2 Y 2 X 2 p 1 = C Y 2 X 2 p 1 + C = B p 2
47 15 46 bitr4id X P Y P X Y R + 0 D p P B p 2 = Y 2 X 2 p 1 + C B p 2 Y 2 X 2 p 1 = C
48 31 29 resubcld X P Y P X 2 Y 2
49 9 48 eqeltrid X P Y P A
50 49 3adant3 X P Y P X Y A
51 50 ad2antrr X P Y P X Y R + 0 D p P A
52 51 36 remulcld X P Y P X Y R + 0 D p P A p 1
53 52 recnd X P Y P X Y R + 0 D p P A p 1
54 53 27 addcomd X P Y P X Y R + 0 D p P A p 1 + B p 2 = B p 2 + A p 1
55 29 3adant3 X P Y P X Y Y 2
56 55 ad2antrr X P Y P X Y R + 0 D p P Y 2
57 56 recnd X P Y P X Y R + 0 D p P Y 2
58 31 3adant3 X P Y P X Y X 2
59 58 ad2antrr X P Y P X Y R + 0 D p P X 2
60 59 recnd X P Y P X Y R + 0 D p P X 2
61 57 60 negsubdi2d X P Y P X Y R + 0 D p P Y 2 X 2 = X 2 Y 2
62 9 61 eqtr4id X P Y P X Y R + 0 D p P A = Y 2 X 2
63 62 oveq1d X P Y P X Y R + 0 D p P A p 1 = Y 2 X 2 p 1
64 32 recnd X P Y P Y 2 X 2
65 64 3adant3 X P Y P X Y Y 2 X 2
66 65 ad2antrr X P Y P X Y R + 0 D p P Y 2 X 2
67 36 recnd X P Y P X Y R + 0 D p P p 1
68 66 67 mulneg1d X P Y P X Y R + 0 D p P Y 2 X 2 p 1 = Y 2 X 2 p 1
69 63 68 eqtr2d X P Y P X Y R + 0 D p P Y 2 X 2 p 1 = A p 1
70 69 oveq2d X P Y P X Y R + 0 D p P B p 2 + Y 2 X 2 p 1 = B p 2 + A p 1
71 27 38 negsubd X P Y P X Y R + 0 D p P B p 2 + Y 2 X 2 p 1 = B p 2 Y 2 X 2 p 1
72 54 70 71 3eqtr2rd X P Y P X Y R + 0 D p P B p 2 Y 2 X 2 p 1 = A p 1 + B p 2
73 72 eqeq1d X P Y P X Y R + 0 D p P B p 2 Y 2 X 2 p 1 = C A p 1 + B p 2 = C
74 47 73 bitrd X P Y P X Y R + 0 D p P B p 2 = Y 2 X 2 p 1 + C A p 1 + B p 2 = C
75 74 rabbidva X P Y P X Y R + 0 D p P | B p 2 = Y 2 X 2 p 1 + C = p P | A p 1 + B p 2 = C
76 14 75 eqtrd X P Y P X Y R + 0 D X L Y = p P | A p 1 + B p 2 = C
77 76 eleq2d X P Y P X Y R + 0 D Z X L Y Z p P | A p 1 + B p 2 = C
78 77 anbi2d X P Y P X Y R + 0 D Z 0 ˙ S R Z X L Y Z 0 ˙ S R Z p P | A p 1 + B p 2 = C
79 50 adantr X P Y P X Y R + 0 D A
80 22 adantr X P Y P X Y R + 0 D B
81 42 3adant3 X P Y P X Y C
82 81 adantr X P Y P X Y R + 0 D C
83 1 3 10 9 rrx2pnedifcoorneorr X P Y P X Y B 0 A 0
84 83 orcomd X P Y P X Y A 0 B 0
85 84 adantr X P Y P X Y R + 0 D A 0 B 0
86 simpr X P Y P X Y R + 0 D R + 0 D
87 eqid p P | A p 1 + B p 2 = C = p P | A p 1 + B p 2 = C
88 1 2 3 4 5 6 7 87 itsclc0b A B C A 0 B 0 R + 0 D Z 0 ˙ S R Z p P | A p 1 + B p 2 = C Z P Z 1 = A C + B D Q Z 2 = B C A D Q Z 1 = A C B D Q Z 2 = B C + A D Q
89 79 80 82 85 86 88 syl311anc X P Y P X Y R + 0 D Z 0 ˙ S R Z p P | A p 1 + B p 2 = C Z P Z 1 = A C + B D Q Z 2 = B C A D Q Z 1 = A C B D Q Z 2 = B C + A D Q
90 78 89 bitrd X P Y P X Y R + 0 D Z 0 ˙ S R Z X L Y Z P Z 1 = A C + B D Q Z 2 = B C A D Q Z 1 = A C B D Q Z 2 = B C + A D Q