Metamath Proof Explorer

Theorem opphllem2

Description: Lemma for opphl . Lemma 9.3 of Schwabhauser p. 68. (Contributed by Thierry Arnoux, 21-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 )
opphllem2.z 
|- ( ph -> ( A e. ( R I B ) \/ B e. ( R I A ) ) )
Assertion opphllem2 
|- ( 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 opphllem2.z 
 |-  ( ph -> ( A e. ( R I B ) \/ B e. ( R I A ) ) )
19 6 adantr 
 |-  ( ( ph /\ A e. ( R I B ) ) -> D e. ran L )
20 7 adantr 
 |-  ( ( ph /\ A e. ( R I B ) ) -> G e. TarskiG )
21 11 adantr 
 |-  ( ( ph /\ A e. ( R I B ) ) -> C e. P )
22 10 adantr 
 |-  ( ( ph /\ A e. ( R I B ) ) -> B e. P )
23 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
24 1 5 3 7 6 14 tglnpt 
 |-  ( ph -> M e. P )
25 24 adantr 
 |-  ( ( ph /\ A e. ( R I B ) ) -> M e. P )
26 1 2 3 5 23 20 25 8 22 mircl 
 |-  ( ( ph /\ A e. ( R I B ) ) -> ( S ` B ) e. P )
27 14 adantr 
 |-  ( ( ph /\ A e. ( R I B ) ) -> M e. D )
28 12 adantr 
 |-  ( ( ph /\ A e. ( R I B ) ) -> R e. D )
29 1 2 3 5 23 20 8 19 27 28 mirln 
 |-  ( ( ph /\ A e. ( R I B ) ) -> ( S ` R ) e. D )
30 simpr 
 |-  ( ( ( ( ph /\ A e. ( R I B ) ) /\ B e. D ) /\ A = B ) -> A = B )
31 simplr 
 |-  ( ( ( ( ph /\ A e. ( R I B ) ) /\ B e. D ) /\ A = B ) -> B e. D )
32 30 31 eqeltrd 
 |-  ( ( ( ( ph /\ A e. ( R I B ) ) /\ B e. D ) /\ A = B ) -> A e. D )
33 7 ad3antrrr 
 |-  ( ( ( ( ph /\ A e. ( R I B ) ) /\ B e. D ) /\ A =/= B ) -> G e. TarskiG )
34 10 ad3antrrr 
 |-  ( ( ( ( ph /\ A e. ( R I B ) ) /\ B e. D ) /\ A =/= B ) -> B e. P )
35 1 5 3 7 6 12 tglnpt 
 |-  ( ph -> R e. P )
36 35 ad3antrrr 
 |-  ( ( ( ( ph /\ A e. ( R I B ) ) /\ B e. D ) /\ A =/= B ) -> R e. P )
37 9 ad3antrrr 
 |-  ( ( ( ( ph /\ A e. ( R I B ) ) /\ B e. D ) /\ A =/= B ) -> A e. P )
38 17 ad3antrrr 
 |-  ( ( ( ( ph /\ A e. ( R I B ) ) /\ B e. D ) /\ A =/= B ) -> B =/= R )
39 38 necomd 
 |-  ( ( ( ( ph /\ A e. ( R I B ) ) /\ B e. D ) /\ A =/= B ) -> R =/= B )
40 simpllr 
 |-  ( ( ( ( ph /\ A e. ( R I B ) ) /\ B e. D ) /\ A =/= B ) -> A e. ( R I B ) )
41 1 3 5 33 36 34 37 39 40 btwnlng1 
 |-  ( ( ( ( ph /\ A e. ( R I B ) ) /\ B e. D ) /\ A =/= B ) -> A e. ( R L B ) )
42 1 3 5 33 34 36 37 38 41 lncom 
 |-  ( ( ( ( ph /\ A e. ( R I B ) ) /\ B e. D ) /\ A =/= B ) -> A e. ( B L R ) )
43 6 ad3antrrr 
 |-  ( ( ( ( ph /\ A e. ( R I B ) ) /\ B e. D ) /\ A =/= B ) -> D e. ran L )
44 simplr 
 |-  ( ( ( ( ph /\ A e. ( R I B ) ) /\ B e. D ) /\ A =/= B ) -> B e. D )
45 12 ad3antrrr 
 |-  ( ( ( ( ph /\ A e. ( R I B ) ) /\ B e. D ) /\ A =/= B ) -> R e. D )
46 1 3 5 33 34 36 38 38 43 44 45 tglinethru 
 |-  ( ( ( ( ph /\ A e. ( R I B ) ) /\ B e. D ) /\ A =/= B ) -> D = ( B L R ) )
47 42 46 eleqtrrd 
 |-  ( ( ( ( ph /\ A e. ( R I B ) ) /\ B e. D ) /\ A =/= B ) -> A e. D )
48 32 47 pm2.61dane 
 |-  ( ( ( ph /\ A e. ( R I B ) ) /\ B e. D ) -> A e. D )
49 1 2 3 4 5 6 7 9 11 13 oppne1 
 |-  ( ph -> -. A e. D )
50 49 ad2antrr 
 |-  ( ( ( ph /\ A e. ( R I B ) ) /\ B e. D ) -> -. A e. D )
51 48 50 pm2.65da 
 |-  ( ( ph /\ A e. ( R I B ) ) -> -. B e. D )
52 20 adantr 
 |-  ( ( ( ph /\ A e. ( R I B ) ) /\ ( S ` B ) e. D ) -> G e. TarskiG )
53 25 adantr 
 |-  ( ( ( ph /\ A e. ( R I B ) ) /\ ( S ` B ) e. D ) -> M e. P )
54 22 adantr 
 |-  ( ( ( ph /\ A e. ( R I B ) ) /\ ( S ` B ) e. D ) -> B e. P )
55 1 2 3 5 23 52 53 8 54 mirmir 
 |-  ( ( ( ph /\ A e. ( R I B ) ) /\ ( S ` B ) e. D ) -> ( S ` ( S ` B ) ) = B )
