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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgbtwndiff.d ⊢ − = ( dist ‘ 𝐺 )
tgbtwndiff.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgbtwndiff.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgbtwndiff.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
tgbtwndiff.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
tgbtwndiff.l ⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝑃 ) )
Assertion tgbtwndiff ( 𝜑 → ∃ 𝑐 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ 𝐵 ≠ 𝑐 ) )

Proof

Step Hyp Ref Expression
1 tgbtwndiff.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgbtwndiff.d ⊢ − = ( dist ‘ 𝐺 )
3 tgbtwndiff.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tgbtwndiff.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 tgbtwndiff.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 tgbtwndiff.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 tgbtwndiff.l ⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝑃 ) )
8 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) → 𝐺 ∈ TarskiG )
9 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) → 𝐴 ∈ 𝑃 )
10 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) → 𝐵 ∈ 𝑃 )
11 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) → 𝑢 ∈ 𝑃 )
12 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) → 𝑣 ∈ 𝑃 )
13 1 2 3 8 9 10 11 12 axtgsegcon ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) → ∃ 𝑐 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑢 − 𝑣 ) ) )
14 8 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑢 − 𝑣 ) ) ∧ 𝐵 = 𝑐 ) → 𝐺 ∈ TarskiG )
15 11 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑢 − 𝑣 ) ) ∧ 𝐵 = 𝑐 ) → 𝑢 ∈ 𝑃 )
16 12 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑢 − 𝑣 ) ) ∧ 𝐵 = 𝑐 ) → 𝑣 ∈ 𝑃 )
17 10 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑢 − 𝑣 ) ) ∧ 𝐵 = 𝑐 ) → 𝐵 ∈ 𝑃 )
18 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑢 − 𝑣 ) ) ∧ 𝐵 = 𝑐 ) → 𝐵 = 𝑐 )
19 18 oveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑢 − 𝑣 ) ) ∧ 𝐵 = 𝑐 ) → ( 𝐵 − 𝐵 ) = ( 𝐵 − 𝑐 ) )
20 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑢 − 𝑣 ) ) ∧ 𝐵 = 𝑐 ) → ( 𝐵 − 𝑐 ) = ( 𝑢 − 𝑣 ) )
21 19 20 eqtr2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑢 − 𝑣 ) ) ∧ 𝐵 = 𝑐 ) → ( 𝑢 − 𝑣 ) = ( 𝐵 − 𝐵 ) )
22 1 2 3 14 15 16 17 21 axtgcgrid ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑢 − 𝑣 ) ) ∧ 𝐵 = 𝑐 ) → 𝑢 = 𝑣 )
23 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑢 − 𝑣 ) ) ∧ 𝐵 = 𝑐 ) → 𝑢 ≠ 𝑣 )
24 23 neneqd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑢 − 𝑣 ) ) ∧ 𝐵 = 𝑐 ) → ¬ 𝑢 = 𝑣 )
25 22 24 pm2.65da ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑢 − 𝑣 ) ) → ¬ 𝐵 = 𝑐 )
26 25 neqned ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑢 − 𝑣 ) ) → 𝐵 ≠ 𝑐 )
27 26 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ 𝑃 ) → ( ( 𝐵 − 𝑐 ) = ( 𝑢 − 𝑣 ) → 𝐵 ≠ 𝑐 ) )
28 27 anim2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ 𝑃 ) → ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑢 − 𝑣 ) ) → ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ 𝐵 ≠ 𝑐 ) ) )
29 28 reximdva ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) → ( ∃ 𝑐 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑢 − 𝑣 ) ) → ∃ 𝑐 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ 𝐵 ≠ 𝑐 ) ) )
30 13 29 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑢 ≠ 𝑣 ) → ∃ 𝑐 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ 𝐵 ≠ 𝑐 ) )
31 1 2 3 4 7 tglowdim1 ⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 𝑢 ≠ 𝑣 )
32 30 31 r19.29vva ⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ 𝐵 ≠ 𝑐 ) )