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 ⟼ a b | [˙Base g / p]˙ [˙ Itv ⁡ g / i]˙ ∃ c ∈ p a ∈ p ∖ d ∧ c ∈ p ∖ d ∧ ∃ t ∈ d t ∈ a i c ∧ b ∈ p ∖ d ∧ c ∈ p ∖ d ∧ ∃ t ∈ d t ∈ b i c

Detailed syntax breakdown

Step Hyp Ref Expression
0 chpg class hp 𝒢
1 vg setvar g
2 cvv class V
3 vd setvar d
4 clng class Line 𝒢
5 1 cv setvar g
6 5 4 cfv class Line 𝒢 ⁡ g
7 6 crn class ran ⁡ Line 𝒢 ⁡ g
8 va setvar a
9 vb setvar b
10 cbs class Base
11 5 10 cfv class Base g
12 vp setvar p
13 citv class Itv
14 5 13 cfv class Itv ⁡ g
15 vi setvar i
16 vc setvar c
17 12 cv setvar p
18 8 cv setvar a
19 3 cv setvar d
20 17 19 cdif class p ∖ d
21 18 20 wcel wff a ∈ p ∖ d
22 16 cv setvar c
23 22 20 wcel wff c ∈ p ∖ d
24 21 23 wa wff a ∈ p ∖ d ∧ c ∈ p ∖ d
25 vt setvar t
26 25 cv setvar t
27 15 cv setvar i
28 18 22 27 co class a i c
29 26 28 wcel wff t ∈ a i c
30 29 25 19 wrex wff ∃ t ∈ d t ∈ a i c
31 24 30 wa wff a ∈ p ∖ d ∧ c ∈ p ∖ d ∧ ∃ t ∈ d t ∈ a i c
32 9 cv setvar b
33 32 20 wcel wff b ∈ p ∖ d
34 33 23 wa wff b ∈ p ∖ d ∧ c ∈ p ∖ d
35 32 22 27 co class b i c
36 26 35 wcel wff t ∈ b i c
37 36 25 19 wrex wff ∃ t ∈ d t ∈ b i c
38 34 37 wa wff b ∈ p ∖ d ∧ c ∈ p ∖ d ∧ ∃ t ∈ d t ∈ b i c
39 31 38 wa wff a ∈ p ∖ d ∧ c ∈ p ∖ d ∧ ∃ t ∈ d t ∈ a i c ∧ b ∈ p ∖ d ∧ c ∈ p ∖ d ∧ ∃ t ∈ d t ∈ b i c
40 39 16 17 wrex wff ∃ c ∈ p a ∈ p ∖ d ∧ c ∈ p ∖ d ∧ ∃ t ∈ d t ∈ a i c ∧ b ∈ p ∖ d ∧ c ∈ p ∖ d ∧ ∃ t ∈ d t ∈ b i c
41 40 15 14 wsbc wff [˙ Itv ⁡ g / i]˙ ∃ c ∈ p a ∈ p ∖ d ∧ c ∈ p ∖ d ∧ ∃ t ∈ d t ∈ a i c ∧ b ∈ p ∖ d ∧ c ∈ p ∖ d ∧ ∃ t ∈ d t ∈ b i c
42 41 12 11 wsbc wff [˙Base g / p]˙ [˙ Itv ⁡ g / i]˙ ∃ c ∈ p a ∈ p ∖ d ∧ c ∈ p ∖ d ∧ ∃ t ∈ d t ∈ a i c ∧ b ∈ p ∖ d ∧ c ∈ p ∖ d ∧ ∃ t ∈ d t ∈ b i c
43 42 8 9 copab class a b | [˙Base g / p]˙ [˙ Itv ⁡ g / i]˙ ∃ c ∈ p a ∈ p ∖ d ∧ c ∈ p ∖ d ∧ ∃ t ∈ d t ∈ a i c ∧ b ∈ p ∖ d ∧ c ∈ p ∖ d ∧ ∃ t ∈ d t ∈ b i c
44 3 7 43 cmpt class d ∈ ran ⁡ Line 𝒢 ⁡ g ⟼ a b | [˙Base g / p]˙ [˙ Itv ⁡ g / i]˙ ∃ c ∈ p a ∈ p ∖ d ∧ c ∈ p ∖ d ∧ ∃ t ∈ d t ∈ a i c ∧ b ∈ p ∖ d ∧ c ∈ p ∖ d ∧ ∃ t ∈ d t ∈ b i c
45 1 2 44 cmpt class g ∈ V ⟼ d ∈ ran ⁡ Line 𝒢 ⁡ g ⟼ a b | [˙Base g / p]˙ [˙ Itv ⁡ g / i]˙ ∃ c ∈ p a ∈ p ∖ d ∧ c ∈ p ∖ d ∧ ∃ t ∈ d t ∈ a i c ∧ b ∈ p ∖ d ∧ c ∈ p ∖ d ∧ ∃ t ∈ d t ∈ b i c
46 0 45 wceq wff hp 𝒢 = g ∈ V ⟼ d ∈ ran ⁡ Line 𝒢 ⁡ g ⟼ a b | [˙Base g / p]˙ [˙ Itv ⁡ g / i]˙ ∃ c ∈ p a ∈ p ∖ d ∧ c ∈ p ∖ d ∧ ∃ t ∈ d t ∈ a i c ∧ b ∈ p ∖ d ∧ c ∈ p ∖ d ∧ ∃ t ∈ d t ∈ b i c