Metamath Proof Explorer

Theorem opphllem1

Description: Lemma for opphl . (Contributed by Thierry Arnoux, 20-Dec-2019)

Ref Expression
Hypotheses hpg.p 
|- P = ( Base ` G )
hpg.d 
|- .- = ( dist ` G )
hpg.i 
|- I = ( Itv ` G )
hpg.o 
|- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
opphl.l 
|- L = ( LineG ` G )
opphl.d 
|- ( ph -> D e. ran L )
opphl.g 
|- ( ph -> G e. TarskiG )
opphllem1.s 
|- S = ( ( pInvG ` G ) ` M )
opphllem1.a 
|- ( ph -> A e. P )
opphllem1.b 
|- ( ph -> B e. P )
opphllem1.c 
|- ( ph -> C e. P )
opphllem1.r 
|- ( ph -> R e. D )
opphllem1.o 
|- ( ph -> A O C )
opphllem1.m 
|- ( ph -> M e. D )
opphllem1.n 
|- ( ph -> A = ( S ` C ) )
opphllem1.x 
|- ( ph -> A =/= R )
opphllem1.y 
|- ( ph -> B =/= R )
opphllem1.z 
|- ( ph -> B e. ( R I A ) )
Assertion opphllem1 
|- ( ph -> B O C )

Proof

Step Hyp Ref Expression
1 hpg.p 
 |-  P = ( Base ` G )
2 hpg.d 
 |-  .- = ( dist ` G )
3 hpg.i 
 |-  I = ( Itv ` G )
4 hpg.o 
 |-  O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
5 opphl.l 
 |-  L = ( LineG ` G )
6 opphl.d 
 |-  ( ph -> D e. ran L )
7 opphl.g 
 |-  ( ph -> G e. TarskiG )
8 opphllem1.s 
 |-  S = ( ( pInvG ` G ) ` M )
9 opphllem1.a 
 |-  ( ph -> A e. P )
10 opphllem1.b 
 |-  ( ph -> B e. P )
11 opphllem1.c 
 |-  ( ph -> C e. P )
12 opphllem1.r 
 |-  ( ph -> R e. D )
13 opphllem1.o 
 |-  ( ph -> A O C )
14 opphllem1.m 
 |-  ( ph -> M e. D )
15 opphllem1.n 
 |-  ( ph -> A = ( S ` C ) )
16 opphllem1.x 
 |-  ( ph -> A =/= R )
17 opphllem1.y 
 |-  ( ph -> B =/= R )
18 opphllem1.z 
 |-  ( ph -> B e. ( R I A ) )
19 1 2 3 4 5 6 7 9 11 13 oppne1 
 |-  ( ph -> -. A e. D )
20 simpr 
 |-  ( ( ( ph /\ B e. D ) /\ A = B ) -> A = B )
21 simplr 
 |-  ( ( ( ph /\ B e. D ) /\ A = B ) -> B e. D )
22 20 21 eqeltrd 
 |-  ( ( ( ph /\ B e. D ) /\ A = B ) -> A e. D )
23 7 ad2antrr 
 |-  ( ( ( ph /\ B e. D ) /\ A =/= B ) -> G e. TarskiG )
24 10 ad2antrr 
 |-  ( ( ( ph /\ B e. D ) /\ A =/= B ) -> B e. P )
25 1 5 3 7 6 12 tglnpt 
 |-  ( ph -> R e. P )
26 25 ad2antrr 
 |-  ( ( ( ph /\ B e. D ) /\ A =/= B ) -> R e. P )
27 9 ad2antrr 
 |-  ( ( ( ph /\ B e. D ) /\ A =/= B ) -> A e. P )
28 17 ad2antrr 
 |-  ( ( ( ph /\ B e. D ) /\ A =/= B ) -> B =/= R )
29 28 necomd 
 |-  ( ( ( ph /\ B e. D ) /\ A =/= B ) -> R =/= B )
30 18 ad2antrr 
 |-  ( ( ( ph /\ B e. D ) /\ A =/= B ) -> B e. ( R I A ) )
31 1 3 5 23 26 24 27 29 30 btwnlng3 
 |-  ( ( ( ph /\ B e. D ) /\ A =/= B ) -> A e. ( R L B ) )
32 1 3 5 23 24 26 27 28 31 lncom 
 |-  ( ( ( ph /\ B e. D ) /\ A =/= B ) -> A e. ( B L R ) )
33 6 ad2antrr 
 |-  ( ( ( ph /\ B e. D ) /\ A =/= B ) -> D e. ran L )
34 simplr 
 |-  ( ( ( ph /\ B e. D ) /\ A =/= B ) -> B e. D )
35 12 ad2antrr 
 |-  ( ( ( ph /\ B e. D ) /\ A =/= B ) -> R e. D )
36 1 3 5 23 24 26 28 28 33 34 35 tglinethru 
 |-  ( ( ( ph /\ B e. D ) /\ A =/= B ) -> D = ( B L R ) )
37 32 36 eleqtrrd 
 |-  ( ( ( ph /\ B e. D ) /\ A =/= B ) -> A e. D )
