Metamath Proof Explorer

Theorem tgextahpl

Description: The generic open half-plane core. From a point X between A and D that is on the half-line from C through W , with W off line A C , both X and D and both X and W land on the same side of line A C (two colhp applications), and hpgcom / hpgtr compose them. X =/= C is read off .xk by hlne1 , so no x = C case reaches here. The $d s are on proof dummies only -- colhp 's class abstraction needs its own bound variables -- so nothing propagates to callers. (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses tgextahpl.p 
|- P = ( Base ` G )
tgextahpl.m 
|- .- = ( dist ` G )
tgextahpl.i 
|- I = ( Itv ` G )
tgextahpl.l 
|- L = ( LineG ` G )
tgextahpl.k 
|- K = ( hlG ` G )
tgextahpl.g 
|- ( ph -> G e. TarskiG )
tgextahpl.a 
|- ( ph -> A e. P )
tgextahpl.c 
|- ( ph -> C e. P )
tgextahpl.d 
|- ( ph -> D e. P )
tgextahpl.w 
|- ( ph -> W e. P )
tgextahpl.x 
|- ( ph -> X e. P )
tgextahpl.ncd 
|- ( ph -> -. ( A e. ( C L D ) \/ C = D ) )
tgextahpl.nw 
|- ( ph -> -. W e. ( A L C ) )
tgextahpl.xad 
|- ( ph -> X e. ( A I D ) )
tgextahpl.xk 
|- ( ph -> X ( K ` C ) W )
Assertion tgextahpl 
|- ( ph -> W ( ( hpG ` G ) ` ( A L C ) ) D )

Proof

Step Hyp Ref Expression
1 tgextahpl.p 
 |-  P = ( Base ` G )
2 tgextahpl.m 
 |-  .- = ( dist ` G )
3 tgextahpl.i 
 |-  I = ( Itv ` G )
4 tgextahpl.l 
 |-  L = ( LineG ` G )
5 tgextahpl.k 
 |-  K = ( hlG ` G )
6 tgextahpl.g 
 |-  ( ph -> G e. TarskiG )
7 tgextahpl.a 
 |-  ( ph -> A e. P )
8 tgextahpl.c 
 |-  ( ph -> C e. P )
9 tgextahpl.d 
 |-  ( ph -> D e. P )
10 tgextahpl.w 
 |-  ( ph -> W e. P )
11 tgextahpl.x 
 |-  ( ph -> X e. P )
12 tgextahpl.ncd 
 |-  ( ph -> -. ( A e. ( C L D ) \/ C = D ) )
13 tgextahpl.nw 
 |-  ( ph -> -. W e. ( A L C ) )
14 tgextahpl.xad 
 |-  ( ph -> X e. ( A I D ) )
15 tgextahpl.xk 
 |-  ( ph -> X ( K ` C ) W )
16 1 3 4 6 7 8 9 12 ncolne1 
 |-  ( ph -> A =/= C )
17 1 3 4 6 7 8 16 tgelrnln 
 |-  ( ph -> ( A L C ) e. ran L )
18 simpl 
 |-  ( ( u = a /\ v = b ) -> u = a )
19 18 eleq1d 
 |-  ( ( u = a /\ v = b ) -> ( u e. ( P \ ( A L C ) ) <-> a e. ( P \ ( A L C ) ) ) )
20 simpr 
 |-  ( ( u = a /\ v = b ) -> v = b )
21 20 eleq1d 
 |-  ( ( u = a /\ v = b ) -> ( v e. ( P \ ( A L C ) ) <-> b e. ( P \ ( A L C ) ) ) )
22 19 21 anbi12d 
 |-  ( ( u = a /\ v = b ) -> ( ( u e. ( P \ ( A L C ) ) /\ v e. ( P \ ( A L C ) ) ) <-> ( a e. ( P \ ( A L C ) ) /\ b e. ( P \ ( A L C ) ) ) ) )
23 simpr 
 |-  ( ( ( u = a /\ v = b ) /\ w = t ) -> w = t )
24 simpll 
 |-  ( ( ( u = a /\ v = b ) /\ w = t ) -> u = a )
25 simplr 
 |-  ( ( ( u = a /\ v = b ) /\ w = t ) -> v = b )
26 24 25 oveq12d 
 |-  ( ( ( u = a /\ v = b ) /\ w = t ) -> ( u I v ) = ( a I b ) )
