Definition df-hpg 25650

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

Assertion

Ref	Expression
df-hpg	|- hpG = ( g e. _V |-> ( d e. ran (LineG ` g ) |-> { <. a , b >. | [. ( Base ` g ) / p ]. [. (Itv ` g ) / i ]. E. c e. p ( ( ( a e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( a i c ) ) /\ ( ( b e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( b i c ) ) ) } ) )

Distinct variable group:   a, b, c, d, g, i, p, t

Detailed syntax breakdown of Definition df-hpg

Step	Hyp	Ref	Expression
1		chpg 25649	. 2 class hpG
2		vg	. . 3 setvar g
3		cvv 3200	. . 3 class _V
4		vd	. . . 4 setvar d
5	2	cv 1482	. . . . . 6 class g
6		clng 25336	. . . . . 6 class LineG
7	5, 6	cfv 5888	. . . . 5 class (LineG ` g )
8	7	crn 5115	. . . 4 class ran (LineG ` g )
9		va	. . . . . . . . . . . . 13 setvar a
10	9	cv 1482	. . . . . . . . . . . 12 class a
11		vp	. . . . . . . . . . . . . 14 setvar p
12	11	cv 1482	. . . . . . . . . . . . 13 class p
13	4	cv 1482	. . . . . . . . . . . . 13 class d
14	12, 13	cdif 3571	. . . . . . . . . . . 12 class ( p \ d )
15	10, 14	wcel 1990	. . . . . . . . . . 11 wff a e. ( p \ d )
16		vc	. . . . . . . . . . . . 13 setvar c
17	16	cv 1482	. . . . . . . . . . . 12 class c
18	17, 14	wcel 1990	. . . . . . . . . . 11 wff c e. ( p \ d )
19	15, 18	wa 384	. . . . . . . . . 10 wff ( a e. ( p \ d ) /\ c e. ( p \ d ) )
20		vt	. . . . . . . . . . . . 13 setvar t
21	20	cv 1482	. . . . . . . . . . . 12 class t
22		vi	. . . . . . . . . . . . . 14 setvar i
23	22	cv 1482	. . . . . . . . . . . . 13 class i
24	10, 17, 23	co 6650	. . . . . . . . . . . 12 class ( a i c )
25	21, 24	wcel 1990	. . . . . . . . . . 11 wff t e. ( a i c )
26	25, 20, 13	wrex 2913	. . . . . . . . . 10 wff E. t e. d t e. ( a i c )
27	19, 26	wa 384	. . . . . . . . 9 wff ( ( a e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( a i c ) )
28		vb	. . . . . . . . . . . . 13 setvar b
29	28	cv 1482	. . . . . . . . . . . 12 class b
30	29, 14	wcel 1990	. . . . . . . . . . 11 wff b e. ( p \ d )
31	30, 18	wa 384	. . . . . . . . . 10 wff ( b e. ( p \ d ) /\ c e. ( p \ d ) )
32	29, 17, 23	co 6650	. . . . . . . . . . . 12 class ( b i c )
33	21, 32	wcel 1990	. . . . . . . . . . 11 wff t e. ( b i c )
34	33, 20, 13	wrex 2913	. . . . . . . . . 10 wff E. t e. d t e. ( b i c )
35	31, 34	wa 384	. . . . . . . . 9 wff ( ( b e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( b i c ) )
36	27, 35	wa 384	. . . . . . . 8 wff ( ( ( a e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( a i c ) ) /\ ( ( b e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( b i c ) ) )
37	36, 16, 12	wrex 2913	. . . . . . 7 wff E. c e. p ( ( ( a e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( a i c ) ) /\ ( ( b e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( b i c ) ) )
38		citv 25335	. . . . . . . 8 class Itv
39	5, 38	cfv 5888	. . . . . . 7 class (Itv ` g )
40	37, 22, 39	wsbc 3435	. . . . . 6 wff [. (Itv ` g ) / i ]. E. c e. p ( ( ( a e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( a i c ) ) /\ ( ( b e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( b i c ) ) )
41		cbs 15857	. . . . . . 7 class Base
42	5, 41	cfv 5888	. . . . . 6 class ( Base ` g )
43	40, 11, 42	wsbc 3435	. . . . 5 wff [. ( Base ` g ) / p ]. [. (Itv ` g ) / i ]. E. c e. p ( ( ( a e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( a i c ) ) /\ ( ( b e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( b i c ) ) )
44	43, 9, 28	copab 4712	. . . 4 class { <. a , b >. | [. ( Base ` g ) / p ]. [. (Itv ` g ) / i ]. E. c e. p ( ( ( a e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( a i c ) ) /\ ( ( b e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( b i c ) ) ) }
45	4, 8, 44	cmpt 4729	. . 3 class ( d e. ran (LineG ` g ) |-> { <. a , b >. | [. ( Base ` g ) / p ]. [. (Itv ` g ) / i ]. E. c e. p ( ( ( a e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( a i c ) ) /\ ( ( b e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( b i c ) ) ) } )
46	2, 3, 45	cmpt 4729	. 2 class ( g e. _V |-> ( d e. ran (LineG ` g ) |-> { <. a , b >. | [. ( Base ` g ) / p ]. [. (Itv ` g ) / i ]. E. c e. p ( ( ( a e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( a i c ) ) /\ ( ( b e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( b i c ) ) ) } ) )
47	1, 46	wceq 1483	1 wff hpG = ( g e. _V |-> ( d e. ran (LineG ` g ) |-> { <. a , b >. | [. ( Base ` g ) / p ]. [. (Itv ` g ) / i ]. E. c e. p ( ( ( a e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( a i c ) ) /\ ( ( b e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( b i c ) ) ) } ) )

This definition is referenced by:  ishpg  25651