Metamath Proof Explorer

Theorem colopp

Description: Opposite sides of a line for colinear points. Theorem 9.18 of Schwabhauser p. 73. (Contributed by Thierry Arnoux, 3-Aug-2020)

Ref Expression
Hypotheses hpgid.p 
|- P = ( Base ` G )
hpgid.i 
|- I = ( Itv ` G )
hpgid.l 
|- L = ( LineG ` G )
hpgid.g 
|- ( ph -> G e. TarskiG )
hpgid.d 
|- ( ph -> D e. ran L )
hpgid.a 
|- ( ph -> A e. P )
hpgid.o 
|- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
colopp.b 
|- ( ph -> B e. P )
colopp.p 
|- ( ph -> C e. D )
colopp.1 
|- ( ph -> ( C e. ( A L B ) \/ A = B ) )
Assertion colopp 
|- ( ph -> ( A O B <-> ( C e. ( A I B ) /\ -. A e. D /\ -. B e. D ) ) )

Proof

Step Hyp Ref Expression
1 hpgid.p 
 |-  P = ( Base ` G )
2 hpgid.i 
 |-  I = ( Itv ` G )
3 hpgid.l 
 |-  L = ( LineG ` G )
4 hpgid.g 
 |-  ( ph -> G e. TarskiG )
5 hpgid.d 
 |-  ( ph -> D e. ran L )
6 hpgid.a 
 |-  ( ph -> A e. P )
7 hpgid.o 
 |-  O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
8 colopp.b 
 |-  ( ph -> B e. P )
9 colopp.p 
 |-  ( ph -> C e. D )
10 colopp.1 
 |-  ( ph -> ( C e. ( A L B ) \/ A = B ) )
11 4 ad3antrrr 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> G e. TarskiG )
12 6 ad3antrrr 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> A e. P )
13 8 ad3antrrr 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> B e. P )
14 eqid 
 |-  ( dist ` G ) = ( dist ` G )
15 5 ad3antrrr 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> D e. ran L )
16 simpllr 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> ( -. A e. D /\ -. B e. D ) )
17 simplr 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> y e. D )
18 eleq1w 
 |-  ( t = y -> ( t e. ( A I B ) <-> y e. ( A I B ) ) )
19 18 adantl 
 |-  ( ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) /\ t = y ) -> ( t e. ( A I B ) <-> y e. ( A I B ) ) )
20 simpr 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> y e. ( A I B ) )
21 17 19 20 rspcedvd 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> E. t e. D t e. ( A I B ) )
22 1 14 2 7 6 8 islnopp 
 |-  ( ph -> ( A O B <-> ( ( -. A e. D /\ -. B e. D ) /\ E. t e. D t e. ( A I B ) ) ) )
23 22 ad3antrrr 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> ( A O B <-> ( ( -. A e. D /\ -. B e. D ) /\ E. t e. D t e. ( A I B ) ) ) )
24 16 21 23 mpbir2and 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> A O B )
25 1 14 2 7 3 15 11 12 13 24 oppne3 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> A =/= B )
26 1 2 3 11 12 13 25 tgelrnln 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> ( A L B ) e. ran L )
27 1 2 3 11 12 13 25 tglinerflx1 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> A e. ( A L B ) )
28 16 simpld 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> -. A e. D )
29 nelne1 
 |-  ( ( A e. ( A L B ) /\ -. A e. D ) -> ( A L B ) =/= D )
30 27 28 29 syl2anc 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> ( A L B ) =/= D )
31 25 neneqd 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> -. A = B )
32 10 orcomd 
 |-  ( ph -> ( A = B \/ C e. ( A L B ) ) )
33 32 ord 
 |-  ( ph -> ( -. A = B -> C e. ( A L B ) ) )
34 33 ad3antrrr 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> ( -. A = B -> C e. ( A L B ) ) )
35 31 34 mpd 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> C e. ( A L B ) )
36 9 ad3antrrr 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> C e. D )
37 35 36 elind 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> C e. ( ( A L B ) i^i D ) )
38 1 3 2 11 15 17 tglnpt 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> y e. P )
39 1 2 3 11 12 13 38 25 20 btwnlng1 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> y e. ( A L B ) )
40 39 17 elind 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> y e. ( ( A L B ) i^i D ) )
41 1 2 3 11 26 15 30 37 40 tglineineq 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> C = y )
42 41 20 eqeltrd 
 |-  ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> C e. ( A I B ) )
43 42 adantllr 
 |-  ( ( ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ E. t e. D t e. ( A I B ) ) /\ y e. D ) /\ y e. ( A I B ) ) -> C e. ( A I B ) )
44 simpr 
 |-  ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ E. t e. D t e. ( A I B ) ) -> E. t e. D t e. ( A I B ) )
45 18 cbvrexvw 
 |-  ( E. t e. D t e. ( A I B ) <-> E. y e. D y e. ( A I B ) )
46 44 45 sylib 
 |-  ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ E. t e. D t e. ( A I B ) ) -> E. y e. D y e. ( A I B ) )
47 43 46 r19.29a 
 |-  ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ E. t e. D t e. ( A I B ) ) -> C e. ( A I B ) )
48 9 adantr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> C e. D )
49 simpr 
 |-  ( ( ( ph /\ C e. ( A I B ) ) /\ t = C ) -> t = C )
50 49 eleq1d 
 |-  ( ( ( ph /\ C e. ( A I B ) ) /\ t = C ) -> ( t e. ( A I B ) <-> C e. ( A I B ) ) )
51 simpr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> C e. ( A I B ) )
52 48 50 51 rspcedvd 
 |-  ( ( ph /\ C e. ( A I B ) ) -> E. t e. D t e. ( A I B ) )
53 52 adantlr 
 |-  ( ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) /\ C e. ( A I B ) ) -> E. t e. D t e. ( A I B ) )
54 47 53 impbida 
 |-  ( ( ph /\ ( -. A e. D /\ -. B e. D ) ) -> ( E. t e. D t e. ( A I B ) <-> C e. ( A I B ) ) )
55 54 pm5.32da 
 |-  ( ph -> ( ( ( -. A e. D /\ -. B e. D ) /\ E. t e. D t e. ( A I B ) ) <-> ( ( -. A e. D /\ -. B e. D ) /\ C e. ( A I B ) ) ) )
56 3anrot 
 |-  ( ( C e. ( A I B ) /\ -. A e. D /\ -. B e. D ) <-> ( -. A e. D /\ -. B e. D /\ C e. ( A I B ) ) )
57 df-3an 
 |-  ( ( -. A e. D /\ -. B e. D /\ C e. ( A I B ) ) <-> ( ( -. A e. D /\ -. B e. D ) /\ C e. ( A I B ) ) )
58 56 57 bitri 
 |-  ( ( C e. ( A I B ) /\ -. A e. D /\ -. B e. D ) <-> ( ( -. A e. D /\ -. B e. D ) /\ C e. ( A I B ) ) )
59 58 a1i 
 |-  ( ph -> ( ( C e. ( A I B ) /\ -. A e. D /\ -. B e. D ) <-> ( ( -. A e. D /\ -. B e. D ) /\ C e. ( A I B ) ) ) )
60 55 22 59 3bitr4d 
 |-  ( ph -> ( A O B <-> ( C e. ( A I B ) /\ -. A e. D /\ -. B e. D ) ) )