Database
ELEMENTARY GEOMETRY
Tarskian Geometry
Half-planes
lnoppnhpg
Metamath Proof Explorer
Description: If two points lie on the opposite side of a line D , they are not on
the same half-plane. Theorem 9.9 of Schwabhauser p. 72. (Contributed by Thierry Arnoux , 4-Mar-2020)
Ref
Expression
Hypotheses
ishpg.p
⊢ 𝑃 = ( Base ‘ 𝐺 )
ishpg.i
⊢ 𝐼 = ( Itv ‘ 𝐺 )
ishpg.l
⊢ 𝐿 = ( LineG ‘ 𝐺 )
ishpg.o
⊢ 𝑂 = { 〈 𝑎 , 𝑏 〉 ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
ishpg.g
⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
ishpg.d
⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
hpgbr.a
⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
hpgbr.b
⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
lnoppnhpg.1
⊢ ( 𝜑 → 𝐴 𝑂 𝐵 )
Assertion
lnoppnhpg
⊢ ( 𝜑 → ¬ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 )
Proof
Step
Hyp
Ref
Expression
1
ishpg.p
⊢ 𝑃 = ( Base ‘ 𝐺 )
2
ishpg.i
⊢ 𝐼 = ( Itv ‘ 𝐺 )
3
ishpg.l
⊢ 𝐿 = ( LineG ‘ 𝐺 )
4
ishpg.o
⊢ 𝑂 = { 〈 𝑎 , 𝑏 〉 ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
5
ishpg.g
⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6
ishpg.d
⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
7
hpgbr.a
⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8
hpgbr.b
⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9
lnoppnhpg.1
⊢ ( 𝜑 → 𝐴 𝑂 𝐵 )
10
eqid
⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
11
1 10 2 4 3 6 5 8
oppnid
⊢ ( 𝜑 → ¬ 𝐵 𝑂 𝐵 )
12
1 2 3 4 5 6 7 8 8 9
lnopp2hpgb
⊢ ( 𝜑 → ( 𝐵 𝑂 𝐵 ↔ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) )
13
11 12
mtbid
⊢ ( 𝜑 → ¬ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 )