56 19 adantr 
 |-  ( ( ( ph /\ A e. ( R I B ) ) /\ ( S ` B ) e. D ) -> D e. ran L )
57 27 adantr 
 |-  ( ( ( ph /\ A e. ( R I B ) ) /\ ( S ` B ) e. D ) -> M e. D )
58 simpr 
 |-  ( ( ( ph /\ A e. ( R I B ) ) /\ ( S ` B ) e. D ) -> ( S ` B ) e. D )
59 1 2 3 5 23 52 8 56 57 58 mirln 
 |-  ( ( ( ph /\ A e. ( R I B ) ) /\ ( S ` B ) e. D ) -> ( S ` ( S ` B ) ) e. D )
60 55 59 eqeltrrd 
 |-  ( ( ( ph /\ A e. ( R I B ) ) /\ ( S ` B ) e. D ) -> B e. D )
61 51 60 mtand 
 |-  ( ( ph /\ A e. ( R I B ) ) -> -. ( S ` B ) e. D )
62 1 2 3 5 23 20 25 8 22 mirbtwn 
 |-  ( ( ph /\ A e. ( R I B ) ) -> M e. ( ( S ` B ) I B ) )
63 1 2 3 4 26 22 27 61 51 62 islnoppd 
 |-  ( ( ph /\ A e. ( R I B ) ) -> ( S ` B ) O B )
64 eqidd 
 |-  ( ( ph /\ A e. ( R I B ) ) -> ( S ` B ) = ( S ` B ) )
65 nelne2 
 |-  ( ( ( S ` R ) e. D /\ -. ( S ` B ) e. D ) -> ( S ` R ) =/= ( S ` B ) )
66 29 61 65 syl2anc 
 |-  ( ( ph /\ A e. ( R I B ) ) -> ( S ` R ) =/= ( S ` B ) )
67 66 necomd 
 |-  ( ( ph /\ A e. ( R I B ) ) -> ( S ` B ) =/= ( S ` R ) )
68 1 2 3 4 5 6 7 9 11 13 oppne2 
 |-  ( ph -> -. C e. D )
69 68 adantr 
 |-  ( ( ph /\ A e. ( R I B ) ) -> -. C e. D )
70 nelne2 
 |-  ( ( ( S ` R ) e. D /\ -. C e. D ) -> ( S ` R ) =/= C )
71 29 69 70 syl2anc 
 |-  ( ( ph /\ A e. ( R I B ) ) -> ( S ` R ) =/= C )
