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	$⊢ P = {Base}_{G}$
	legval.d	$⊢ \underset{˙}{-} = dist (G)$
	legval.i	$⊢ I = Itv (G)$
	legval.l	$⊢ \underset{˙}{\leq} = \leq_{𝒢} (G)$
	legval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	legid.a	$⊢ φ \to A \in P$
	legid.b	$⊢ φ \to B \in P$
	legtrd.c	$⊢ φ \to C \in P$
	legtrd.d	$⊢ φ \to D \in P$
	legbtwn.1	$⊢ φ \to (A \in (C I B) \lor B \in (C I A))$
	legbtwn.2	$⊢ φ \to (C \underset{˙}{-} A) \underset{˙}{\leq} (C \underset{˙}{-} B)$
Assertion	legbtwn	$⊢ φ \to A \in (C I B)$

Proof

Step	Hyp	Ref	Expression
1		legval.p	$⊢ P = {Base}_{G}$
2		legval.d	$⊢ \underset{˙}{-} = dist (G)$
3		legval.i	$⊢ I = Itv (G)$
4		legval.l	$⊢ \underset{˙}{\leq} = \leq_{𝒢} (G)$
5		legval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		legid.a	$⊢ φ \to A \in P$
7		legid.b	$⊢ φ \to B \in P$
8		legtrd.c	$⊢ φ \to C \in P$
9		legtrd.d	$⊢ φ \to D \in P$
10		legbtwn.1	$⊢ φ \to (A \in (C I B) \lor B \in (C I A))$
11		legbtwn.2	$⊢ φ \to (C \underset{˙}{-} A) \underset{˙}{\leq} (C \underset{˙}{-} B)$
12		simpr	$⊢ (φ \land A \in (C I B)) \to A \in (C I B)$
13	5	adantr	$⊢ (φ \land B \in (C I A)) \to G \in 𝒢_{Tarski}$
14	6	adantr	$⊢ (φ \land B \in (C I A)) \to A \in P$
15	7	adantr	$⊢ (φ \land B \in (C I A)) \to B \in P$
16	8	adantr	$⊢ (φ \land B \in (C I A)) \to C \in P$
17		simpr	$⊢ (φ \land B \in (C I A)) \to B \in (C I A)$
18	1 2 3 13 16 15 14 17	tgbtwncom	$⊢ (φ \land B \in (C I A)) \to B \in (A I C)$
19	1 2 3 13 15 16	tgbtwntriv1	$⊢ (φ \land B \in (C I A)) \to B \in (B I C)$
20	11	adantr	$⊢ (φ \land B \in (C I A)) \to (C \underset{˙}{-} A) \underset{˙}{\leq} (C \underset{˙}{-} B)$
21	1 2 3 4 13 16 15 14 17	btwnleg	$⊢ (φ \land B \in (C I A)) \to (C \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} A)$
22	1 2 3 4 13 16 14 16 15 20 21	legtri3	$⊢ (φ \land B \in (C I A)) \to C \underset{˙}{-} A = C \underset{˙}{-} B$
23	1 2 3 13 16 14 16 15 22	tgcgrcomlr	$⊢ (φ \land B \in (C I A)) \to A \underset{˙}{-} C = B \underset{˙}{-} C$
24		eqidd	$⊢ (φ \land B \in (C I A)) \to B \underset{˙}{-} C = B \underset{˙}{-} C$
25	1 2 3 13 14 15 16 15 15 16 18 19 23 24	tgcgrsub	$⊢ (φ \land B \in (C I A)) \to A \underset{˙}{-} B = B \underset{˙}{-} B$
26	1 2 3 13 14 15 15 25	axtgcgrid	$⊢ (φ \land B \in (C I A)) \to A = B$
27	26 17	eqeltrd	$⊢ (φ \land B \in (C I A)) \to A \in (C I A)$
28	26	oveq2d	$⊢ (φ \land B \in (C I A)) \to C I A = C I B$
29	27 28	eleqtrd	$⊢ (φ \land B \in (C I A)) \to A \in (C I B)$
30	12 29 10	mpjaodan	$⊢ φ \to A \in (C I B)$

Metamath Proof Explorer

Theorem legbtwn

Proof