38 22 37 pm2.61dane 
 |-  ( ( ph /\ B e. D ) -> A e. D )
39 19 38 mtand 
 |-  ( ph -> -. B e. D )
40 1 2 3 4 5 6 7 9 11 13 oppne2 
 |-  ( ph -> -. C e. D )
41 1 5 3 7 6 14 tglnpt 
 |-  ( ph -> M e. P )
42 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
43 1 2 3 5 42 7 41 8 9 mirbtwn 
 |-  ( ph -> M e. ( ( S ` A ) I A ) )
44 15 eqcomd 
 |-  ( ph -> ( S ` C ) = A )
45 1 2 3 5 42 7 41 8 11 44 mircom 
 |-  ( ph -> ( S ` A ) = C )
46 45 oveq1d 
 |-  ( ph -> ( ( S ` A ) I A ) = ( C I A ) )
47 43 46 eleqtrd 
 |-  ( ph -> M e. ( C I A ) )
48 1 2 3 7 25 11 9 10 41 18 47 axtgpasch 
 |-  ( ph -> E. t e. P ( t e. ( B I C ) /\ t e. ( M I R ) ) )
49 7 ad2antrr 
 |-  ( ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) /\ M = R ) -> G e. TarskiG )
50 25 ad2antrr 
 |-  ( ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) /\ M = R ) -> R e. P )
51 simplrl 
 |-  ( ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) /\ M = R ) -> t e. P )
52 simplrr 
 |-  ( ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) /\ M = R ) -> ( t e. ( B I C ) /\ t e. ( M I R ) ) )
53 52 simprd 
 |-  ( ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) /\ M = R ) -> t e. ( M I R ) )
54 simpr 
 |-  ( ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) /\ M = R ) -> M = R )
55 54 oveq1d 
 |-  ( ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) /\ M = R ) -> ( M I R ) = ( R I R ) )
56 53 55 eleqtrd 
 |-  ( ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) /\ M = R ) -> t e. ( R I R ) )
57 1 2 3 49 50 51 56 axtgbtwnid 
 |-  ( ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) /\ M = R ) -> R = t )
58 12 ad2antrr 
 |-  ( ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) /\ M = R ) -> R e. D )
59 57 58 eqeltrrd 
 |-  ( ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) /\ M = R ) -> t e. D )
60 7 ad2antrr 
 |-  ( ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) /\ M =/= R ) -> G e. TarskiG )
61 41 ad2antrr 
 |-  ( ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) /\ M =/= R ) -> M e. P )
62 25 ad2antrr 
 |-  ( ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) /\ M =/= R ) -> R e. P )
63 simplrl 
 |-  ( ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) /\ M =/= R ) -> t e. P )
64 simpr 
 |-  ( ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) /\ M =/= R ) -> M =/= R )
65 simplrr 
 |-  ( ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) /\ M =/= R ) -> ( t e. ( B I C ) /\ t e. ( M I R ) ) )
66 65 simprd 
 |-  ( ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) /\ M =/= R ) -> t e. ( M I R ) )
67 1 3 5 60 61 62 63 64 66 btwnlng1 
 |-  ( ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) /\ M =/= R ) -> t e. ( M L R ) )
68 7 adantr 
 |-  ( ( ph /\ M =/= R ) -> G e. TarskiG )
69 41 adantr 
 |-  ( ( ph /\ M =/= R ) -> M e. P )
70 25 adantr 
 |-  ( ( ph /\ M =/= R ) -> R e. P )
71 simpr 
 |-  ( ( ph /\ M =/= R ) -> M =/= R )
72 6 adantr 
 |-  ( ( ph /\ M =/= R ) -> D e. ran L )
73 14 adantr 
 |-  ( ( ph /\ M =/= R ) -> M e. D )
74 12 adantr 
 |-  ( ( ph /\ M =/= R ) -> R e. D )
75 1 3 5 68 69 70 71 71 72 73 74 tglinethru 
 |-  ( ( ph /\ M =/= R ) -> D = ( M L R ) )
76 75 adantlr 
 |-  ( ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) /\ M =/= R ) -> D = ( M L R ) )
77 67 76 eleqtrrd 
 |-  ( ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) /\ M =/= R ) -> t e. D )
78 59 77 pm2.61dane 
 |-  ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) -> t e. D )
79 simprrl 
 |-  ( ( ph /\ ( t e. P /\ ( t e. ( B I C ) /\ t e. ( M I R ) ) ) ) -> t e. ( B I C ) )
80 48 78 79 reximssdv 
 |-  ( ph -> E. t e. D t e. ( B I C ) )
81 39 40 80 jca31 
 |-  ( ph -> ( ( -. B e. D /\ -. C e. D ) /\ E. t e. D t e. ( B I C ) ) )
82 1 2 3 4 10 11 islnopp 
 |-  ( ph -> ( B O C <-> ( ( -. B e. D /\ -. C e. D ) /\ E. t e. D t e. ( B I C ) ) ) )
83 81 82 mpbird 
 |-  ( ph -> B O C )