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 = ( 𝑔 ∈ V ↦ ( 𝑑 ∈ ran ( LineG ‘ 𝑔 ) ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ]𝑐𝑝 ( ( ( 𝑎 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 chpg hpG
1 vg 𝑔
2 cvv V
3 vd 𝑑
4 clng LineG
5 1 cv 𝑔
6 5 4 cfv ( LineG ‘ 𝑔 )
7 6 crn ran ( LineG ‘ 𝑔 )
8 va 𝑎
9 vb 𝑏
10 cbs Base
11 5 10 cfv ( Base ‘ 𝑔 )
12 vp 𝑝
13 citv Itv
14 5 13 cfv ( Itv ‘ 𝑔 )
15 vi 𝑖
16 vc 𝑐
17 12 cv 𝑝
18 8 cv 𝑎
19 3 cv 𝑑
20 17 19 cdif ( 𝑝𝑑 )
21 18 20 wcel 𝑎 ∈ ( 𝑝𝑑 )
22 16 cv 𝑐
23 22 20 wcel 𝑐 ∈ ( 𝑝𝑑 )
24 21 23 wa ( 𝑎 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) )
25 vt 𝑡
26 25 cv 𝑡
27 15 cv 𝑖
28 18 22 27 co ( 𝑎 𝑖 𝑐 )
29 26 28 wcel 𝑡 ∈ ( 𝑎 𝑖 𝑐 )
30 29 25 19 wrex 𝑡𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 )
31 24 30 wa ( ( 𝑎 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) )
32 9 cv 𝑏
33 32 20 wcel 𝑏 ∈ ( 𝑝𝑑 )
34 33 23 wa ( 𝑏 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) )
35 32 22 27 co ( 𝑏 𝑖 𝑐 )
36 26 35 wcel 𝑡 ∈ ( 𝑏 𝑖 𝑐 )
37 36 25 19 wrex 𝑡𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 )
38 34 37 wa ( ( 𝑏 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) )
39 31 38 wa ( ( ( 𝑎 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) )
40 39 16 17 wrex 𝑐𝑝 ( ( ( 𝑎 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) )
41 40 15 14 wsbc [ ( Itv ‘ 𝑔 ) / 𝑖 ]𝑐𝑝 ( ( ( 𝑎 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) )
42 41 12 11 wsbc [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ]𝑐𝑝 ( ( ( 𝑎 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) )
43 42 8 9 copab { ⟨ 𝑎 , 𝑏 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ]𝑐𝑝 ( ( ( 𝑎 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) ) }
44 3 7 43 cmpt ( 𝑑 ∈ ran ( LineG ‘ 𝑔 ) ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ]𝑐𝑝 ( ( ( 𝑎 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) ) } )
45 1 2 44 cmpt ( 𝑔 ∈ V ↦ ( 𝑑 ∈ ran ( LineG ‘ 𝑔 ) ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ]𝑐𝑝 ( ( ( 𝑎 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) ) } ) )
46 0 45 wceq hpG = ( 𝑔 ∈ V ↦ ( 𝑑 ∈ ran ( LineG ‘ 𝑔 ) ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ]𝑐𝑝 ( ( ( 𝑎 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) ) } ) )