Metamath Proof Explorer

Theorem tglowdim2l

Description: Reformulation of the lower dimension axiom for dimension two. There exist three non-colinear points. Theorem 6.24 of Schwabhauser p. 46. (Contributed by Thierry Arnoux, 30-May-2019)

Ref Expression
Hypotheses tglineintmo.p 
|- P = ( Base ` G )
tglineintmo.i 
|- I = ( Itv ` G )
tglineintmo.l 
|- L = ( LineG ` G )
tglineintmo.g 
|- ( ph -> G e. TarskiG )
tglowdim2l.1 
|- ( ph -> G TarskiGDim>= 2 )
Assertion tglowdim2l 
|- ( ph -> E. a e. P E. b e. P E. c e. P -. ( c e. ( a L b ) \/ a = b ) )

Proof

Step Hyp Ref Expression
1 tglineintmo.p 
 |-  P = ( Base ` G )
2 tglineintmo.i 
 |-  I = ( Itv ` G )
3 tglineintmo.l 
 |-  L = ( LineG ` G )
4 tglineintmo.g 
 |-  ( ph -> G e. TarskiG )
5 tglowdim2l.1 
 |-  ( ph -> G TarskiGDim>= 2 )
6 eqid 
 |-  ( dist ` G ) = ( dist ` G )
7 1 6 2 4 5 axtglowdim2 
 |-  ( ph -> E. a e. P E. b e. P E. c e. P -. ( c e. ( a I b ) \/ a e. ( c I b ) \/ b e. ( a I c ) ) )
8 4 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ c e. P ) -> G e. TarskiG )
9 simpllr 
 |-  ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ c e. P ) -> a e. P )
10 simplr 
 |-  ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ c e. P ) -> b e. P )
11 simpr 
 |-  ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ c e. P ) -> c e. P )
12 1 3 2 8 9 10 11 tgcolg 
 |-  ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ c e. P ) -> ( ( c e. ( a L b ) \/ a = b ) <-> ( c e. ( a I b ) \/ a e. ( c I b ) \/ b e. ( a I c ) ) ) )
13 12 notbid 
 |-  ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ c e. P ) -> ( -. ( c e. ( a L b ) \/ a = b ) <-> -. ( c e. ( a I b ) \/ a e. ( c I b ) \/ b e. ( a I c ) ) ) )
14 13 rexbidva 
 |-  ( ( ( ph /\ a e. P ) /\ b e. P ) -> ( E. c e. P -. ( c e. ( a L b ) \/ a = b ) <-> E. c e. P -. ( c e. ( a I b ) \/ a e. ( c I b ) \/ b e. ( a I c ) ) ) )
15 14 rexbidva 
 |-  ( ( ph /\ a e. P ) -> ( E. b e. P E. c e. P -. ( c e. ( a L b ) \/ a = b ) <-> E. b e. P E. c e. P -. ( c e. ( a I b ) \/ a e. ( c I b ) \/ b e. ( a I c ) ) ) )
16 15 rexbidva 
 |-  ( ph -> ( E. a e. P E. b e. P E. c e. P -. ( c e. ( a L b ) \/ a = b ) <-> E. a e. P E. b e. P E. c e. P -. ( c e. ( a I b ) \/ a e. ( c I b ) \/ b e. ( a I c ) ) ) )
17 7 16 mpbird 
 |-  ( ph -> E. a e. P E. b e. P E. c e. P -. ( c e. ( a L b ) \/ a = b ) )