Metamath Proof Explorer

Theorem opptgdim2

Description: If two points opposite to a line exist, dimension must be 2 or more. (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 opptgdim2 
|- ( ph -> G TarskiGDim>= 2 )

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 7 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( D = ( x L y ) /\ x =/= y ) ) -> G e. TarskiG )
12 simpllr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( D = ( x L y ) /\ x =/= y ) ) -> x e. P )
13 simplr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( D = ( x L y ) /\ x =/= y ) ) -> y e. P )
14 8 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( D = ( x L y ) /\ x =/= y ) ) -> A e. P )
15 1 2 3 4 5 6 7 8 9 10 oppne1 
 |-  ( ph -> -. A e. D )
16 15 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( D = ( x L y ) /\ x =/= y ) ) -> -. A e. D )
17 simprl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( D = ( x L y ) /\ x =/= y ) ) -> D = ( x L y ) )
18 16 17 neleqtrd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( D = ( x L y ) /\ x =/= y ) ) -> -. A e. ( x L y ) )
19 simprr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( D = ( x L y ) /\ x =/= y ) ) -> x =/= y )
20 19 neneqd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( D = ( x L y ) /\ x =/= y ) ) -> -. x = y )
21 ioran 
 |-  ( -. ( A e. ( x L y ) \/ x = y ) <-> ( -. A e. ( x L y ) /\ -. x = y ) )
22 18 20 21 sylanbrc 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( D = ( x L y ) /\ x =/= y ) ) -> -. ( A e. ( x L y ) \/ x = y ) )
23 1 5 3 11 12 13 14 22 ncoltgdim2 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( D = ( x L y ) /\ x =/= y ) ) -> G TarskiGDim>= 2 )
24 1 3 5 7 6 tgisline 
 |-  ( ph -> E. x e. P E. y e. P ( D = ( x L y ) /\ x =/= y ) )
25 23 24 r19.29vva 
 |-  ( ph -> G TarskiGDim>= 2 )