Definition df-hpg 27119

Description: Define the open half plane relation for a geometry 𝐺. Definition 9.7 of [Schwabhauser] p. 71. See hpgbr 27121 to find the same formulation. (Contributed by Thierry Arnoux, 4-Mar-2020.)

Assertion

Ref	Expression
df-hpg	⊢ hpG = (𝑔 ∈ V ↦ (𝑑 ∈ ran (LineG‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))}))

Distinct variable group:   𝑎,𝑏,𝑐,𝑑,𝑔,𝑖,𝑝,𝑡

Detailed syntax breakdown of Definition df-hpg

Step	Hyp	Ref	Expression
1		chpg 27118	. 2 class hpG
2		vg	. . 3 setvar 𝑔
3		cvv 3432	. . 3 class V
4		vd	. . . 4 setvar 𝑑
5	2	cv 1538	. . . . . 6 class 𝑔
6		clng 26795	. . . . . 6 class LineG
7	5, 6	cfv 6433	. . . . 5 class (LineG‘𝑔)
8	7	crn 5590	. . . 4 class ran (LineG‘𝑔)
9		va	. . . . . . . . . . . . 13 setvar 𝑎
10	9	cv 1538	. . . . . . . . . . . 12 class 𝑎
11		vp	. . . . . . . . . . . . . 14 setvar 𝑝
12	11	cv 1538	. . . . . . . . . . . . 13 class 𝑝
13	4	cv 1538	. . . . . . . . . . . . 13 class 𝑑
14	12, 13	cdif 3884	. . . . . . . . . . . 12 class (𝑝 ∖ 𝑑)
15	10, 14	wcel 2106	. . . . . . . . . . 11 wff 𝑎 ∈ (𝑝 ∖ 𝑑)
16		vc	. . . . . . . . . . . . 13 setvar 𝑐
17	16	cv 1538	. . . . . . . . . . . 12 class 𝑐
18	17, 14	wcel 2106	. . . . . . . . . . 11 wff 𝑐 ∈ (𝑝 ∖ 𝑑)
19	15, 18	wa 396	. . . . . . . . . 10 wff (𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑))
20		vt	. . . . . . . . . . . . 13 setvar 𝑡
21	20	cv 1538	. . . . . . . . . . . 12 class 𝑡
22		vi	. . . . . . . . . . . . . 14 setvar 𝑖
23	22	cv 1538	. . . . . . . . . . . . 13 class 𝑖
24	10, 17, 23	co 7275	. . . . . . . . . . . 12 class (𝑎𝑖𝑐)
25	21, 24	wcel 2106	. . . . . . . . . . 11 wff 𝑡 ∈ (𝑎𝑖𝑐)
26	25, 20, 13	wrex 3065	. . . . . . . . . 10 wff ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)
27	19, 26	wa 396	. . . . . . . . 9 wff ((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐))
28		vb	. . . . . . . . . . . . 13 setvar 𝑏
29	28	cv 1538	. . . . . . . . . . . 12 class 𝑏
30	29, 14	wcel 2106	. . . . . . . . . . 11 wff 𝑏 ∈ (𝑝 ∖ 𝑑)
31	30, 18	wa 396	. . . . . . . . . 10 wff (𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑))
32	29, 17, 23	co 7275	. . . . . . . . . . . 12 class (𝑏𝑖𝑐)
33	21, 32	wcel 2106	. . . . . . . . . . 11 wff 𝑡 ∈ (𝑏𝑖𝑐)
34	33, 20, 13	wrex 3065	. . . . . . . . . 10 wff ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)
35	31, 34	wa 396	. . . . . . . . 9 wff ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐))
36	27, 35	wa 396	. . . . . . . 8 wff (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))
37	36, 16, 12	wrex 3065	. . . . . . 7 wff ∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))
38		citv 26794	. . . . . . . 8 class Itv
39	5, 38	cfv 6433	. . . . . . 7 class (Itv‘𝑔)
40	37, 22, 39	wsbc 3716	. . . . . 6 wff [(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))
41		cbs 16912	. . . . . . 7 class Base
42	5, 41	cfv 6433	. . . . . 6 class (Base‘𝑔)
43	40, 11, 42	wsbc 3716	. . . . 5 wff [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))
44	43, 9, 28	copab 5136	. . . 4 class {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))}
45	4, 8, 44	cmpt 5157	. . 3 class (𝑑 ∈ ran (LineG‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))})
46	2, 3, 45	cmpt 5157	. 2 class (𝑔 ∈ V ↦ (𝑑 ∈ ran (LineG‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))}))
47	1, 46	wceq 1539	1 wff hpG = (𝑔 ∈ V ↦ (𝑑 ∈ ran (LineG‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))}))

This definition is referenced by:  ishpg  27120