Metamath Proof Explorer

Definition df-hpg

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

Ref Expression
Assertion 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 ) ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 chpg 
 |-  hpG
1 vg 
 |-  g
2 cvv 
 |-  _V
3 vd 
 |-  d
4 clng 
 |-  LineG
5 1 cv 
 |-  g
6 5 4 cfv 
 |-  ( LineG ` g )
7 6 crn 
 |-  ran ( LineG ` g )
8 va 
 |-  a
9 vb 
 |-  b
10 cbs 
 |-  Base
11 5 10 cfv 
 |-  ( Base ` g )
12 vp 
 |-  p
13 citv 
 |-  Itv
14 5 13 cfv 
 |-  ( Itv ` g )
15 vi 
 |-  i
16 vc 
 |-  c
17 12 cv 
 |-  p
18 8 cv 
 |-  a
19 3 cv 
 |-  d
20 17 19 cdif 
 |-  ( p \ d )
21 18 20 wcel 
 |-  a e. ( p \ d )
22 16 cv 
 |-  c
23 22 20 wcel 
 |-  c e. ( p \ d )
24 21 23 wa 
 |-  ( a e. ( p \ d ) /\ c e. ( p \ d ) )
25 vt 
 |-  t
26 25 cv 
 |-  t
27 15 cv 
 |-  i
28 18 22 27 co 
 |-  ( a i c )
29 26 28 wcel 
 |-  t e. ( a i c )
30 29 25 19 wrex 
 |-  E. t e. d t e. ( a i c )
31 24 30 wa 
 |-  ( ( a e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( a i c ) )
32 9 cv 
 |-  b
33 32 20 wcel 
 |-  b e. ( p \ d )
34 33 23 wa 
 |-  ( b e. ( p \ d ) /\ c e. ( p \ d ) )
35 32 22 27 co 
 |-  ( b i c )
36 26 35 wcel 
 |-  t e. ( b i c )
37 36 25 19 wrex 
 |-  E. t e. d t e. ( b i c )
38 34 37 wa 
 |-  ( ( b e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( b i c ) )
39 31 38 wa 
 |-  ( ( ( 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 ) ) )
40 39 16 17 wrex 
 |-  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 40 15 14 wsbc 
 |-  [. ( 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 ) ) )
42 41 12 11 wsbc 
 |-  [. ( 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 ) ) )
43 42 8 9 copab 
 |-  { <. 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 ) ) ) }
44 3 7 43 cmpt 
 |-  ( 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 ) ) ) } )
45 1 2 44 cmpt 
 |-  ( 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 ) ) ) } ) )
46 0 45 wceq 
 |-  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 ) ) ) } ) )