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 = ( RR^ ` I )
itsclc0.p 
|- P = ( RR ^m I )
itsclc0.s 
|- S = ( Sphere ` E )
itsclc0.0 
|- .0. = ( I X. { 0 } )
itsclc0.q 
|- Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
itsclc0.d 
|- D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
itsclinecirc0.l 
|- L = ( LineM ` E )
itsclinecirc0.a 
|- A = ( ( Y ` 2 ) - ( Z ` 2 ) )
itsclinecirc0.b 
|- B = ( ( Z ` 1 ) - ( Y ` 1 ) )
itsclinecirc0.c 
|- C = ( ( ( Y ` 2 ) x. ( Z ` 1 ) ) - ( ( Y ` 1 ) x. ( Z ` 2 ) ) )
Assertion itsclinecirc0 
|- ( ( ( Y e. P /\ Z e. P /\ Y =/= Z ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( X e. ( .0. S R ) /\ X e. ( Y L Z ) ) -> ( ( ( X ` 1 ) = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( X ` 2 ) = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( ( X ` 1 ) = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( X ` 2 ) = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) )

Proof

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