27 23 26 eleq12d 
 |-  ( ( ( u = a /\ v = b ) /\ w = t ) -> ( w e. ( u I v ) <-> t e. ( a I b ) ) )
28 27 cbvrexdva 
 |-  ( ( u = a /\ v = b ) -> ( E. w e. ( A L C ) w e. ( u I v ) <-> E. t e. ( A L C ) t e. ( a I b ) ) )
29 22 28 anbi12d 
 |-  ( ( u = a /\ v = b ) -> ( ( ( u e. ( P \ ( A L C ) ) /\ v e. ( P \ ( A L C ) ) ) /\ E. w e. ( A L C ) w e. ( u I v ) ) <-> ( ( a e. ( P \ ( A L C ) ) /\ b e. ( P \ ( A L C ) ) ) /\ E. t e. ( A L C ) t e. ( a I b ) ) ) )
30 29 cbvopabv 
 |-  { <. u , v >. | ( ( u e. ( P \ ( A L C ) ) /\ v e. ( P \ ( A L C ) ) ) /\ E. w e. ( A L C ) w e. ( u I v ) ) } = { <. a , b >. | ( ( a e. ( P \ ( A L C ) ) /\ b e. ( P \ ( A L C ) ) ) /\ E. t e. ( A L C ) t e. ( a I b ) ) }
31 10 adantr 
 |-  ( ( ph /\ X e. ( A L C ) ) -> W e. P )
32 11 adantr 
 |-  ( ( ph /\ X e. ( A L C ) ) -> X e. P )
33 8 adantr 
 |-  ( ( ph /\ X e. ( A L C ) ) -> C e. P )
34 6 adantr 
 |-  ( ( ph /\ X e. ( A L C ) ) -> G e. TarskiG )
35 15 adantr 
 |-  ( ( ph /\ X e. ( A L C ) ) -> X ( K ` C ) W )
36 1 3 5 32 31 33 34 35 hlcomd 
 |-  ( ( ph /\ X e. ( A L C ) ) -> W ( K ` C ) X )
37 1 3 5 31 32 33 34 4 36 hlln 
 |-  ( ( ph /\ X e. ( A L C ) ) -> W e. ( X L C ) )
38 7 adantr 
 |-  ( ( ph /\ X e. ( A L C ) ) -> A e. P )
39 16 adantr 
 |-  ( ( ph /\ X e. ( A L C ) ) -> A =/= C )
40 1 3 4 34 38 33 39 tglinecom 
 |-  ( ( ph /\ X e. ( A L C ) ) -> ( A L C ) = ( C L A ) )
41 16 necomd 
 |-  ( ph -> C =/= A )
42 41 adantr 
 |-  ( ( ph /\ X e. ( A L C ) ) -> C =/= A )
43 1 3 5 11 10 8 6 15 hlne1 
 |-  ( ph -> X =/= C )
44 43 adantr 
 |-  ( ( ph /\ X e. ( A L C ) ) -> X =/= C )
45 simpr 
 |-  ( ( ph /\ X e. ( A L C ) ) -> X e. ( A L C ) )
46 45 40 eleqtrd 
 |-  ( ( ph /\ X e. ( A L C ) ) -> X e. ( C L A ) )
47 1 3 4 34 33 38 42 32 44 46 tglineelsb2 
 |-  ( ( ph /\ X e. ( A L C ) ) -> ( C L A ) = ( C L X ) )
48 43 necomd 
 |-  ( ph -> C =/= X )
49 48 adantr 
 |-  ( ( ph /\ X e. ( A L C ) ) -> C =/= X )
50 1 3 4 34 33 32 49 tglinecom 
 |-  ( ( ph /\ X e. ( A L C ) ) -> ( C L X ) = ( X L C ) )
51 47 50 eqtrd 
 |-  ( ( ph /\ X e. ( A L C ) ) -> ( C L A ) = ( X L C ) )
52 40 51 eqtrd 
 |-  ( ( ph /\ X e. ( A L C ) ) -> ( A L C ) = ( X L C ) )
53 37 52 eleqtrrd 
 |-  ( ( ph /\ X e. ( A L C ) ) -> W e. ( A L C ) )
54 13 53 mtand 
 |-  ( ph -> -. X e. ( A L C ) )
