Theorem btwnleg

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

	Ref	Expression
Hypotheses	legval.p	$$⊢P={\mathrm{Base}}_G$$
	legval.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	legval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	legval.l	$$⊢\underset{\dot{}}{\le }={\le }_{𝒢}\left(G\right)$$
	legval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	legid.a	$$⊢\phi \to A\in P$$
	legid.b	$$⊢\phi \to B\in P$$
	legtrd.c	$$⊢\phi \to C\in P$$
	btwnleg.1	$$⊢\phi \to B\in \left(AIC\right)$$
Assertion	btwnleg	$$⊢\phi \to \left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{\le }\left(A\underset{\dot{}}{-}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		legval.p	$$⊢P={\mathrm{Base}}_G$$
2		legval.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		legval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		legval.l	$$⊢\underset{\dot{}}{\le }={\le }_{𝒢}\left(G\right)$$
5		legval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
6		legid.a	$$⊢\phi \to A\in P$$
7		legid.b	$$⊢\phi \to B\in P$$
8		legtrd.c	$$⊢\phi \to C\in P$$
9		btwnleg.1	$$⊢\phi \to B\in \left(AIC\right)$$
10		eqidd	$$⊢\phi \to A\underset{\dot{}}{-}B=A\underset{\dot{}}{-}B$$
11		eleq1	$$⊢x=B\to \left(x\in \left(AIC\right)\leftrightarrow B\in \left(AIC\right)\right)$$
12		oveq2	$$⊢x=B\to A\underset{\dot{}}{-}x=A\underset{\dot{}}{-}B$$
13	12	eqeq2d	$$⊢x=B\to \left(A\underset{\dot{}}{-}B=A\underset{\dot{}}{-}x\leftrightarrow A\underset{\dot{}}{-}B=A\underset{\dot{}}{-}B\right)$$
14	11 13	anbi12d	$$⊢x=B\to \left(\left(x\in \left(AIC\right)\wedge A\underset{\dot{}}{-}B=A\underset{\dot{}}{-}x\right)\leftrightarrow \left(B\in \left(AIC\right)\wedge A\underset{\dot{}}{-}B=A\underset{\dot{}}{-}B\right)\right)$$
15	14	rspcev	$$⊢\left(B\in P\wedge \left(B\in \left(AIC\right)\wedge A\underset{\dot{}}{-}B=A\underset{\dot{}}{-}B\right)\right)\to \exists x\in P\left(x\in \left(AIC\right)\wedge A\underset{\dot{}}{-}B=A\underset{\dot{}}{-}x\right)$$
16	7 9 10 15	syl12anc	$$⊢\phi \to \exists x\in P\left(x\in \left(AIC\right)\wedge A\underset{\dot{}}{-}B=A\underset{\dot{}}{-}x\right)$$
17	1 2 3 4 5 6 7 6 8	legov	$$⊢\phi \to \left(\left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{\le }\left(A\underset{\dot{}}{-}C\right)\leftrightarrow \exists x\in P\left(x\in \left(AIC\right)\wedge A\underset{\dot{}}{-}B=A\underset{\dot{}}{-}x\right)\right)$$
18	16 17	mpbird	$$⊢\phi \to \left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{\le }\left(A\underset{\dot{}}{-}C\right)$$