Metamath Proof Explorer


Theorem btwnleg

Description: Betweenness implies less-than relation. (Contributed by Thierry Arnoux, 3-Jul-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 âŠĒ ( 𝜑 → ðķ ∈ 𝑃 )
btwnleg.1 âŠĒ ( 𝜑 → ðĩ ∈ ( ðī 𝐞 ðķ ) )
Assertion btwnleg ( 𝜑 → ( ðī − ðĩ ) â‰Ī ( ðī − ðķ ) )

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 btwnleg.1 âŠĒ ( 𝜑 → ðĩ ∈ ( ðī 𝐞 ðķ ) )
10 eqidd âŠĒ ( 𝜑 → ( ðī − ðĩ ) = ( ðī − ðĩ ) )
11 eleq1 âŠĒ ( ð‘Ĩ = ðĩ → ( ð‘Ĩ ∈ ( ðī 𝐞 ðķ ) ↔ ðĩ ∈ ( ðī 𝐞 ðķ ) ) )
12 oveq2 âŠĒ ( ð‘Ĩ = ðĩ → ( ðī − ð‘Ĩ ) = ( ðī − ðĩ ) )
13 12 eqeq2d âŠĒ ( ð‘Ĩ = ðĩ → ( ( ðī − ðĩ ) = ( ðī − ð‘Ĩ ) ↔ ( ðī − ðĩ ) = ( ðī − ðĩ ) ) )
14 11 13 anbi12d âŠĒ ( ð‘Ĩ = ðĩ → ( ( ð‘Ĩ ∈ ( ðī 𝐞 ðķ ) ∧ ( ðī − ðĩ ) = ( ðī − ð‘Ĩ ) ) ↔ ( ðĩ ∈ ( ðī 𝐞 ðķ ) ∧ ( ðī − ðĩ ) = ( ðī − ðĩ ) ) ) )
15 14 rspcev âŠĒ ( ( ðĩ ∈ 𝑃 ∧ ( ðĩ ∈ ( ðī 𝐞 ðķ ) ∧ ( ðī − ðĩ ) = ( ðī − ðĩ ) ) ) → ∃ ð‘Ĩ ∈ 𝑃 ( ð‘Ĩ ∈ ( ðī 𝐞 ðķ ) ∧ ( ðī − ðĩ ) = ( ðī − ð‘Ĩ ) ) )
16 7 9 10 15 syl12anc âŠĒ ( 𝜑 → ∃ ð‘Ĩ ∈ 𝑃 ( ð‘Ĩ ∈ ( ðī 𝐞 ðķ ) ∧ ( ðī − ðĩ ) = ( ðī − ð‘Ĩ ) ) )
17 1 2 3 4 5 6 7 6 8 legov âŠĒ ( 𝜑 → ( ( ðī − ðĩ ) â‰Ī ( ðī − ðķ ) ↔ ∃ ð‘Ĩ ∈ 𝑃 ( ð‘Ĩ ∈ ( ðī 𝐞 ðķ ) ∧ ( ðī − ðĩ ) = ( ðī − ð‘Ĩ ) ) ) )
18 16 17 mpbird âŠĒ ( 𝜑 → ( ðī − ðĩ ) â‰Ī ( ðī − ðķ ) )