Metamath Proof Explorer

Theorem legbtwn

Description: Deduce betweenness from "less than" relation. Corresponds loosely to Proposition 6.13 of Schwabhauser p. 45. (Contributed by Thierry Arnoux, 25-Aug-2019)

Ref Expression
Hypotheses legval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
legval.d ⊢ − = ( dist ‘ 𝐺 )
legval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
legval.l ⊢ ≤ = ( ≤G ‘ 𝐺 )
legval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
legid.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
legid.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
legtrd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
legtrd.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
legbtwn.1 ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) )
legbtwn.2 ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) ≤ ( 𝐶 − 𝐵 ) )
Assertion legbtwn ( 𝜑 → 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) )

Proof

Step Hyp Ref Expression
1 legval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 legval.d ⊢ − = ( dist ‘ 𝐺 )
3 legval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 legval.l ⊢ ≤ = ( ≤G ‘ 𝐺 )
5 legval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 legid.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 legid.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 legtrd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9 legtrd.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
10 legbtwn.1 ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) )
11 legbtwn.2 ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) ≤ ( 𝐶 − 𝐵 ) )
12 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) → 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) )
13 5 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐺 ∈ TarskiG )
14 6 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐴 ∈ 𝑃 )
15 7 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐵 ∈ 𝑃 )
16 8 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐶 ∈ 𝑃 )
17 simpr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) )
18 1 2 3 13 16 15 14 17 tgbtwncom ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
19 1 2 3 13 15 16 tgbtwntriv1 ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐵 ∈ ( 𝐵 𝐼 𝐶 ) )
20 11 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → ( 𝐶 − 𝐴 ) ≤ ( 𝐶 − 𝐵 ) )
21 1 2 3 4 13 16 15 14 17 btwnleg ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → ( 𝐶 − 𝐵 ) ≤ ( 𝐶 − 𝐴 ) )
22 1 2 3 4 13 16 14 16 15 20 21 legtri3 ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → ( 𝐶 − 𝐴 ) = ( 𝐶 − 𝐵 ) )
23 1 2 3 13 16 14 16 15 22 tgcgrcomlr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → ( 𝐴 − 𝐶 ) = ( 𝐵 − 𝐶 ) )
24 eqidd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → ( 𝐵 − 𝐶 ) = ( 𝐵 − 𝐶 ) )
25 1 2 3 13 14 15 16 15 15 16 18 19 23 24 tgcgrsub ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → ( 𝐴 − 𝐵 ) = ( 𝐵 − 𝐵 ) )
26 1 2 3 13 14 15 15 25 axtgcgrid ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐴 = 𝐵 )
27 26 17 eqeltrd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐴 ∈ ( 𝐶 𝐼 𝐴 ) )
28 26 oveq2d ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → ( 𝐶 𝐼 𝐴 ) = ( 𝐶 𝐼 𝐵 ) )
29 27 28 eleqtrd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) )
30 12 29 10 mpjaodan ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) )