hpgerlem

Description: Lemma for the proof that the half-plane relation is an equivalence relation. Lemma 9.10 of Schwabhauser p. 72. (Contributed by Thierry Arnoux, 4-Mar-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))\}$
	hpgid.1	$⊢ φ \to \neg A \in D$
Assertion	hpgerlem	$⊢ φ \to \exists c \in P A O c$

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		hpgid.1	$⊢ φ \to \neg A \in D$
9	3 4 5	tglnne0	$⊢ φ \to D \neq \emptyset$
10		n0	$⊢ D \neq \emptyset \leftrightarrow \exists x x \in D$
11	9 10	sylib	$⊢ φ \to \exists x x \in D$
12		eqid	$⊢ dist (G) = dist (G)$
13	4	adantr	$⊢ (φ \land x \in D) \to G \in 𝒢_{Tarski}$
14	6	adantr	$⊢ (φ \land x \in D) \to A \in P$
15	5	adantr	$⊢ (φ \land x \in D) \to D \in ran L$
16		simpr	$⊢ (φ \land x \in D) \to x \in D$
17	1 3 2 13 15 16	tglnpt	$⊢ (φ \land x \in D) \to x \in P$
18	5	adantr	$⊢ (φ \land \|P\| = 1) \to D \in ran L$
19	4	adantr	$⊢ (φ \land \|P\| = 1) \to G \in 𝒢_{Tarski}$
20		simpr	$⊢ (φ \land \|P\| = 1) \to \|P\| = 1$
21	1 2 3 19 20	tglndim0	$⊢ (φ \land \|P\| = 1) \to \neg D \in ran L$
22	18 21	pm2.65da	$⊢ φ \to \neg \|P\| = 1$
23	1 6	tgldimor	$⊢ φ \to (\|P\| = 1 \lor 2 \leq \|P\|)$
24	23	ord	$⊢ φ \to (\neg \|P\| = 1 \to 2 \leq \|P\|)$
25	22 24	mpd	$⊢ φ \to 2 \leq \|P\|$
26	25	adantr	$⊢ (φ \land x \in D) \to 2 \leq \|P\|$
27	1 12 2 13 14 17 26	tgbtwndiff	$⊢ (φ \land x \in D) \to \exists c \in P (x \in (A I c) \land x \neq c)$
28	8	ad4antr	$⊢ ((((φ \land x \in D) \land c \in P) \land x \in (A I c)) \land x \neq c) \to \neg A \in D$
29	13	ad4antr	$⊢ (((((φ \land x \in D) \land c \in P) \land x \in (A I c)) \land x \neq c) \land c \in D) \to G \in 𝒢_{Tarski}$
30	17	ad4antr	$⊢ (((((φ \land x \in D) \land c \in P) \land x \in (A I c)) \land x \neq c) \land c \in D) \to x \in P$
31		simpr	$⊢ ((φ \land x \in D) \land c \in P) \to c \in P$
32	31	ad3antrrr	$⊢ (((((φ \land x \in D) \land c \in P) \land x \in (A I c)) \land x \neq c) \land c \in D) \to c \in P$
33	14	ad4antr	$⊢ (((((φ \land x \in D) \land c \in P) \land x \in (A I c)) \land x \neq c) \land c \in D) \to A \in P$
34		simplr	$⊢ (((((φ \land x \in D) \land c \in P) \land x \in (A I c)) \land x \neq c) \land c \in D) \to x \neq c$
35		simplr	$⊢ ((((φ \land x \in D) \land c \in P) \land x \in (A I c)) \land x \neq c) \to x \in (A I c)$
36	35	adantr	$⊢ (((((φ \land x \in D) \land c \in P) \land x \in (A I c)) \land x \neq c) \land c \in D) \to x \in (A I c)$
37	1 2 3 29 30 32 33 34 36	btwnlng2	$⊢ (((((φ \land x \in D) \land c \in P) \land x \in (A I c)) \land x \neq c) \land c \in D) \to A \in (x L c)$
38	15	ad4antr	$⊢ (((((φ \land x \in D) \land c \in P) \land x \in (A I c)) \land x \neq c) \land c \in D) \to D \in ran L$
39	16	ad4antr	$⊢ (((((φ \land x \in D) \land c \in P) \land x \in (A I c)) \land x \neq c) \land c \in D) \to x \in D$
40		simpr	$⊢ (((((φ \land x \in D) \land c \in P) \land x \in (A I c)) \land x \neq c) \land c \in D) \to c \in D$
41	1 2 3 29 30 32 34 34 38 39 40	tglinethru	$⊢ (((((φ \land x \in D) \land c \in P) \land x \in (A I c)) \land x \neq c) \land c \in D) \to D = x L c$
42	37 41	eleqtrrd	$⊢ (((((φ \land x \in D) \land c \in P) \land x \in (A I c)) \land x \neq c) \land c \in D) \to A \in D$
43	28 42	mtand	$⊢ ((((φ \land x \in D) \land c \in P) \land x \in (A I c)) \land x \neq c) \to \neg c \in D$
44		eleq1w	$⊢ t = x \to (t \in (A I c) \leftrightarrow x \in (A I c))$
45	44	rspcev	$⊢ (x \in D \land x \in (A I c)) \to \exists t \in D t \in (A I c)$
46	45	ad5ant24	$⊢ ((((φ \land x \in D) \land c \in P) \land x \in (A I c)) \land x \neq c) \to \exists t \in D t \in (A I c)$
47	28 43 46	jca31	$⊢ ((((φ \land x \in D) \land c \in P) \land x \in (A I c)) \land x \neq c) \to ((\neg A \in D \land \neg c \in D) \land \exists t \in D t \in (A I c))$
48	47	anasss	$⊢ (((φ \land x \in D) \land c \in P) \land (x \in (A I c) \land x \neq c)) \to ((\neg A \in D \land \neg c \in D) \land \exists t \in D t \in (A I c))$
49	14	adantr	$⊢ ((φ \land x \in D) \land c \in P) \to A \in P$
50	1 12 2 7 49 31	islnopp	$⊢ ((φ \land x \in D) \land c \in P) \to (A O c \leftrightarrow ((\neg A \in D \land \neg c \in D) \land \exists t \in D t \in (A I c)))$
51	50	adantr	$⊢ (((φ \land x \in D) \land c \in P) \land (x \in (A I c) \land x \neq c)) \to (A O c \leftrightarrow ((\neg A \in D \land \neg c \in D) \land \exists t \in D t \in (A I c)))$
52	48 51	mpbird	$⊢ (((φ \land x \in D) \land c \in P) \land (x \in (A I c) \land x \neq c)) \to A O c$
53	52	ex	$⊢ ((φ \land x \in D) \land c \in P) \to ((x \in (A I c) \land x \neq c) \to A O c)$
54	53	reximdva	$⊢ (φ \land x \in D) \to (\exists c \in P (x \in (A I c) \land x \neq c) \to \exists c \in P A O c)$
55	27 54	mpd	$⊢ (φ \land x \in D) \to \exists c \in P A O c$
56	11 55	exlimddv	$⊢ φ \to \exists c \in P A O c$

Metamath Proof Explorer

Theorem hpgerlem

Proof