colhp

Description: Half-plane relation for colinear points. Theorem 9.19 of Schwabhauser p. 73. (Contributed by Thierry Arnoux, 3-Aug-2020)

	Ref	Expression
Hypotheses	hpgid.p	$⊢ P = {Base}_{G}$
	hpgid.i	$⊢ I = Itv (G)$
	hpgid.l	$⊢ L = {Line}_{𝒢} (G)$
	hpgid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	hpgid.d	$⊢ φ \to D \in ran L$
	hpgid.a	$⊢ φ \to A \in P$
	hpgid.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
	colopp.b	$⊢ φ \to B \in P$
	colopp.p	$⊢ φ \to C \in D$
	colopp.1	$⊢ φ \to (C \in (A L B) \lor A = B)$
	colhp.k	$⊢ K = {hl}_{𝒢} (G)$
Assertion	colhp	$⊢ φ \to (A {hp}_{𝒢} (G) (D) B \leftrightarrow (A K (C) B \land \neg A \in D))$

Proof

Step	Hyp	Ref	Expression
1		hpgid.p	$⊢ P = {Base}_{G}$
2		hpgid.i	$⊢ I = Itv (G)$
3		hpgid.l	$⊢ L = {Line}_{𝒢} (G)$
4		hpgid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		hpgid.d	$⊢ φ \to D \in ran L$
6		hpgid.a	$⊢ φ \to A \in P$
7		hpgid.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
8		colopp.b	$⊢ φ \to B \in P$
9		colopp.p	$⊢ φ \to C \in D$
10		colopp.1	$⊢ φ \to (C \in (A L B) \lor A = B)$
11		colhp.k	$⊢ K = {hl}_{𝒢} (G)$
12		ancom	$⊢ (A K (C) B \land \neg A \in D) \leftrightarrow (\neg A \in D \land A K (C) B)$
13	12	a1i	$⊢ φ \to ((A K (C) B \land \neg A \in D) \leftrightarrow (\neg A \in D \land A K (C) B))$
14	4	adantr	$⊢ (φ \land \neg A \in D) \to G \in 𝒢_{Tarski}$
15	5	adantr	$⊢ (φ \land \neg A \in D) \to D \in ran L$
16	8	adantr	$⊢ (φ \land \neg A \in D) \to B \in P$
17		eqid	$⊢ dist (G) = dist (G)$
18		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
19	1 3 2 4 5 9	tglnpt	$⊢ φ \to C \in P$
20		eqid	$⊢ {pInv}_{𝒢} (G) (C) = {pInv}_{𝒢} (G) (C)$
21	1 17 2 3 18 4 19 20 6	mircl	$⊢ φ \to {pInv}_{𝒢} (G) (C) (A) \in P$
22	21	adantr	$⊢ (φ \land \neg A \in D) \to {pInv}_{𝒢} (G) (C) (A) \in P$
23	9	adantr	$⊢ (φ \land \neg A \in D) \to C \in D$
24	19	adantr	$⊢ (φ \land \neg A \in D) \to C \in P$
25	6	adantr	$⊢ (φ \land \neg A \in D) \to A \in P$
26		nelne2	$⊢ (C \in D \land \neg A \in D) \to C \neq A$
27	9 26	sylan	$⊢ (φ \land \neg A \in D) \to C \neq A$
28	27	necomd	$⊢ (φ \land \neg A \in D) \to A \neq C$
29	1 17 2 3 18 4 19 20 6	mirbtwn	$⊢ φ \to C \in ({pInv}_{𝒢} (G) (C) (A) I A)$
30	1 17 2 4 21 19 6 29	tgbtwncom	$⊢ φ \to C \in (A I {pInv}_{𝒢} (G) (C) (A))$
31	30	adantr	$⊢ (φ \land \neg A \in D) \to C \in (A I {pInv}_{𝒢} (G) (C) (A))$
32	1 2 3 14 25 24 22 28 31	btwnlng3	$⊢ (φ \land \neg A \in D) \to {pInv}_{𝒢} (G) (C) (A) \in (A L C)$
33	1 3 2 4 6 8 19 10	colrot1	$⊢ φ \to (A \in (B L C) \lor B = C)$
34	1 3 2 4 8 19 6 33	colcom	$⊢ φ \to (A \in (C L B) \lor C = B)$
35	34	adantr	$⊢ (φ \land \neg A \in D) \to (A \in (C L B) \lor C = B)$
36	1 2 3 14 22 25 24 16 32 35	coltr	$⊢ (φ \land \neg A \in D) \to ({pInv}_{𝒢} (G) (C) (A) \in (C L B) \lor C = B)$
37	1 3 2 14 24 16 22 36	colrot1	$⊢ (φ \land \neg A \in D) \to (C \in (B L {pInv}_{𝒢} (G) (C) (A)) \lor B = {pInv}_{𝒢} (G) (C) (A))$
38	1 2 3 14 15 16 7 22 23 37	colopp	$⊢ (φ \land \neg A \in D) \to (B O {pInv}_{𝒢} (G) (C) (A) \leftrightarrow (C \in (B I {pInv}_{𝒢} (G) (C) (A)) \land \neg B \in D \land \neg {pInv}_{𝒢} (G) (C) (A) \in D))$
39		simpr	$⊢ (φ \land \neg A \in D) \to \neg A \in D$
40	1 17 2 3 18 4 19 20 6	mirmir	$⊢ φ \to {pInv}_{𝒢} (G) (C) ({pInv}_{𝒢} (G) (C) (A)) = A$
41	40	adantr	$⊢ (φ \land {pInv}_{𝒢} (G) (C) (A) \in D) \to {pInv}_{𝒢} (G) (C) ({pInv}_{𝒢} (G) (C) (A)) = A$
42	4	adantr	$⊢ (φ \land {pInv}_{𝒢} (G) (C) (A) \in D) \to G \in 𝒢_{Tarski}$
43	5	adantr	$⊢ (φ \land {pInv}_{𝒢} (G) (C) (A) \in D) \to D \in ran L$
44	9	adantr	$⊢ (φ \land {pInv}_{𝒢} (G) (C) (A) \in D) \to C \in D$
45		simpr	$⊢ (φ \land {pInv}_{𝒢} (G) (C) (A) \in D) \to {pInv}_{𝒢} (G) (C) (A) \in D$
46	1 17 2 3 18 42 20 43 44 45	mirln	$⊢ (φ \land {pInv}_{𝒢} (G) (C) (A) \in D) \to {pInv}_{𝒢} (G) (C) ({pInv}_{𝒢} (G) (C) (A)) \in D$
47	41 46	eqeltrrd	$⊢ (φ \land {pInv}_{𝒢} (G) (C) (A) \in D) \to A \in D$
48	47	stoic1a	$⊢ (φ \land \neg A \in D) \to \neg {pInv}_{𝒢} (G) (C) (A) \in D$
49		simpr	$⊢ (φ \land t = C) \to t = C$
50	49	eleq1d	$⊢ (φ \land t = C) \to (t \in (A I {pInv}_{𝒢} (G) (C) (A)) \leftrightarrow C \in (A I {pInv}_{𝒢} (G) (C) (A)))$
51	9 50 30	rspcedvd	$⊢ φ \to \exists t \in D t \in (A I {pInv}_{𝒢} (G) (C) (A))$
52	51	adantr	$⊢ (φ \land \neg A \in D) \to \exists t \in D t \in (A I {pInv}_{𝒢} (G) (C) (A))$
53	39 48 52	jca31	$⊢ (φ \land \neg A \in D) \to ((\neg A \in D \land \neg {pInv}_{𝒢} (G) (C) (A) \in D) \land \exists t \in D t \in (A I {pInv}_{𝒢} (G) (C) (A)))$
54	1 17 2 7 25 22	islnopp	$⊢ (φ \land \neg A \in D) \to (A O {pInv}_{𝒢} (G) (C) (A) \leftrightarrow ((\neg A \in D \land \neg {pInv}_{𝒢} (G) (C) (A) \in D) \land \exists t \in D t \in (A I {pInv}_{𝒢} (G) (C) (A))))$
55	53 54	mpbird	$⊢ (φ \land \neg A \in D) \to A O {pInv}_{𝒢} (G) (C) (A)$
56	1 2 3 7 14 15 25 16 22 55	lnopp2hpgb	$⊢ (φ \land \neg A \in D) \to (B O {pInv}_{𝒢} (G) (C) (A) \leftrightarrow A {hp}_{𝒢} (G) (D) B)$
57	8	ad2antrr	$⊢ ((φ \land \neg A \in D) \land (C \in (B I {pInv}_{𝒢} (G) (C) (A)) \land \neg B \in D)) \to B \in P$
58	6	ad2antrr	$⊢ ((φ \land \neg A \in D) \land (C \in (B I {pInv}_{𝒢} (G) (C) (A)) \land \neg B \in D)) \to A \in P$
59	19	ad2antrr	$⊢ ((φ \land \neg A \in D) \land (C \in (B I {pInv}_{𝒢} (G) (C) (A)) \land \neg B \in D)) \to C \in P$
60	4	ad2antrr	$⊢ ((φ \land \neg A \in D) \land (C \in (B I {pInv}_{𝒢} (G) (C) (A)) \land \neg B \in D)) \to G \in 𝒢_{Tarski}$
61	9	ad2antrr	$⊢ ((φ \land \neg A \in D) \land (C \in (B I {pInv}_{𝒢} (G) (C) (A)) \land \neg B \in D)) \to C \in D$
62		simprr	$⊢ ((φ \land \neg A \in D) \land (C \in (B I {pInv}_{𝒢} (G) (C) (A)) \land \neg B \in D)) \to \neg B \in D$
63		nelne2	$⊢ (C \in D \land \neg B \in D) \to C \neq B$
64	63	necomd	$⊢ (C \in D \land \neg B \in D) \to B \neq C$
65	61 62 64	syl2anc	$⊢ ((φ \land \neg A \in D) \land (C \in (B I {pInv}_{𝒢} (G) (C) (A)) \land \neg B \in D)) \to B \neq C$
66	28	adantr	$⊢ ((φ \land \neg A \in D) \land (C \in (B I {pInv}_{𝒢} (G) (C) (A)) \land \neg B \in D)) \to A \neq C$
67		simprl	$⊢ ((φ \land \neg A \in D) \land (C \in (B I {pInv}_{𝒢} (G) (C) (A)) \land \neg B \in D)) \to C \in (B I {pInv}_{𝒢} (G) (C) (A))$
68	1 17 2 3 18 60 20 11 59 57 58 58 65 66 67	mirhl2	$⊢ ((φ \land \neg A \in D) \land (C \in (B I {pInv}_{𝒢} (G) (C) (A)) \land \neg B \in D)) \to B K (C) A$
69	1 2 11 57 58 59 60 68	hlcomd	$⊢ ((φ \land \neg A \in D) \land (C \in (B I {pInv}_{𝒢} (G) (C) (A)) \land \neg B \in D)) \to A K (C) B$
70	69	3adantr3	$⊢ ((φ \land \neg A \in D) \land (C \in (B I {pInv}_{𝒢} (G) (C) (A)) \land \neg B \in D \land \neg {pInv}_{𝒢} (G) (C) (A) \in D)) \to A K (C) B$
71	6	ad2antrr	$⊢ ((φ \land \neg A \in D) \land A K (C) B) \to A \in P$
72	8	ad2antrr	$⊢ ((φ \land \neg A \in D) \land A K (C) B) \to B \in P$
73	21	ad2antrr	$⊢ ((φ \land \neg A \in D) \land A K (C) B) \to {pInv}_{𝒢} (G) (C) (A) \in P$
74	4	ad2antrr	$⊢ ((φ \land \neg A \in D) \land A K (C) B) \to G \in 𝒢_{Tarski}$
75	19	ad2antrr	$⊢ ((φ \land \neg A \in D) \land A K (C) B) \to C \in P$
76		simpr	$⊢ ((φ \land \neg A \in D) \land A K (C) B) \to A K (C) B$
77	30	ad2antrr	$⊢ ((φ \land \neg A \in D) \land A K (C) B) \to C \in (A I {pInv}_{𝒢} (G) (C) (A))$
78	1 2 11 71 72 73 74 75 76 77	btwnhl	$⊢ ((φ \land \neg A \in D) \land A K (C) B) \to C \in (B I {pInv}_{𝒢} (G) (C) (A))$
79	1 2 11 71 72 75 74 3 76	hlln	$⊢ ((φ \land \neg A \in D) \land A K (C) B) \to A \in (B L C)$
80	79	adantr	$⊢ (((φ \land \neg A \in D) \land A K (C) B) \land B \in D) \to A \in (B L C)$
81	14	ad2antrr	$⊢ (((φ \land \neg A \in D) \land A K (C) B) \land B \in D) \to G \in 𝒢_{Tarski}$
82	16	ad2antrr	$⊢ (((φ \land \neg A \in D) \land A K (C) B) \land B \in D) \to B \in P$
83	75	adantr	$⊢ (((φ \land \neg A \in D) \land A K (C) B) \land B \in D) \to C \in P$
84	25	ad2antrr	$⊢ (((φ \land \neg A \in D) \land A K (C) B) \land B \in D) \to A \in P$
85	76	adantr	$⊢ (((φ \land \neg A \in D) \land A K (C) B) \land B \in D) \to A K (C) B$
86	1 2 11 84 82 83 81 85	hlne2	$⊢ (((φ \land \neg A \in D) \land A K (C) B) \land B \in D) \to B \neq C$
87	15	ad2antrr	$⊢ (((φ \land \neg A \in D) \land A K (C) B) \land B \in D) \to D \in ran L$
88		simpr	$⊢ (((φ \land \neg A \in D) \land A K (C) B) \land B \in D) \to B \in D$
89	9	ad3antrrr	$⊢ (((φ \land \neg A \in D) \land A K (C) B) \land B \in D) \to C \in D$
90	1 2 3 81 82 83 86 86 87 88 89	tglinethru	$⊢ (((φ \land \neg A \in D) \land A K (C) B) \land B \in D) \to D = B L C$
91	80 90	eleqtrrd	$⊢ (((φ \land \neg A \in D) \land A K (C) B) \land B \in D) \to A \in D$
92	39	ad2antrr	$⊢ (((φ \land \neg A \in D) \land A K (C) B) \land B \in D) \to \neg A \in D$
93	91 92	pm2.65da	$⊢ ((φ \land \neg A \in D) \land A K (C) B) \to \neg B \in D$
94	48	adantr	$⊢ ((φ \land \neg A \in D) \land A K (C) B) \to \neg {pInv}_{𝒢} (G) (C) (A) \in D$
95	78 93 94	3jca	$⊢ ((φ \land \neg A \in D) \land A K (C) B) \to (C \in (B I {pInv}_{𝒢} (G) (C) (A)) \land \neg B \in D \land \neg {pInv}_{𝒢} (G) (C) (A) \in D)$
96	70 95	impbida	$⊢ (φ \land \neg A \in D) \to ((C \in (B I {pInv}_{𝒢} (G) (C) (A)) \land \neg B \in D \land \neg {pInv}_{𝒢} (G) (C) (A) \in D) \leftrightarrow A K (C) B)$
97	38 56 96	3bitr3d	$⊢ (φ \land \neg A \in D) \to (A {hp}_{𝒢} (G) (D) B \leftrightarrow A K (C) B)$
98	97	pm5.32da	$⊢ φ \to ((\neg A \in D \land A {hp}_{𝒢} (G) (D) B) \leftrightarrow (\neg A \in D \land A K (C) B))$
99		simprr	$⊢ (φ \land (\neg A \in D \land A {hp}_{𝒢} (G) (D) B)) \to A {hp}_{𝒢} (G) (D) B$
100	4	adantr	$⊢ (φ \land A {hp}_{𝒢} (G) (D) B) \to G \in 𝒢_{Tarski}$
101	5	adantr	$⊢ (φ \land A {hp}_{𝒢} (G) (D) B) \to D \in ran L$
102	6	adantr	$⊢ (φ \land A {hp}_{𝒢} (G) (D) B) \to A \in P$
103	8	adantr	$⊢ (φ \land A {hp}_{𝒢} (G) (D) B) \to B \in P$
104		simpr	$⊢ (φ \land A {hp}_{𝒢} (G) (D) B) \to A {hp}_{𝒢} (G) (D) B$
105	1 2 3 7 100 101 102 103 104	hpgne1	$⊢ (φ \land A {hp}_{𝒢} (G) (D) B) \to \neg A \in D$
106	105 104	jca	$⊢ (φ \land A {hp}_{𝒢} (G) (D) B) \to (\neg A \in D \land A {hp}_{𝒢} (G) (D) B)$
107	99 106	impbida	$⊢ φ \to ((\neg A \in D \land A {hp}_{𝒢} (G) (D) B) \leftrightarrow A {hp}_{𝒢} (G) (D) B)$
108	13 98 107	3bitr2rd	$⊢ φ \to (A {hp}_{𝒢} (G) (D) B \leftrightarrow (A K (C) B \land \neg A \in D))$

Metamath Proof Explorer

Theorem colhp

Proof