Theorem 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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	hpgid.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	hpgid.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	hpgid.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	hpgid.d	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
	hpgid.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	hpgid.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
	hpgid.1	⊢ ( 𝜑 → ¬ 𝐴 ∈ 𝐷 )
Assertion	hpgerlem	⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝑃 𝐴 𝑂 𝑐 )

Proof

Step	Hyp	Ref	Expression
1		hpgid.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		hpgid.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		hpgid.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		hpgid.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		hpgid.d	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
6		hpgid.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7		hpgid.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
8		hpgid.1	⊢ ( 𝜑 → ¬ 𝐴 ∈ 𝐷 )
9	3 4 5	tglnne0	⊢ ( 𝜑 → 𝐷 ≠ ∅ )
10		n0	⊢ ( 𝐷 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐷 )
11	9 10	sylib	⊢ ( 𝜑 → ∃ 𝑥 𝑥 ∈ 𝐷 )
12		eqid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
13	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐺 ∈ TarskiG )
14	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ 𝑃 )
15	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐷 ∈ ran 𝐿 )
16		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 )
17	1 3 2 13 15 16	tglnpt	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝑃 )
18	5	adantr	⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐷 ∈ ran 𝐿 )
19	4	adantr	⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐺 ∈ TarskiG )
20		simpr	⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( ♯ ‘ 𝑃 ) = 1 )
21	1 2 3 19 20	tglndim0	⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ¬ 𝐷 ∈ ran 𝐿 )
22	18 21	pm2.65da	⊢ ( 𝜑 → ¬ ( ♯ ‘ 𝑃 ) = 1 )
23	1 6	tgldimor	⊢ ( 𝜑 → ( ( ♯ ‘ 𝑃 ) = 1 ∨ 2 ≤ ( ♯ ‘ 𝑃 ) ) )
24	23	ord	⊢ ( 𝜑 → ( ¬ ( ♯ ‘ 𝑃 ) = 1 → 2 ≤ ( ♯ ‘ 𝑃 ) ) )
25	22 24	mpd	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝑃 ) )
26	25	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 2 ≤ ( ♯ ‘ 𝑃 ) )
27	1 12 2 13 14 17 26	tgbtwndiff	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ∃ 𝑐 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ∧ 𝑥 ≠ 𝑐 ) )
28	8	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ) ∧ 𝑥 ≠ 𝑐 ) → ¬ 𝐴 ∈ 𝐷 )
29	13	ad4antr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ) ∧ 𝑥 ≠ 𝑐 ) ∧ 𝑐 ∈ 𝐷 ) → 𝐺 ∈ TarskiG )
30	17	ad4antr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ) ∧ 𝑥 ≠ 𝑐 ) ∧ 𝑐 ∈ 𝐷 ) → 𝑥 ∈ 𝑃 )
31		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) → 𝑐 ∈ 𝑃 )
32	31	ad3antrrr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ) ∧ 𝑥 ≠ 𝑐 ) ∧ 𝑐 ∈ 𝐷 ) → 𝑐 ∈ 𝑃 )
33	14	ad4antr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ) ∧ 𝑥 ≠ 𝑐 ) ∧ 𝑐 ∈ 𝐷 ) → 𝐴 ∈ 𝑃 )
34		simplr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ) ∧ 𝑥 ≠ 𝑐 ) ∧ 𝑐 ∈ 𝐷 ) → 𝑥 ≠ 𝑐 )
35		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ) ∧ 𝑥 ≠ 𝑐 ) → 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) )
36	35	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ) ∧ 𝑥 ≠ 𝑐 ) ∧ 𝑐 ∈ 𝐷 ) → 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) )
37	1 2 3 29 30 32 33 34 36	btwnlng2	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ) ∧ 𝑥 ≠ 𝑐 ) ∧ 𝑐 ∈ 𝐷 ) → 𝐴 ∈ ( 𝑥 𝐿 𝑐 ) )
38	15	ad4antr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ) ∧ 𝑥 ≠ 𝑐 ) ∧ 𝑐 ∈ 𝐷 ) → 𝐷 ∈ ran 𝐿 )
39	16	ad4antr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ) ∧ 𝑥 ≠ 𝑐 ) ∧ 𝑐 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 )
40		simpr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ) ∧ 𝑥 ≠ 𝑐 ) ∧ 𝑐 ∈ 𝐷 ) → 𝑐 ∈ 𝐷 )
41	1 2 3 29 30 32 34 34 38 39 40	tglinethru	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ) ∧ 𝑥 ≠ 𝑐 ) ∧ 𝑐 ∈ 𝐷 ) → 𝐷 = ( 𝑥 𝐿 𝑐 ) )
42	37 41	eleqtrrd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ) ∧ 𝑥 ≠ 𝑐 ) ∧ 𝑐 ∈ 𝐷 ) → 𝐴 ∈ 𝐷 )
43	28 42	mtand	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ) ∧ 𝑥 ≠ 𝑐 ) → ¬ 𝑐 ∈ 𝐷 )
44		eleq1w	⊢ ( 𝑡 = 𝑥 → ( 𝑡 ∈ ( 𝐴 𝐼 𝑐 ) ↔ 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ) )
45	44	rspcev	⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ) → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝑐 ) )
46	45	ad5ant24	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ) ∧ 𝑥 ≠ 𝑐 ) → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝑐 ) )
47	28 43 46	jca31	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ) ∧ 𝑥 ≠ 𝑐 ) → ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝑐 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝑐 ) ) )
48	47	anasss	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ∧ 𝑥 ≠ 𝑐 ) ) → ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝑐 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝑐 ) ) )
49	14	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) → 𝐴 ∈ 𝑃 )
50	1 12 2 7 49 31	islnopp	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) → ( 𝐴 𝑂 𝑐 ↔ ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝑐 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝑐 ) ) ) )
51	50	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ∧ 𝑥 ≠ 𝑐 ) ) → ( 𝐴 𝑂 𝑐 ↔ ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝑐 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝑐 ) ) ) )
52	48 51	mpbird	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ∧ 𝑥 ≠ 𝑐 ) ) → 𝐴 𝑂 𝑐 )
53	52	ex	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝑃 ) → ( ( 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ∧ 𝑥 ≠ 𝑐 ) → 𝐴 𝑂 𝑐 ) )
54	53	reximdva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ∃ 𝑐 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝑐 ) ∧ 𝑥 ≠ 𝑐 ) → ∃ 𝑐 ∈ 𝑃 𝐴 𝑂 𝑐 ) )
55	27 54	mpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ∃ 𝑐 ∈ 𝑃 𝐴 𝑂 𝑐 )
56	11 55	exlimddv	⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝑃 𝐴 𝑂 𝑐 )