Metamath Proof Explorer

Theorem tglowdim2ln

Description: There is always one point outside of any line. Theorem 6.25 of Schwabhauser p. 46. (Contributed by Thierry Arnoux, 16-Nov-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 )
tglowdim2ln.a 
|- ( ph -> A e. P )
tglowdim2ln.b 
|- ( ph -> B e. P )
tglowdim2ln.1 
|- ( ph -> A =/= B )
Assertion tglowdim2ln 
|- ( ph -> E. c e. P -. c e. ( A L 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 tglowdim2ln.a 
 |-  ( ph -> A e. P )
7 tglowdim2ln.b 
 |-  ( ph -> B e. P )
8 tglowdim2ln.1 
 |-  ( ph -> A =/= B )
9 1 2 3 4 5 tglowdim2l 
 |-  ( ph -> E. a e. P E. b e. P E. z e. P -. ( z e. ( a L b ) \/ a = b ) )
10 9 adantr 
 |-  ( ( ph /\ A. c e. P c e. ( A L B ) ) -> E. a e. P E. b e. P E. z e. P -. ( z e. ( a L b ) \/ a = b ) )
11 eleq1w 
 |-  ( c = z -> ( c e. ( A L B ) <-> z e. ( A L B ) ) )
12 simpllr 
 |-  ( ( ( ( ph /\ A. c e. P c e. ( A L B ) ) /\ ( a e. P /\ b e. P /\ z e. P ) ) /\ -. a = b ) -> A. c e. P c e. ( A L B ) )
13 simplr3 
 |-  ( ( ( ( ph /\ A. c e. P c e. ( A L B ) ) /\ ( a e. P /\ b e. P /\ z e. P ) ) /\ -. a = b ) -> z e. P )
14 11 12 13 rspcdva 
 |-  ( ( ( ( ph /\ A. c e. P c e. ( A L B ) ) /\ ( a e. P /\ b e. P /\ z e. P ) ) /\ -. a = b ) -> z e. ( A L B ) )
15 4 ad3antrrr 
 |-  ( ( ( ( ph /\ A. c e. P c e. ( A L B ) ) /\ ( a e. P /\ b e. P /\ z e. P ) ) /\ -. a = b ) -> G e. TarskiG )
16 simplr1 
 |-  ( ( ( ( ph /\ A. c e. P c e. ( A L B ) ) /\ ( a e. P /\ b e. P /\ z e. P ) ) /\ -. a = b ) -> a e. P )
17 simplr2 
 |-  ( ( ( ( ph /\ A. c e. P c e. ( A L B ) ) /\ ( a e. P /\ b e. P /\ z e. P ) ) /\ -. a = b ) -> b e. P )
18 simpr 
 |-  ( ( ( ( ph /\ A. c e. P c e. ( A L B ) ) /\ ( a e. P /\ b e. P /\ z e. P ) ) /\ -. a = b ) -> -. a = b )
19 18 neqned 
 |-  ( ( ( ( ph /\ A. c e. P c e. ( A L B ) ) /\ ( a e. P /\ b e. P /\ z e. P ) ) /\ -. a = b ) -> a =/= b )
20 6 ad3antrrr 
 |-  ( ( ( ( ph /\ A. c e. P c e. ( A L B ) ) /\ ( a e. P /\ b e. P /\ z e. P ) ) /\ -. a = b ) -> A e. P )
21 7 ad3antrrr 
 |-  ( ( ( ( ph /\ A. c e. P c e. ( A L B ) ) /\ ( a e. P /\ b e. P /\ z e. P ) ) /\ -. a = b ) -> B e. P )
22 8 ad3antrrr 
 |-  ( ( ( ( ph /\ A. c e. P c e. ( A L B ) ) /\ ( a e. P /\ b e. P /\ z e. P ) ) /\ -. a = b ) -> A =/= B )
23 1 2 3 15 20 21 22 tgelrnln 
 |-  ( ( ( ( ph /\ A. c e. P c e. ( A L B ) ) /\ ( a e. P /\ b e. P /\ z e. P ) ) /\ -. a = b ) -> ( A L B ) e. ran L )
24 eleq1w 
 |-  ( c = a -> ( c e. ( A L B ) <-> a e. ( A L B ) ) )
25 24 12 16 rspcdva 
 |-  ( ( ( ( ph /\ A. c e. P c e. ( A L B ) ) /\ ( a e. P /\ b e. P /\ z e. P ) ) /\ -. a = b ) -> a e. ( A L B ) )
26 eleq1w 
 |-  ( c = b -> ( c e. ( A L B ) <-> b e. ( A L B ) ) )
27 26 12 17 rspcdva 
 |-  ( ( ( ( ph /\ A. c e. P c e. ( A L B ) ) /\ ( a e. P /\ b e. P /\ z e. P ) ) /\ -. a = b ) -> b e. ( A L B ) )
28 1 2 3 15 16 17 19 19 23 25 27 tglinethru 
 |-  ( ( ( ( ph /\ A. c e. P c e. ( A L B ) ) /\ ( a e. P /\ b e. P /\ z e. P ) ) /\ -. a = b ) -> ( A L B ) = ( a L b ) )
29 14 28 eleqtrd 
 |-  ( ( ( ( ph /\ A. c e. P c e. ( A L B ) ) /\ ( a e. P /\ b e. P /\ z e. P ) ) /\ -. a = b ) -> z e. ( a L b ) )
30 29 ex 
 |-  ( ( ( ph /\ A. c e. P c e. ( A L B ) ) /\ ( a e. P /\ b e. P /\ z e. P ) ) -> ( -. a = b -> z e. ( a L b ) ) )
31 30 orrd 
 |-  ( ( ( ph /\ A. c e. P c e. ( A L B ) ) /\ ( a e. P /\ b e. P /\ z e. P ) ) -> ( a = b \/ z e. ( a L b ) ) )
32 31 orcomd 
 |-  ( ( ( ph /\ A. c e. P c e. ( A L B ) ) /\ ( a e. P /\ b e. P /\ z e. P ) ) -> ( z e. ( a L b ) \/ a = b ) )
33 32 ralrimivvva 
 |-  ( ( ph /\ A. c e. P c e. ( A L B ) ) -> A. a e. P A. b e. P A. z e. P ( z e. ( a L b ) \/ a = b ) )
34 dfral2 
 |-  ( A. z e. P ( z e. ( a L b ) \/ a = b ) <-> -. E. z e. P -. ( z e. ( a L b ) \/ a = b ) )
35 34 ralbii 
 |-  ( A. b e. P A. z e. P ( z e. ( a L b ) \/ a = b ) <-> A. b e. P -. E. z e. P -. ( z e. ( a L b ) \/ a = b ) )
36 ralnex 
 |-  ( A. b e. P -. E. z e. P -. ( z e. ( a L b ) \/ a = b ) <-> -. E. b e. P E. z e. P -. ( z e. ( a L b ) \/ a = b ) )
37 35 36 bitri 
 |-  ( A. b e. P A. z e. P ( z e. ( a L b ) \/ a = b ) <-> -. E. b e. P E. z e. P -. ( z e. ( a L b ) \/ a = b ) )
38 37 ralbii 
 |-  ( A. a e. P A. b e. P A. z e. P ( z e. ( a L b ) \/ a = b ) <-> A. a e. P -. E. b e. P E. z e. P -. ( z e. ( a L b ) \/ a = b ) )
39 ralnex 
 |-  ( A. a e. P -. E. b e. P E. z e. P -. ( z e. ( a L b ) \/ a = b ) <-> -. E. a e. P E. b e. P E. z e. P -. ( z e. ( a L b ) \/ a = b ) )
40 38 39 bitri 
 |-  ( A. a e. P A. b e. P A. z e. P ( z e. ( a L b ) \/ a = b ) <-> -. E. a e. P E. b e. P E. z e. P -. ( z e. ( a L b ) \/ a = b ) )
41 33 40 sylib 
 |-  ( ( ph /\ A. c e. P c e. ( A L B ) ) -> -. E. a e. P E. b e. P E. z e. P -. ( z e. ( a L b ) \/ a = b ) )
42 10 41 pm2.65da 
 |-  ( ph -> -. A. c e. P c e. ( A L B ) )
43 rexnal 
 |-  ( E. c e. P -. c e. ( A L B ) <-> -. A. c e. P c e. ( A L B ) )
44 42 43 sylibr 
 |-  ( ph -> E. c e. P -. c e. ( A L B ) )