72 71 necomd 
 |-  ( ( ph /\ A e. ( R I B ) ) -> C =/= ( S ` R ) )
73 15 eqcomd 
 |-  ( ph -> ( S ` C ) = A )
74 1 2 3 5 23 7 24 8 11 73 mircom 
 |-  ( ph -> ( S ` A ) = C )
75 74 adantr 
 |-  ( ( ph /\ A e. ( R I B ) ) -> ( S ` A ) = C )
76 35 adantr 
 |-  ( ( ph /\ A e. ( R I B ) ) -> R e. P )
77 9 adantr 
 |-  ( ( ph /\ A e. ( R I B ) ) -> A e. P )
78 simpr 
 |-  ( ( ph /\ A e. ( R I B ) ) -> A e. ( R I B ) )
79 1 2 3 5 23 20 25 8 76 77 22 78 mirbtwni 
 |-  ( ( ph /\ A e. ( R I B ) ) -> ( S ` A ) e. ( ( S ` R ) I ( S ` B ) ) )
80 75 79 eqeltrrd 
 |-  ( ( ph /\ A e. ( R I B ) ) -> C e. ( ( S ` R ) I ( S ` B ) ) )
81 1 2 3 4 5 19 20 8 26 21 22 29 63 27 64 67 72 80 opphllem1 
 |-  ( ( ph /\ A e. ( R I B ) ) -> C O B )
82 1 2 3 4 5 19 20 21 22 81 oppcom 
 |-  ( ( ph /\ A e. ( R I B ) ) -> B O C )
83 6 adantr 
 |-  ( ( ph /\ B e. ( R I A ) ) -> D e. ran L )
84 7 adantr 
 |-  ( ( ph /\ B e. ( R I A ) ) -> G e. TarskiG )
85 9 adantr 
 |-  ( ( ph /\ B e. ( R I A ) ) -> A e. P )
86 10 adantr 
 |-  ( ( ph /\ B e. ( R I A ) ) -> B e. P )
87 11 adantr 
 |-  ( ( ph /\ B e. ( R I A ) ) -> C e. P )
88 12 adantr 
 |-  ( ( ph /\ B e. ( R I A ) ) -> R e. D )
89 13 adantr 
 |-  ( ( ph /\ B e. ( R I A ) ) -> A O C )
90 14 adantr 
 |-  ( ( ph /\ B e. ( R I A ) ) -> M e. D )
91 15 adantr 
 |-  ( ( ph /\ B e. ( R I A ) ) -> A = ( S ` C ) )
92 16 adantr 
 |-  ( ( ph /\ B e. ( R I A ) ) -> A =/= R )
93 17 adantr 
 |-  ( ( ph /\ B e. ( R I A ) ) -> B =/= R )
94 simpr 
 |-  ( ( ph /\ B e. ( R I A ) ) -> B e. ( R I A ) )
95 1 2 3 4 5 83 84 8 85 86 87 88 89 90 91 92 93 94 opphllem1 
 |-  ( ( ph /\ B e. ( R I A ) ) -> B O C )
96 82 95 18 mpjaodan 
 |-  ( ph -> B O C )