colopp

Description: Opposite sides of a line for colinear points. Theorem 9.18 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)$
Assertion	colopp	$⊢ φ \to (A O B \leftrightarrow (C \in (A I B) \land \neg A \in D \land \neg B \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	4	ad3antrrr	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to G \in 𝒢_{Tarski}$
12	6	ad3antrrr	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to A \in P$
13	8	ad3antrrr	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to B \in P$
14		eqid	$⊢ dist (G) = dist (G)$
15	5	ad3antrrr	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to D \in ran L$
16		simpllr	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to (\neg A \in D \land \neg B \in D)$
17		simplr	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to y \in D$
18		eleq1w	$⊢ t = y \to (t \in (A I B) \leftrightarrow y \in (A I B))$
19	18	adantl	$⊢ ((((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \land t = y) \to (t \in (A I B) \leftrightarrow y \in (A I B))$
20		simpr	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to y \in (A I B)$
21	17 19 20	rspcedvd	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to \exists t \in D t \in (A I B)$
22	1 14 2 7 6 8	islnopp	$⊢ φ \to (A O B \leftrightarrow ((\neg A \in D \land \neg B \in D) \land \exists t \in D t \in (A I B)))$
23	22	ad3antrrr	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to (A O B \leftrightarrow ((\neg A \in D \land \neg B \in D) \land \exists t \in D t \in (A I B)))$
24	16 21 23	mpbir2and	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to A O B$
25	1 14 2 7 3 15 11 12 13 24	oppne3	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to A \neq B$
26	1 2 3 11 12 13 25	tgelrnln	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to A L B \in ran L$
27	1 2 3 11 12 13 25	tglinerflx1	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to A \in (A L B)$
28	16	simpld	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to \neg A \in D$
29		nelne1	$⊢ (A \in (A L B) \land \neg A \in D) \to A L B \neq D$
30	27 28 29	syl2anc	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to A L B \neq D$
31	25	neneqd	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to \neg A = B$
32	10	orcomd	$⊢ φ \to (A = B \lor C \in (A L B))$
33	32	ord	$⊢ φ \to (\neg A = B \to C \in (A L B))$
34	33	ad3antrrr	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to (\neg A = B \to C \in (A L B))$
35	31 34	mpd	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to C \in (A L B)$
36	9	ad3antrrr	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to C \in D$
37	35 36	elind	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to C \in ((A L B) \cap D)$
38	1 3 2 11 15 17	tglnpt	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to y \in P$
39	1 2 3 11 12 13 38 25 20	btwnlng1	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to y \in (A L B)$
40	39 17	elind	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to y \in ((A L B) \cap D)$
41	1 2 3 11 26 15 30 37 40	tglineineq	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to C = y$
42	41 20	eqeltrd	$⊢ (((φ \land (\neg A \in D \land \neg B \in D)) \land y \in D) \land y \in (A I B)) \to C \in (A I B)$
43	42	adantllr	$⊢ ((((φ \land (\neg A \in D \land \neg B \in D)) \land \exists t \in D t \in (A I B)) \land y \in D) \land y \in (A I B)) \to C \in (A I B)$
44		simpr	$⊢ ((φ \land (\neg A \in D \land \neg B \in D)) \land \exists t \in D t \in (A I B)) \to \exists t \in D t \in (A I B)$
45	18	cbvrexvw	$⊢ \exists t \in D t \in (A I B) \leftrightarrow \exists y \in D y \in (A I B)$
46	44 45	sylib	$⊢ ((φ \land (\neg A \in D \land \neg B \in D)) \land \exists t \in D t \in (A I B)) \to \exists y \in D y \in (A I B)$
47	43 46	r19.29a	$⊢ ((φ \land (\neg A \in D \land \neg B \in D)) \land \exists t \in D t \in (A I B)) \to C \in (A I B)$
48	9	adantr	$⊢ (φ \land C \in (A I B)) \to C \in D$
49		simpr	$⊢ ((φ \land C \in (A I B)) \land t = C) \to t = C$
50	49	eleq1d	$⊢ ((φ \land C \in (A I B)) \land t = C) \to (t \in (A I B) \leftrightarrow C \in (A I B))$
51		simpr	$⊢ (φ \land C \in (A I B)) \to C \in (A I B)$
52	48 50 51	rspcedvd	$⊢ (φ \land C \in (A I B)) \to \exists t \in D t \in (A I B)$
53	52	adantlr	$⊢ ((φ \land (\neg A \in D \land \neg B \in D)) \land C \in (A I B)) \to \exists t \in D t \in (A I B)$
54	47 53	impbida	$⊢ (φ \land (\neg A \in D \land \neg B \in D)) \to (\exists t \in D t \in (A I B) \leftrightarrow C \in (A I B))$
55	54	pm5.32da	$⊢ φ \to (((\neg A \in D \land \neg B \in D) \land \exists t \in D t \in (A I B)) \leftrightarrow ((\neg A \in D \land \neg B \in D) \land C \in (A I B)))$
56		3anrot	$⊢ (C \in (A I B) \land \neg A \in D \land \neg B \in D) \leftrightarrow (\neg A \in D \land \neg B \in D \land C \in (A I B))$
57		df-3an	$⊢ (\neg A \in D \land \neg B \in D \land C \in (A I B)) \leftrightarrow ((\neg A \in D \land \neg B \in D) \land C \in (A I B))$
58	56 57	bitri	$⊢ (C \in (A I B) \land \neg A \in D \land \neg B \in D) \leftrightarrow ((\neg A \in D \land \neg B \in D) \land C \in (A I B))$
59	58	a1i	$⊢ φ \to ((C \in (A I B) \land \neg A \in D \land \neg B \in D) \leftrightarrow ((\neg A \in D \land \neg B \in D) \land C \in (A I B)))$
60	55 22 59	3bitr4d	$⊢ φ \to (A O B \leftrightarrow (C \in (A I B) \land \neg A \in D \land \neg B \in D))$

Metamath Proof Explorer

Theorem colopp

Proof