hltr

Description: The half-line relation is transitive. Theorem 6.7 of Schwabhauser p. 44. (Contributed by Thierry Arnoux, 23-Feb-2020)

	Ref	Expression
Hypotheses	ishlg.p	$⊢ P = {Base}_{G}$
	ishlg.i	$⊢ I = Itv (G)$
	ishlg.k	$⊢ K = {hl}_{𝒢} (G)$
	ishlg.a	$⊢ φ \to A \in P$
	ishlg.b	$⊢ φ \to B \in P$
	ishlg.c	$⊢ φ \to C \in P$
	hlln.1	$⊢ φ \to G \in 𝒢_{Tarski}$
	hltr.d	$⊢ φ \to D \in P$
	hltr.1	$⊢ φ \to A K (D) B$
	hltr.2	$⊢ φ \to B K (D) C$
Assertion	hltr	$⊢ φ \to A K (D) C$

Proof

Step	Hyp	Ref	Expression
1		ishlg.p	$⊢ P = {Base}_{G}$
2		ishlg.i	$⊢ I = Itv (G)$
3		ishlg.k	$⊢ K = {hl}_{𝒢} (G)$
4		ishlg.a	$⊢ φ \to A \in P$
5		ishlg.b	$⊢ φ \to B \in P$
6		ishlg.c	$⊢ φ \to C \in P$
7		hlln.1	$⊢ φ \to G \in 𝒢_{Tarski}$
8		hltr.d	$⊢ φ \to D \in P$
9		hltr.1	$⊢ φ \to A K (D) B$
10		hltr.2	$⊢ φ \to B K (D) C$
11	1 2 3 4 5 8 7 9	hlne1	$⊢ φ \to A \neq D$
12	1 2 3 5 6 8 7 10	hlne2	$⊢ φ \to C \neq D$
13		eqid	$⊢ dist (G) = dist (G)$
14	7	ad2antrr	$⊢ ((φ \land A \in (D I B)) \land B \in (D I C)) \to G \in 𝒢_{Tarski}$
15	8	ad2antrr	$⊢ ((φ \land A \in (D I B)) \land B \in (D I C)) \to D \in P$
16	4	ad2antrr	$⊢ ((φ \land A \in (D I B)) \land B \in (D I C)) \to A \in P$
17	5	ad2antrr	$⊢ ((φ \land A \in (D I B)) \land B \in (D I C)) \to B \in P$
18	6	ad2antrr	$⊢ ((φ \land A \in (D I B)) \land B \in (D I C)) \to C \in P$
19		simplr	$⊢ ((φ \land A \in (D I B)) \land B \in (D I C)) \to A \in (D I B)$
20		simpr	$⊢ ((φ \land A \in (D I B)) \land B \in (D I C)) \to B \in (D I C)$
21	1 13 2 14 15 16 17 18 19 20	tgbtwnexch	$⊢ ((φ \land A \in (D I B)) \land B \in (D I C)) \to A \in (D I C)$
22	21	orcd	$⊢ ((φ \land A \in (D I B)) \land B \in (D I C)) \to (A \in (D I C) \lor C \in (D I A))$
23	7	ad2antrr	$⊢ ((φ \land A \in (D I B)) \land C \in (D I B)) \to G \in 𝒢_{Tarski}$
24	8	ad2antrr	$⊢ ((φ \land A \in (D I B)) \land C \in (D I B)) \to D \in P$
25	4	ad2antrr	$⊢ ((φ \land A \in (D I B)) \land C \in (D I B)) \to A \in P$
26	6	ad2antrr	$⊢ ((φ \land A \in (D I B)) \land C \in (D I B)) \to C \in P$
27	5	ad2antrr	$⊢ ((φ \land A \in (D I B)) \land C \in (D I B)) \to B \in P$
28		simplr	$⊢ ((φ \land A \in (D I B)) \land C \in (D I B)) \to A \in (D I B)$
29		simpr	$⊢ ((φ \land A \in (D I B)) \land C \in (D I B)) \to C \in (D I B)$
30	1 2 23 24 25 26 27 28 29	tgbtwnconn3	$⊢ ((φ \land A \in (D I B)) \land C \in (D I B)) \to (A \in (D I C) \lor C \in (D I A))$
31	1 2 3 5 6 8 7	ishlg	$⊢ φ \to (B K (D) C \leftrightarrow (B \neq D \land C \neq D \land (B \in (D I C) \lor C \in (D I B))))$
32	10 31	mpbid	$⊢ φ \to (B \neq D \land C \neq D \land (B \in (D I C) \lor C \in (D I B)))$
33	32	simp3d	$⊢ φ \to (B \in (D I C) \lor C \in (D I B))$
34	33	adantr	$⊢ (φ \land A \in (D I B)) \to (B \in (D I C) \lor C \in (D I B))$
35	22 30 34	mpjaodan	$⊢ (φ \land A \in (D I B)) \to (A \in (D I C) \lor C \in (D I A))$
36	7	ad2antrr	$⊢ ((φ \land B \in (D I A)) \land B \in (D I C)) \to G \in 𝒢_{Tarski}$
37	8	ad2antrr	$⊢ ((φ \land B \in (D I A)) \land B \in (D I C)) \to D \in P$
38	5	ad2antrr	$⊢ ((φ \land B \in (D I A)) \land B \in (D I C)) \to B \in P$
39	4	ad2antrr	$⊢ ((φ \land B \in (D I A)) \land B \in (D I C)) \to A \in P$
40	6	ad2antrr	$⊢ ((φ \land B \in (D I A)) \land B \in (D I C)) \to C \in P$
41	32	simp1d	$⊢ φ \to B \neq D$
42	41	necomd	$⊢ φ \to D \neq B$
43	42	ad2antrr	$⊢ ((φ \land B \in (D I A)) \land B \in (D I C)) \to D \neq B$
44		simplr	$⊢ ((φ \land B \in (D I A)) \land B \in (D I C)) \to B \in (D I A)$
45		simpr	$⊢ ((φ \land B \in (D I A)) \land B \in (D I C)) \to B \in (D I C)$
46	1 2 36 37 38 39 40 43 44 45	tgbtwnconn1	$⊢ ((φ \land B \in (D I A)) \land B \in (D I C)) \to (A \in (D I C) \lor C \in (D I A))$
47	7	ad2antrr	$⊢ ((φ \land B \in (D I A)) \land C \in (D I B)) \to G \in 𝒢_{Tarski}$
48	8	ad2antrr	$⊢ ((φ \land B \in (D I A)) \land C \in (D I B)) \to D \in P$
49	6	ad2antrr	$⊢ ((φ \land B \in (D I A)) \land C \in (D I B)) \to C \in P$
50	5	ad2antrr	$⊢ ((φ \land B \in (D I A)) \land C \in (D I B)) \to B \in P$
51	4	ad2antrr	$⊢ ((φ \land B \in (D I A)) \land C \in (D I B)) \to A \in P$
52		simpr	$⊢ ((φ \land B \in (D I A)) \land C \in (D I B)) \to C \in (D I B)$
53		simplr	$⊢ ((φ \land B \in (D I A)) \land C \in (D I B)) \to B \in (D I A)$
54	1 13 2 47 48 49 50 51 52 53	tgbtwnexch	$⊢ ((φ \land B \in (D I A)) \land C \in (D I B)) \to C \in (D I A)$
55	54	olcd	$⊢ ((φ \land B \in (D I A)) \land C \in (D I B)) \to (A \in (D I C) \lor C \in (D I A))$
56	33	adantr	$⊢ (φ \land B \in (D I A)) \to (B \in (D I C) \lor C \in (D I B))$
57	46 55 56	mpjaodan	$⊢ (φ \land B \in (D I A)) \to (A \in (D I C) \lor C \in (D I A))$
58	1 2 3 4 5 8 7	ishlg	$⊢ φ \to (A K (D) B \leftrightarrow (A \neq D \land B \neq D \land (A \in (D I B) \lor B \in (D I A))))$
59	9 58	mpbid	$⊢ φ \to (A \neq D \land B \neq D \land (A \in (D I B) \lor B \in (D I A)))$
60	59	simp3d	$⊢ φ \to (A \in (D I B) \lor B \in (D I A))$
61	35 57 60	mpjaodan	$⊢ φ \to (A \in (D I C) \lor C \in (D I A))$
62	1 2 3 4 6 8 7	ishlg	$⊢ φ \to (A K (D) C \leftrightarrow (A \neq D \land C \neq D \land (A \in (D I C) \lor C \in (D I A))))$
63	11 12 61 62	mpbir3and	$⊢ φ \to A K (D) C$

Metamath Proof Explorer

Theorem hltr

Proof