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 ⊢hp𝒢=g∈V⟼d∈ran⁡Line𝒢⁡g⟼ab|[˙Baseg/p]˙[˙Itv⁡g/i]˙∃c∈pa∈p∖d∧c∈p∖d∧∃t∈dt∈aic∧b∈p∖d∧c∈p∖d∧∃t∈dt∈bic

Detailed syntax breakdown

Step Hyp Ref Expression
0 chpg classhp𝒢
1 vg setvarg
2 cvv classV
3 vd setvard
4 clng classLine𝒢
5 1 cv setvarg
6 5 4 cfv classLine𝒢⁡g
7 6 crn classran⁡Line𝒢⁡g
8 va setvara
9 vb setvarb
10 cbs classBase
11 5 10 cfv classBaseg
12 vp setvarp
13 citv classItv
14 5 13 cfv classItv⁡g
15 vi setvari
16 vc setvarc
17 12 cv setvarp
18 8 cv setvara
19 3 cv setvard
20 17 19 cdif classp∖d
21 18 20 wcel wffa∈p∖d
22 16 cv setvarc
23 22 20 wcel wffc∈p∖d
24 21 23 wa wffa∈p∖d∧c∈p∖d
25 vt setvart
26 25 cv setvart
27 15 cv setvari
28 18 22 27 co classaic
29 26 28 wcel wfft∈aic
30 29 25 19 wrex wff∃t∈dt∈aic
31 24 30 wa wffa∈p∖d∧c∈p∖d∧∃t∈dt∈aic
32 9 cv setvarb
33 32 20 wcel wffb∈p∖d
34 33 23 wa wffb∈p∖d∧c∈p∖d
35 32 22 27 co classbic
36 26 35 wcel wfft∈bic
37 36 25 19 wrex wff∃t∈dt∈bic
38 34 37 wa wffb∈p∖d∧c∈p∖d∧∃t∈dt∈bic
39 31 38 wa wffa∈p∖d∧c∈p∖d∧∃t∈dt∈aic∧b∈p∖d∧c∈p∖d∧∃t∈dt∈bic
40 39 16 17 wrex wff∃c∈pa∈p∖d∧c∈p∖d∧∃t∈dt∈aic∧b∈p∖d∧c∈p∖d∧∃t∈dt∈bic
41 40 15 14 wsbc wff[˙Itv⁡g/i]˙∃c∈pa∈p∖d∧c∈p∖d∧∃t∈dt∈aic∧b∈p∖d∧c∈p∖d∧∃t∈dt∈bic
42 41 12 11 wsbc wff[˙Baseg/p]˙[˙Itv⁡g/i]˙∃c∈pa∈p∖d∧c∈p∖d∧∃t∈dt∈aic∧b∈p∖d∧c∈p∖d∧∃t∈dt∈bic
43 42 8 9 copab classab|[˙Baseg/p]˙[˙Itv⁡g/i]˙∃c∈pa∈p∖d∧c∈p∖d∧∃t∈dt∈aic∧b∈p∖d∧c∈p∖d∧∃t∈dt∈bic
44 3 7 43 cmpt classd∈ran⁡Line𝒢⁡g⟼ab|[˙Baseg/p]˙[˙Itv⁡g/i]˙∃c∈pa∈p∖d∧c∈p∖d∧∃t∈dt∈aic∧b∈p∖d∧c∈p∖d∧∃t∈dt∈bic
45 1 2 44 cmpt classg∈V⟼d∈ran⁡Line𝒢⁡g⟼ab|[˙Baseg/p]˙[˙Itv⁡g/i]˙∃c∈pa∈p∖d∧c∈p∖d∧∃t∈dt∈aic∧b∈p∖d∧c∈p∖d∧∃t∈dt∈bic
46 0 45 wceq wffhp𝒢=g∈V⟼d∈ran⁡Line𝒢⁡g⟼ab|[˙Baseg/p]˙[˙Itv⁡g/i]˙∃c∈pa∈p∖d∧c∈p∖d∧∃t∈dt∈aic∧b∈p∖d∧c∈p∖d∧∃t∈dt∈bic