Theorem btwnleg

Description: Betweenness implies less-than relation. (Contributed by Thierry Arnoux, 3-Jul-2019)

	Ref	Expression
Hypotheses	legval.p	|- P = ( Base ` G )
	legval.d	|- .- = ( dist ` G )
	legval.i	|- I = ( Itv ` G )
	legval.l	|- .<_ = ( leG ` G )
	legval.g	|- ( ph -> G e. TarskiG )
	legid.a	|- ( ph -> A e. P )
	legid.b	|- ( ph -> B e. P )
	legtrd.c	|- ( ph -> C e. P )
	btwnleg.1	|- ( ph -> B e. ( A I C ) )
Assertion	btwnleg	|- ( ph -> ( A .- B ) .<_ ( A .- C ) )

Proof

Step	Hyp	Ref	Expression
1		legval.p	|- P = ( Base ` G )
2		legval.d	|- .- = ( dist ` G )
3		legval.i	|- I = ( Itv ` G )
4		legval.l	|- .<_ = ( leG ` G )
5		legval.g	|- ( ph -> G e. TarskiG )
6		legid.a	|- ( ph -> A e. P )
7		legid.b	|- ( ph -> B e. P )
8		legtrd.c	|- ( ph -> C e. P )
9		btwnleg.1	|- ( ph -> B e. ( A I C ) )
10		eqidd	|- ( ph -> ( A .- B ) = ( A .- B ) )
11		eleq1	|- ( x = B -> ( x e. ( A I C ) <-> B e. ( A I C ) ) )
12		oveq2	|- ( x = B -> ( A .- x ) = ( A .- B ) )
13	12	eqeq2d	|- ( x = B -> ( ( A .- B ) = ( A .- x ) <-> ( A .- B ) = ( A .- B ) ) )
14	11 13	anbi12d	|- ( x = B -> ( ( x e. ( A I C ) /\ ( A .- B ) = ( A .- x ) ) <-> ( B e. ( A I C ) /\ ( A .- B ) = ( A .- B ) ) ) )
15	14	rspcev	|- ( ( B e. P /\ ( B e. ( A I C ) /\ ( A .- B ) = ( A .- B ) ) ) -> E. x e. P ( x e. ( A I C ) /\ ( A .- B ) = ( A .- x ) ) )
16	7 9 10 15	syl12anc	|- ( ph -> E. x e. P ( x e. ( A I C ) /\ ( A .- B ) = ( A .- x ) ) )
17	1 2 3 4 5 6 7 6 8	legov	|- ( ph -> ( ( A .- B ) .<_ ( A .- C ) <-> E. x e. P ( x e. ( A I C ) /\ ( A .- B ) = ( A .- x ) ) ) )
18	16 17	mpbird	|- ( ph -> ( A .- B ) .<_ ( A .- C ) )