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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgextahpl.m ⊢ − = ( dist ‘ 𝐺 )
tgextahpl.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgextahpl.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tgextahpl.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
tgextahpl.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgextahpl.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
tgextahpl.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
tgextahpl.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
tgextahpl.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
tgextahpl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
tgextahpl.ncd ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )
tgextahpl.nw ⊢ ( 𝜑 → ¬ 𝑊 ∈ ( 𝐴 𝐿 𝐶 ) )
tgextahpl.xad ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 𝐼 𝐷 ) )
tgextahpl.xk ⊢ ( 𝜑 → 𝑋 ( 𝐾 ‘ 𝐶 ) 𝑊 )
Assertion tgextahpl ( 𝜑 → 𝑊 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐴 𝐿 𝐶 ) ) 𝐷 )

Proof

Step Hyp Ref Expression
1 tgextahpl.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgextahpl.m ⊢ − = ( dist ‘ 𝐺 )
3 tgextahpl.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tgextahpl.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 tgextahpl.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
6 tgextahpl.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7 tgextahpl.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8 tgextahpl.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9 tgextahpl.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
10 tgextahpl.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
11 tgextahpl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
12 tgextahpl.ncd ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )
13 tgextahpl.nw ⊢ ( 𝜑 → ¬ 𝑊 ∈ ( 𝐴 𝐿 𝐶 ) )
14 tgextahpl.xad ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 𝐼 𝐷 ) )
15 tgextahpl.xk ⊢ ( 𝜑 → 𝑋 ( 𝐾 ‘ 𝐶 ) 𝑊 )
16 1 3 4 6 7 8 9 12 ncolne1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
17 1 3 4 6 7 8 16 tgelrnln ⊢ ( 𝜑 → ( 𝐴 𝐿 𝐶 ) ∈ ran 𝐿 )
18 simpl ⊢ ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) → 𝑢 = 𝑎 )
19 18 eleq1d ⊢ ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) → ( 𝑢 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ↔ 𝑎 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ) )
20 simpr ⊢ ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) → 𝑣 = 𝑏 )
21 20 eleq1d ⊢ ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) → ( 𝑣 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ↔ 𝑏 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ) )
22 19 21 anbi12d ⊢ ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) → ( ( 𝑢 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ∧ 𝑣 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ) ↔ ( 𝑎 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ) ) )
23 simpr ⊢ ( ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) ∧ 𝑤 = 𝑡 ) → 𝑤 = 𝑡 )
24 simpll ⊢ ( ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) ∧ 𝑤 = 𝑡 ) → 𝑢 = 𝑎 )
25 simplr ⊢ ( ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) ∧ 𝑤 = 𝑡 ) → 𝑣 = 𝑏 )
26 24 25 oveq12d ⊢ ( ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) ∧ 𝑤 = 𝑡 ) → ( 𝑢 𝐼 𝑣 ) = ( 𝑎 𝐼 𝑏 ) )
27 23 26 eleq12d ⊢ ( ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) ∧ 𝑤 = 𝑡 ) → ( 𝑤 ∈ ( 𝑢 𝐼 𝑣 ) ↔ 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) )
28 27 cbvrexdva ⊢ ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) → ( ∃ 𝑤 ∈ ( 𝐴 𝐿 𝐶 ) 𝑤 ∈ ( 𝑢 𝐼 𝑣 ) ↔ ∃ 𝑡 ∈ ( 𝐴 𝐿 𝐶 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) )
29 22 28 anbi12d ⊢ ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) → ( ( ( 𝑢 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ∧ 𝑣 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ) ∧ ∃ 𝑤 ∈ ( 𝐴 𝐿 𝐶 ) 𝑤 ∈ ( 𝑢 𝐼 𝑣 ) ) ↔ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝐴 𝐿 𝐶 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) ) )
30 29 cbvopabv ⊢ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ∧ 𝑣 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ) ∧ ∃ 𝑤 ∈ ( 𝐴 𝐿 𝐶 ) 𝑤 ∈ ( 𝑢 𝐼 𝑣 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝐴 𝐿 𝐶 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
31 10 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝑊 ∈ 𝑃 )
32 11 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝑋 ∈ 𝑃 )
33 8 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝐶 ∈ 𝑃 )
34 6 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝐺 ∈ TarskiG )
35 15 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝑋 ( 𝐾 ‘ 𝐶 ) 𝑊 )
36 1 3 5 32 31 33 34 35 hlcomd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝑊 ( 𝐾 ‘ 𝐶 ) 𝑋 )
37 1 3 5 31 32 33 34 4 36 hlln ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝑊 ∈ ( 𝑋 𝐿 𝐶 ) )
38 7 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝐴 ∈ 𝑃 )
39 16 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝐴 ≠ 𝐶 )
40 1 3 4 34 38 33 39 tglinecom ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) → ( 𝐴 𝐿 𝐶 ) = ( 𝐶 𝐿 𝐴 ) )
41 16 necomd ⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝐶 ≠ 𝐴 )
43 1 3 5 11 10 8 6 15 hlne1 ⊢ ( 𝜑 → 𝑋 ≠ 𝐶 )
44 43 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝑋 ≠ 𝐶 )
45 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) )
46 45 40 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝑋 ∈ ( 𝐶 𝐿 𝐴 ) )
47 1 3 4 34 33 38 42 32 44 46 tglineelsb2 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) → ( 𝐶 𝐿 𝐴 ) = ( 𝐶 𝐿 𝑋 ) )
48 43 necomd ⊢ ( 𝜑 → 𝐶 ≠ 𝑋 )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝐶 ≠ 𝑋 )
50 1 3 4 34 33 32 49 tglinecom ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) → ( 𝐶 𝐿 𝑋 ) = ( 𝑋 𝐿 𝐶 ) )
51 47 50 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) → ( 𝐶 𝐿 𝐴 ) = ( 𝑋 𝐿 𝐶 ) )
52 40 51 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) → ( 𝐴 𝐿 𝐶 ) = ( 𝑋 𝐿 𝐶 ) )
53 37 52 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝑊 ∈ ( 𝐴 𝐿 𝐶 ) )
54 13 53 mtand ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) )
55 15 54 jca ⊢ ( 𝜑 → ( 𝑋 ( 𝐾 ‘ 𝐶 ) 𝑊 ∧ ¬ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) )
56 1 3 4 6 7 8 16 tglinerflx2 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐿 𝐶 ) )
57 6 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐶 𝐼 𝑊 ) ) → 𝐺 ∈ TarskiG )
58 11 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐶 𝐼 𝑊 ) ) → 𝑋 ∈ 𝑃 )
59 10 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐶 𝐼 𝑊 ) ) → 𝑊 ∈ 𝑃 )
60 8 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐶 𝐼 𝑊 ) ) → 𝐶 ∈ 𝑃 )
61 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐶 𝐼 𝑊 ) ) → 𝑋 ∈ ( 𝐶 𝐼 𝑊 ) )
62 1 4 3 57 58 59 60 61 btwncolg2 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐶 𝐼 𝑊 ) ) → ( 𝐶 ∈ ( 𝑋 𝐿 𝑊 ) ∨ 𝑋 = 𝑊 ) )
63 6 adantr ⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝐶 𝐼 𝑋 ) ) → 𝐺 ∈ TarskiG )
64 11 adantr ⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝐶 𝐼 𝑋 ) ) → 𝑋 ∈ 𝑃 )
65 10 adantr ⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝐶 𝐼 𝑋 ) ) → 𝑊 ∈ 𝑃 )
66 8 adantr ⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝐶 𝐼 𝑋 ) ) → 𝐶 ∈ 𝑃 )
67 simpr ⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝐶 𝐼 𝑋 ) ) → 𝑊 ∈ ( 𝐶 𝐼 𝑋 ) )
68 1 2 3 63 66 65 64 67 tgbtwncom ⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝐶 𝐼 𝑋 ) ) → 𝑊 ∈ ( 𝑋 𝐼 𝐶 ) )
69 1 4 3 63 64 65 66 68 btwncolg3 ⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝐶 𝐼 𝑋 ) ) → ( 𝐶 ∈ ( 𝑋 𝐿 𝑊 ) ∨ 𝑋 = 𝑊 ) )
70 1 3 5 11 10 8 6 ishlg ⊢ ( 𝜑 → ( 𝑋 ( 𝐾 ‘ 𝐶 ) 𝑊 ↔ ( 𝑋 ≠ 𝐶 ∧ 𝑊 ≠ 𝐶 ∧ ( 𝑋 ∈ ( 𝐶 𝐼 𝑊 ) ∨ 𝑊 ∈ ( 𝐶 𝐼 𝑋 ) ) ) ) )
71 15 70 mpbid ⊢ ( 𝜑 → ( 𝑋 ≠ 𝐶 ∧ 𝑊 ≠ 𝐶 ∧ ( 𝑋 ∈ ( 𝐶 𝐼 𝑊 ) ∨ 𝑊 ∈ ( 𝐶 𝐼 𝑋 ) ) ) )
72 71 simp3d ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐶 𝐼 𝑊 ) ∨ 𝑊 ∈ ( 𝐶 𝐼 𝑋 ) ) )
73 62 69 72 mpjaodan ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝑋 𝐿 𝑊 ) ∨ 𝑋 = 𝑊 ) )
74 1 3 4 6 17 11 30 10 56 73 5 colhp ⊢ ( 𝜑 → ( 𝑋 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐴 𝐿 𝐶 ) ) 𝑊 ↔ ( 𝑋 ( 𝐾 ‘ 𝐶 ) 𝑊 ∧ ¬ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) ) )
75 55 74 mpbird ⊢ ( 𝜑 → 𝑋 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐴 𝐿 𝐶 ) ) 𝑊 )
76 1 3 4 6 17 11 30 10 75 hpgcom ⊢ ( 𝜑 → 𝑊 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐴 𝐿 𝐶 ) ) 𝑋 )
77 1 3 4 6 7 8 9 12 ncolne2 ⊢ ( 𝜑 → 𝐴 ≠ 𝐷 )
78 1 3 4 6 7 8 16 tglinerflx1 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 𝐿 𝐶 ) )
79 nelne2 ⊢ ( ( 𝐴 ∈ ( 𝐴 𝐿 𝐶 ) ∧ ¬ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝐴 ≠ 𝑋 )
80 78 54 79 syl2anc ⊢ ( 𝜑 → 𝐴 ≠ 𝑋 )
81 80 necomd ⊢ ( 𝜑 → 𝑋 ≠ 𝐴 )
82 1 3 5 7 9 11 6 8 14 77 81 btwnhl1 ⊢ ( 𝜑 → 𝑋 ( 𝐾 ‘ 𝐴 ) 𝐷 )
83 82 54 jca ⊢ ( 𝜑 → ( 𝑋 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ¬ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) )
84 1 4 3 6 11 9 7 14 btwncolg2 ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝑋 𝐿 𝐷 ) ∨ 𝑋 = 𝐷 ) )
85 1 3 4 6 17 11 30 9 78 84 5 colhp ⊢ ( 𝜑 → ( 𝑋 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐴 𝐿 𝐶 ) ) 𝐷 ↔ ( 𝑋 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ¬ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) ) )
86 83 85 mpbird ⊢ ( 𝜑 → 𝑋 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐴 𝐿 𝐶 ) ) 𝐷 )
87 1 3 4 6 17 10 30 11 76 9 86 hpgtr ⊢ ( 𝜑 → 𝑊 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐴 𝐿 𝐶 ) ) 𝐷 )