55 15 54 jca 
 |-  ( ph -> ( X ( K ` C ) W /\ -. X e. ( A L C ) ) )
56 1 3 4 6 7 8 16 tglinerflx2 
 |-  ( ph -> C e. ( A L C ) )
57 6 adantr 
 |-  ( ( ph /\ X e. ( C I W ) ) -> G e. TarskiG )
58 11 adantr 
 |-  ( ( ph /\ X e. ( C I W ) ) -> X e. P )
59 10 adantr 
 |-  ( ( ph /\ X e. ( C I W ) ) -> W e. P )
60 8 adantr 
 |-  ( ( ph /\ X e. ( C I W ) ) -> C e. P )
61 simpr 
 |-  ( ( ph /\ X e. ( C I W ) ) -> X e. ( C I W ) )
62 1 4 3 57 58 59 60 61 btwncolg2 
 |-  ( ( ph /\ X e. ( C I W ) ) -> ( C e. ( X L W ) \/ X = W ) )
63 6 adantr 
 |-  ( ( ph /\ W e. ( C I X ) ) -> G e. TarskiG )
64 11 adantr 
 |-  ( ( ph /\ W e. ( C I X ) ) -> X e. P )
65 10 adantr 
 |-  ( ( ph /\ W e. ( C I X ) ) -> W e. P )
66 8 adantr 
 |-  ( ( ph /\ W e. ( C I X ) ) -> C e. P )
67 simpr 
 |-  ( ( ph /\ W e. ( C I X ) ) -> W e. ( C I X ) )
68 1 2 3 63 66 65 64 67 tgbtwncom 
 |-  ( ( ph /\ W e. ( C I X ) ) -> W e. ( X I C ) )
69 1 4 3 63 64 65 66 68 btwncolg3 
 |-  ( ( ph /\ W e. ( C I X ) ) -> ( C e. ( X L W ) \/ X = W ) )
70 1 3 5 11 10 8 6 ishlg 
 |-  ( ph -> ( X ( K ` C ) W <-> ( X =/= C /\ W =/= C /\ ( X e. ( C I W ) \/ W e. ( C I X ) ) ) ) )
71 15 70 mpbid 
 |-  ( ph -> ( X =/= C /\ W =/= C /\ ( X e. ( C I W ) \/ W e. ( C I X ) ) ) )
72 71 simp3d 
 |-  ( ph -> ( X e. ( C I W ) \/ W e. ( C I X ) ) )
73 62 69 72 mpjaodan 
 |-  ( ph -> ( C e. ( X L W ) \/ X = W ) )
74 1 3 4 6 17 11 30 10 56 73 5 colhp 
 |-  ( ph -> ( X ( ( hpG ` G ) ` ( A L C ) ) W <-> ( X ( K ` C ) W /\ -. X e. ( A L C ) ) ) )
75 55 74 mpbird 
 |-  ( ph -> X ( ( hpG ` G ) ` ( A L C ) ) W )
76 1 3 4 6 17 11 30 10 75 hpgcom 
 |-  ( ph -> W ( ( hpG ` G ) ` ( A L C ) ) X )
77 1 3 4 6 7 8 9 12 ncolne2 
 |-  ( ph -> A =/= D )
78 1 3 4 6 7 8 16 tglinerflx1 
 |-  ( ph -> A e. ( A L C ) )
79 nelne2 
 |-  ( ( A e. ( A L C ) /\ -. X e. ( A L C ) ) -> A =/= X )
80 78 54 79 syl2anc 
 |-  ( ph -> A =/= X )
81 80 necomd 
 |-  ( ph -> X =/= A )
82 1 3 5 7 9 11 6 8 14 77 81 btwnhl1 
 |-  ( ph -> X ( K ` A ) D )
83 82 54 jca 
 |-  ( ph -> ( X ( K ` A ) D /\ -. X e. ( A L C ) ) )
84 1 4 3 6 11 9 7 14 btwncolg2 
 |-  ( ph -> ( A e. ( X L D ) \/ X = D ) )
85 1 3 4 6 17 11 30 9 78 84 5 colhp 
 |-  ( ph -> ( X ( ( hpG ` G ) ` ( A L C ) ) D <-> ( X ( K ` A ) D /\ -. X e. ( A L C ) ) ) )
86 83 85 mpbird 
 |-  ( ph -> X ( ( hpG ` G ) ` ( A L C ) ) D )
87 1 3 4 6 17 10 30 11 76 9 86 hpgtr 
 |-  ( ph -> W ( ( hpG ` G ) ` ( A L C ) ) D )