Metamath Proof Explorer


Theorem oppne2

Description: Points lying on opposite sides of a line cannot be on the line. (Contributed by Thierry Arnoux, 3-Mar-2020)

Ref Expression
Hypotheses hpg.p
|- P = ( Base ` G )
hpg.d
|- .- = ( dist ` G )
hpg.i
|- I = ( Itv ` G )
hpg.o
|- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
opphl.l
|- L = ( LineG ` G )
opphl.d
|- ( ph -> D e. ran L )
opphl.g
|- ( ph -> G e. TarskiG )
oppcom.a
|- ( ph -> A e. P )
oppcom.b
|- ( ph -> B e. P )
oppcom.o
|- ( ph -> A O B )
Assertion oppne2
|- ( ph -> -. B e. D )

Proof

Step Hyp Ref Expression
1 hpg.p
 |-  P = ( Base ` G )
2 hpg.d
 |-  .- = ( dist ` G )
3 hpg.i
 |-  I = ( Itv ` G )
4 hpg.o
 |-  O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
5 opphl.l
 |-  L = ( LineG ` G )
6 opphl.d
 |-  ( ph -> D e. ran L )
7 opphl.g
 |-  ( ph -> G e. TarskiG )
8 oppcom.a
 |-  ( ph -> A e. P )
9 oppcom.b
 |-  ( ph -> B e. P )
10 oppcom.o
 |-  ( ph -> A O B )
11 1 2 3 4 8 9 islnopp
 |-  ( ph -> ( A O B <-> ( ( -. A e. D /\ -. B e. D ) /\ E. t e. D t e. ( A I B ) ) ) )
12 10 11 mpbid
 |-  ( ph -> ( ( -. A e. D /\ -. B e. D ) /\ E. t e. D t e. ( A I B ) ) )
13 12 simplrd
 |-  ( ph -> -. B e. D )