Metamath Proof Explorer

Theorem tgbtwndiff

Description: There is always a c distinct from B such that B lies between A and c . Theorem 3.14 of Schwabhauser p. 32. The condition "the space is of dimension 1 or more" is written here as 2 <_ ( #P ) for simplicity. (Contributed by Thierry Arnoux, 23-Mar-2019)

Ref Expression
Hypotheses tgbtwndiff.p 
|- P = ( Base ` G )
tgbtwndiff.d 
|- .- = ( dist ` G )
tgbtwndiff.i 
|- I = ( Itv ` G )
tgbtwndiff.g 
|- ( ph -> G e. TarskiG )
tgbtwndiff.a 
|- ( ph -> A e. P )
tgbtwndiff.b 
|- ( ph -> B e. P )
tgbtwndiff.l 
|- ( ph -> 2 <_ ( # ` P ) )
Assertion tgbtwndiff 
|- ( ph -> E. c e. P ( B e. ( A I c ) /\ B =/= c ) )

Proof

Step Hyp Ref Expression
1 tgbtwndiff.p 
 |-  P = ( Base ` G )
2 tgbtwndiff.d 
 |-  .- = ( dist ` G )
3 tgbtwndiff.i 
 |-  I = ( Itv ` G )
4 tgbtwndiff.g 
 |-  ( ph -> G e. TarskiG )
5 tgbtwndiff.a 
 |-  ( ph -> A e. P )
6 tgbtwndiff.b 
 |-  ( ph -> B e. P )
7 tgbtwndiff.l 
 |-  ( ph -> 2 <_ ( # ` P ) )
8 4 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) -> G e. TarskiG )
9 5 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) -> A e. P )
10 6 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) -> B e. P )
11 simpllr 
 |-  ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) -> u e. P )
12 simplr 
 |-  ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) -> v e. P )
13 1 2 3 8 9 10 11 12 axtgsegcon 
 |-  ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) -> E. c e. P ( B e. ( A I c ) /\ ( B .- c ) = ( u .- v ) ) )
14 8 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) /\ c e. P ) /\ ( B .- c ) = ( u .- v ) ) /\ B = c ) -> G e. TarskiG )
15 11 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) /\ c e. P ) /\ ( B .- c ) = ( u .- v ) ) /\ B = c ) -> u e. P )
16 12 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) /\ c e. P ) /\ ( B .- c ) = ( u .- v ) ) /\ B = c ) -> v e. P )
17 10 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) /\ c e. P ) /\ ( B .- c ) = ( u .- v ) ) /\ B = c ) -> B e. P )
18 simpr 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) /\ c e. P ) /\ ( B .- c ) = ( u .- v ) ) /\ B = c ) -> B = c )
19 18 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) /\ c e. P ) /\ ( B .- c ) = ( u .- v ) ) /\ B = c ) -> ( B .- B ) = ( B .- c ) )
20 simplr 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) /\ c e. P ) /\ ( B .- c ) = ( u .- v ) ) /\ B = c ) -> ( B .- c ) = ( u .- v ) )
21 19 20 eqtr2d 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) /\ c e. P ) /\ ( B .- c ) = ( u .- v ) ) /\ B = c ) -> ( u .- v ) = ( B .- B ) )
22 1 2 3 14 15 16 17 21 axtgcgrid 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) /\ c e. P ) /\ ( B .- c ) = ( u .- v ) ) /\ B = c ) -> u = v )
23 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) /\ c e. P ) /\ ( B .- c ) = ( u .- v ) ) /\ B = c ) -> u =/= v )
24 23 neneqd 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) /\ c e. P ) /\ ( B .- c ) = ( u .- v ) ) /\ B = c ) -> -. u = v )
25 22 24 pm2.65da 
 |-  ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) /\ c e. P ) /\ ( B .- c ) = ( u .- v ) ) -> -. B = c )
26 25 neqned 
 |-  ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) /\ c e. P ) /\ ( B .- c ) = ( u .- v ) ) -> B =/= c )
27 26 ex 
 |-  ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) /\ c e. P ) -> ( ( B .- c ) = ( u .- v ) -> B =/= c ) )
28 27 anim2d 
 |-  ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) /\ c e. P ) -> ( ( B e. ( A I c ) /\ ( B .- c ) = ( u .- v ) ) -> ( B e. ( A I c ) /\ B =/= c ) ) )
29 28 reximdva 
 |-  ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) -> ( E. c e. P ( B e. ( A I c ) /\ ( B .- c ) = ( u .- v ) ) -> E. c e. P ( B e. ( A I c ) /\ B =/= c ) ) )
30 13 29 mpd 
 |-  ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ u =/= v ) -> E. c e. P ( B e. ( A I c ) /\ B =/= c ) )
31 1 2 3 4 7 tglowdim1 
 |-  ( ph -> E. u e. P E. v e. P u =/= v )
32 30 31 r19.29vva 
 |-  ( ph -> E. c e. P ( B e. ( A I c ) /\ B =/= c ) )