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	$⊢ \underset{˙}{-} = dist (G)$
	tgextahpl.i	$⊢ I = Itv (G)$
	tgextahpl.l	$⊢ L = {Line}_{𝒢} (G)$
	tgextahpl.k	$⊢ K = {hl}_{𝒢} (G)$
	tgextahpl.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgextahpl.a	$⊢ φ \to A \in P$
	tgextahpl.c	$⊢ φ \to C \in P$
	tgextahpl.d	$⊢ φ \to D \in P$
	tgextahpl.w	$⊢ φ \to W \in P$
	tgextahpl.x	$⊢ φ \to X \in P$
	tgextahpl.ncd	$⊢ φ \to \neg (A \in (C L D) \lor C = D)$
	tgextahpl.nw	$⊢ φ \to \neg W \in (A L C)$
	tgextahpl.xad	$⊢ φ \to X \in (A I D)$
	tgextahpl.xk	$⊢ φ \to X K (C) W$
Assertion	tgextahpl	$⊢ φ \to W {hp}_{𝒢} (G) (A L C) D$

Proof

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

Metamath Proof Explorer

Theorem tgextahpl

Proof