Metamath Proof Explorer

Theorem tglndim0

Description: There are no lines in dimension 0. (Contributed by Thierry Arnoux, 18-Oct-2019)

Ref Expression
Hypotheses tglineelsb2.p 
|- B = ( Base ` G )
tglineelsb2.i 
|- I = ( Itv ` G )
tglineelsb2.l 
|- L = ( LineG ` G )
tglineelsb2.g 
|- ( ph -> G e. TarskiG )
tglndim0.d 
|- ( ph -> ( # ` B ) = 1 )
Assertion tglndim0 
|- ( ph -> -. A e. ran L )

Proof

Step Hyp Ref Expression
1 tglineelsb2.p 
 |-  B = ( Base ` G )
2 tglineelsb2.i 
 |-  I = ( Itv ` G )
3 tglineelsb2.l 
 |-  L = ( LineG ` G )
4 tglineelsb2.g 
 |-  ( ph -> G e. TarskiG )
5 tglndim0.d 
 |-  ( ph -> ( # ` B ) = 1 )
6 5 ad4antr 
 |-  ( ( ( ( ( ph /\ A e. ran L ) /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) -> ( # ` B ) = 1 )
7 simpllr 
 |-  ( ( ( ( ( ph /\ A e. ran L ) /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) -> x e. B )
8 simplr 
 |-  ( ( ( ( ( ph /\ A e. ran L ) /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) -> y e. B )
9 1 6 7 8 tgldim0eq 
 |-  ( ( ( ( ( ph /\ A e. ran L ) /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) -> x = y )
10 simprr 
 |-  ( ( ( ( ( ph /\ A e. ran L ) /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) -> x =/= y )
11 9 10 pm2.21ddne 
 |-  ( ( ( ( ( ph /\ A e. ran L ) /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) -> F. )
12 4 adantr 
 |-  ( ( ph /\ A e. ran L ) -> G e. TarskiG )
13 simpr 
 |-  ( ( ph /\ A e. ran L ) -> A e. ran L )
14 1 2 3 12 13 tgisline 
 |-  ( ( ph /\ A e. ran L ) -> E. x e. B E. y e. B ( A = ( x L y ) /\ x =/= y ) )
15 11 14 r19.29vva 
 |-  ( ( ph /\ A e. ran L ) -> F. )
16 15 inegd 
 |-  ( ph -> -. A e. ran L )