MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-hpg Structured version   Visualization version   GIF version

Definition df-hpg 28009
Description: Define the open half plane relation for a geometry 𝐺. Definition 9.7 of [Schwabhauser] p. 71. See hpgbr 28011 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
StepHypRef Expression
1 chpg 28008 . 2 class hpG
2 vg . . 3 setvar 𝑔
3 cvv 3475 . . 3 class V
4 vd . . . 4 setvar 𝑑
52cv 1541 . . . . . 6 class 𝑔
6 clng 27685 . . . . . 6 class LineG
75, 6cfv 6544 . . . . 5 class (LineGβ€˜π‘”)
87crn 5678 . . . 4 class ran (LineGβ€˜π‘”)
9 va . . . . . . . . . . . . 13 setvar π‘Ž
109cv 1541 . . . . . . . . . . . 12 class π‘Ž
11 vp . . . . . . . . . . . . . 14 setvar 𝑝
1211cv 1541 . . . . . . . . . . . . 13 class 𝑝
134cv 1541 . . . . . . . . . . . . 13 class 𝑑
1412, 13cdif 3946 . . . . . . . . . . . 12 class (𝑝 βˆ– 𝑑)
1510, 14wcel 2107 . . . . . . . . . . 11 wff π‘Ž ∈ (𝑝 βˆ– 𝑑)
16 vc . . . . . . . . . . . . 13 setvar 𝑐
1716cv 1541 . . . . . . . . . . . 12 class 𝑐
1817, 14wcel 2107 . . . . . . . . . . 11 wff 𝑐 ∈ (𝑝 βˆ– 𝑑)
1915, 18wa 397 . . . . . . . . . 10 wff (π‘Ž ∈ (𝑝 βˆ– 𝑑) ∧ 𝑐 ∈ (𝑝 βˆ– 𝑑))
20 vt . . . . . . . . . . . . 13 setvar 𝑑
2120cv 1541 . . . . . . . . . . . 12 class 𝑑
22 vi . . . . . . . . . . . . . 14 setvar 𝑖
2322cv 1541 . . . . . . . . . . . . 13 class 𝑖
2410, 17, 23co 7409 . . . . . . . . . . . 12 class (π‘Žπ‘–π‘)
2521, 24wcel 2107 . . . . . . . . . . 11 wff 𝑑 ∈ (π‘Žπ‘–π‘)
2625, 20, 13wrex 3071 . . . . . . . . . 10 wff βˆƒπ‘‘ ∈ 𝑑 𝑑 ∈ (π‘Žπ‘–π‘)
2719, 26wa 397 . . . . . . . . 9 wff ((π‘Ž ∈ (𝑝 βˆ– 𝑑) ∧ 𝑐 ∈ (𝑝 βˆ– 𝑑)) ∧ βˆƒπ‘‘ ∈ 𝑑 𝑑 ∈ (π‘Žπ‘–π‘))
28 vb . . . . . . . . . . . . 13 setvar 𝑏
2928cv 1541 . . . . . . . . . . . 12 class 𝑏
3029, 14wcel 2107 . . . . . . . . . . 11 wff 𝑏 ∈ (𝑝 βˆ– 𝑑)
3130, 18wa 397 . . . . . . . . . 10 wff (𝑏 ∈ (𝑝 βˆ– 𝑑) ∧ 𝑐 ∈ (𝑝 βˆ– 𝑑))
3229, 17, 23co 7409 . . . . . . . . . . . 12 class (𝑏𝑖𝑐)
3321, 32wcel 2107 . . . . . . . . . . 11 wff 𝑑 ∈ (𝑏𝑖𝑐)
3433, 20, 13wrex 3071 . . . . . . . . . 10 wff βˆƒπ‘‘ ∈ 𝑑 𝑑 ∈ (𝑏𝑖𝑐)
3531, 34wa 397 . . . . . . . . 9 wff ((𝑏 ∈ (𝑝 βˆ– 𝑑) ∧ 𝑐 ∈ (𝑝 βˆ– 𝑑)) ∧ βˆƒπ‘‘ ∈ 𝑑 𝑑 ∈ (𝑏𝑖𝑐))
3627, 35wa 397 . . . . . . . 8 wff (((π‘Ž ∈ (𝑝 βˆ– 𝑑) ∧ 𝑐 ∈ (𝑝 βˆ– 𝑑)) ∧ βˆƒπ‘‘ ∈ 𝑑 𝑑 ∈ (π‘Žπ‘–π‘)) ∧ ((𝑏 ∈ (𝑝 βˆ– 𝑑) ∧ 𝑐 ∈ (𝑝 βˆ– 𝑑)) ∧ βˆƒπ‘‘ ∈ 𝑑 𝑑 ∈ (𝑏𝑖𝑐)))
3736, 16, 12wrex 3071 . . . . . . 7 wff βˆƒπ‘ ∈ 𝑝 (((π‘Ž ∈ (𝑝 βˆ– 𝑑) ∧ 𝑐 ∈ (𝑝 βˆ– 𝑑)) ∧ βˆƒπ‘‘ ∈ 𝑑 𝑑 ∈ (π‘Žπ‘–π‘)) ∧ ((𝑏 ∈ (𝑝 βˆ– 𝑑) ∧ 𝑐 ∈ (𝑝 βˆ– 𝑑)) ∧ βˆƒπ‘‘ ∈ 𝑑 𝑑 ∈ (𝑏𝑖𝑐)))
38 citv 27684 . . . . . . . 8 class Itv
395, 38cfv 6544 . . . . . . 7 class (Itvβ€˜π‘”)
4037, 22, 39wsbc 3778 . . . . . 6 wff [(Itvβ€˜π‘”) / 𝑖]βˆƒπ‘ ∈ 𝑝 (((π‘Ž ∈ (𝑝 βˆ– 𝑑) ∧ 𝑐 ∈ (𝑝 βˆ– 𝑑)) ∧ βˆƒπ‘‘ ∈ 𝑑 𝑑 ∈ (π‘Žπ‘–π‘)) ∧ ((𝑏 ∈ (𝑝 βˆ– 𝑑) ∧ 𝑐 ∈ (𝑝 βˆ– 𝑑)) ∧ βˆƒπ‘‘ ∈ 𝑑 𝑑 ∈ (𝑏𝑖𝑐)))
41 cbs 17144 . . . . . . 7 class Base
425, 41cfv 6544 . . . . . 6 class (Baseβ€˜π‘”)
4340, 11, 42wsbc 3778 . . . . 5 wff [(Baseβ€˜π‘”) / 𝑝][(Itvβ€˜π‘”) / 𝑖]βˆƒπ‘ ∈ 𝑝 (((π‘Ž ∈ (𝑝 βˆ– 𝑑) ∧ 𝑐 ∈ (𝑝 βˆ– 𝑑)) ∧ βˆƒπ‘‘ ∈ 𝑑 𝑑 ∈ (π‘Žπ‘–π‘)) ∧ ((𝑏 ∈ (𝑝 βˆ– 𝑑) ∧ 𝑐 ∈ (𝑝 βˆ– 𝑑)) ∧ βˆƒπ‘‘ ∈ 𝑑 𝑑 ∈ (𝑏𝑖𝑐)))
4443, 9, 28copab 5211 . . . 4 class {βŸ¨π‘Ž, π‘βŸ© ∣ [(Baseβ€˜π‘”) / 𝑝][(Itvβ€˜π‘”) / 𝑖]βˆƒπ‘ ∈ 𝑝 (((π‘Ž ∈ (𝑝 βˆ– 𝑑) ∧ 𝑐 ∈ (𝑝 βˆ– 𝑑)) ∧ βˆƒπ‘‘ ∈ 𝑑 𝑑 ∈ (π‘Žπ‘–π‘)) ∧ ((𝑏 ∈ (𝑝 βˆ– 𝑑) ∧ 𝑐 ∈ (𝑝 βˆ– 𝑑)) ∧ βˆƒπ‘‘ ∈ 𝑑 𝑑 ∈ (𝑏𝑖𝑐)))}
454, 8, 44cmpt 5232 . . 3 class (𝑑 ∈ ran (LineGβ€˜π‘”) ↦ {βŸ¨π‘Ž, π‘βŸ© ∣ [(Baseβ€˜π‘”) / 𝑝][(Itvβ€˜π‘”) / 𝑖]βˆƒπ‘ ∈ 𝑝 (((π‘Ž ∈ (𝑝 βˆ– 𝑑) ∧ 𝑐 ∈ (𝑝 βˆ– 𝑑)) ∧ βˆƒπ‘‘ ∈ 𝑑 𝑑 ∈ (π‘Žπ‘–π‘)) ∧ ((𝑏 ∈ (𝑝 βˆ– 𝑑) ∧ 𝑐 ∈ (𝑝 βˆ– 𝑑)) ∧ βˆƒπ‘‘ ∈ 𝑑 𝑑 ∈ (𝑏𝑖𝑐)))})
462, 3, 45cmpt 5232 . 2 class (𝑔 ∈ V ↦ (𝑑 ∈ ran (LineGβ€˜π‘”) ↦ {βŸ¨π‘Ž, π‘βŸ© ∣ [(Baseβ€˜π‘”) / 𝑝][(Itvβ€˜π‘”) / 𝑖]βˆƒπ‘ ∈ 𝑝 (((π‘Ž ∈ (𝑝 βˆ– 𝑑) ∧ 𝑐 ∈ (𝑝 βˆ– 𝑑)) ∧ βˆƒπ‘‘ ∈ 𝑑 𝑑 ∈ (π‘Žπ‘–π‘)) ∧ ((𝑏 ∈ (𝑝 βˆ– 𝑑) ∧ 𝑐 ∈ (𝑝 βˆ– 𝑑)) ∧ βˆƒπ‘‘ ∈ 𝑑 𝑑 ∈ (𝑏𝑖𝑐)))}))
471, 46wceq 1542 1 wff hpG = (𝑔 ∈ V ↦ (𝑑 ∈ ran (LineGβ€˜π‘”) ↦ {βŸ¨π‘Ž, π‘βŸ© ∣ [(Baseβ€˜π‘”) / 𝑝][(Itvβ€˜π‘”) / 𝑖]βˆƒπ‘ ∈ 𝑝 (((π‘Ž ∈ (𝑝 βˆ– 𝑑) ∧ 𝑐 ∈ (𝑝 βˆ– 𝑑)) ∧ βˆƒπ‘‘ ∈ 𝑑 𝑑 ∈ (π‘Žπ‘–π‘)) ∧ ((𝑏 ∈ (𝑝 βˆ– 𝑑) ∧ 𝑐 ∈ (𝑝 βˆ– 𝑑)) ∧ βˆƒπ‘‘ ∈ 𝑑 𝑑 ∈ (𝑏𝑖𝑐)))}))
Colors of variables: wff setvar class
This definition is referenced by:  ishpg  28010
  Copyright terms: Public domain W3C validator