Metamath Proof Explorer

Theorem oppne3

Description: Points lying on opposite sides of a line cannot be equal. (Contributed by Thierry Arnoux, 3-Aug-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 oppne3 
|- ( ph -> A =/= B )

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 5 6 7 8 9 10 oppne1 
 |-  ( ph -> -. A e. D )
12 7 ad3antrrr 
 |-  ( ( ( ( ph /\ A = B ) /\ t e. D ) /\ t e. ( A I B ) ) -> G e. TarskiG )
13 8 ad3antrrr 
 |-  ( ( ( ( ph /\ A = B ) /\ t e. D ) /\ t e. ( A I B ) ) -> A e. P )
14 6 ad3antrrr 
 |-  ( ( ( ( ph /\ A = B ) /\ t e. D ) /\ t e. ( A I B ) ) -> D e. ran L )
15 simplr 
 |-  ( ( ( ( ph /\ A = B ) /\ t e. D ) /\ t e. ( A I B ) ) -> t e. D )
16 1 5 3 12 14 15 tglnpt 
 |-  ( ( ( ( ph /\ A = B ) /\ t e. D ) /\ t e. ( A I B ) ) -> t e. P )
17 simpr 
 |-  ( ( ( ( ph /\ A = B ) /\ t e. D ) /\ t e. ( A I B ) ) -> t e. ( A I B ) )
18 simpllr 
 |-  ( ( ( ( ph /\ A = B ) /\ t e. D ) /\ t e. ( A I B ) ) -> A = B )
19 18 oveq2d 
 |-  ( ( ( ( ph /\ A = B ) /\ t e. D ) /\ t e. ( A I B ) ) -> ( A I A ) = ( A I B ) )
20 17 19 eleqtrrd 
 |-  ( ( ( ( ph /\ A = B ) /\ t e. D ) /\ t e. ( A I B ) ) -> t e. ( A I A ) )
21 1 2 3 12 13 16 20 axtgbtwnid 
 |-  ( ( ( ( ph /\ A = B ) /\ t e. D ) /\ t e. ( A I B ) ) -> A = t )
22 21 15 eqeltrd 
 |-  ( ( ( ( ph /\ A = B ) /\ t e. D ) /\ t e. ( A I B ) ) -> A e. D )
23 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 ) ) ) )
24 10 23 mpbid 
 |-  ( ph -> ( ( -. A e. D /\ -. B e. D ) /\ E. t e. D t e. ( A I B ) ) )
25 24 simprd 
 |-  ( ph -> E. t e. D t e. ( A I B ) )
26 25 adantr 
 |-  ( ( ph /\ A = B ) -> E. t e. D t e. ( A I B ) )
27 22 26 r19.29a 
 |-  ( ( ph /\ A = B ) -> A e. D )
28 11 27 mtand 
 |-  ( ph -> -. A = B )
29 28 neqned 
 |-  ( ph -> A =/= B )