hlbtwn

Description: Betweenness is a sufficient condition to swap half-lines. (Contributed by Thierry Arnoux, 21-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$
	hlbtwn.1	$⊢ φ \to D \in (C I B)$
	hlbtwn.2	$⊢ φ \to B \neq C$
	hlbtwn.3	$⊢ φ \to D \neq C$
Assertion	hlbtwn	$⊢ φ \to (A K (C) B \leftrightarrow A K (C) D)$

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		hlbtwn.1	$⊢ φ \to D \in (C I B)$
10		hlbtwn.2	$⊢ φ \to B \neq C$
11		hlbtwn.3	$⊢ φ \to D \neq C$
12	10 11	2thd	$⊢ φ \to (B \neq C \leftrightarrow D \neq C)$
13	7	adantr	$⊢ (φ \land A \in (C I B)) \to G \in 𝒢_{Tarski}$
14	6	adantr	$⊢ (φ \land A \in (C I B)) \to C \in P$
15	4	adantr	$⊢ (φ \land A \in (C I B)) \to A \in P$
16	8	adantr	$⊢ (φ \land A \in (C I B)) \to D \in P$
17	5	adantr	$⊢ (φ \land A \in (C I B)) \to B \in P$
18		simpr	$⊢ (φ \land A \in (C I B)) \to A \in (C I B)$
19	9	adantr	$⊢ (φ \land A \in (C I B)) \to D \in (C I B)$
20	1 2 13 14 15 16 17 18 19	tgbtwnconn3	$⊢ (φ \land A \in (C I B)) \to (A \in (C I D) \lor D \in (C I A))$
21		eqid	$⊢ dist (G) = dist (G)$
22	7	adantr	$⊢ (φ \land B \in (C I A)) \to G \in 𝒢_{Tarski}$
23	6	adantr	$⊢ (φ \land B \in (C I A)) \to C \in P$
24	8	adantr	$⊢ (φ \land B \in (C I A)) \to D \in P$
25	5	adantr	$⊢ (φ \land B \in (C I A)) \to B \in P$
26	4	adantr	$⊢ (φ \land B \in (C I A)) \to A \in P$
27	9	adantr	$⊢ (φ \land B \in (C I A)) \to D \in (C I B)$
28		simpr	$⊢ (φ \land B \in (C I A)) \to B \in (C I A)$
29	1 21 2 22 23 24 25 26 27 28	tgbtwnexch	$⊢ (φ \land B \in (C I A)) \to D \in (C I A)$
30	29	olcd	$⊢ (φ \land B \in (C I A)) \to (A \in (C I D) \lor D \in (C I A))$
31	20 30	jaodan	$⊢ (φ \land (A \in (C I B) \lor B \in (C I A))) \to (A \in (C I D) \lor D \in (C I A))$
32	7	adantr	$⊢ (φ \land A \in (C I D)) \to G \in 𝒢_{Tarski}$
33	6	adantr	$⊢ (φ \land A \in (C I D)) \to C \in P$
34	4	adantr	$⊢ (φ \land A \in (C I D)) \to A \in P$
35	8	adantr	$⊢ (φ \land A \in (C I D)) \to D \in P$
36	5	adantr	$⊢ (φ \land A \in (C I D)) \to B \in P$
37		simpr	$⊢ (φ \land A \in (C I D)) \to A \in (C I D)$
38	9	adantr	$⊢ (φ \land A \in (C I D)) \to D \in (C I B)$
39	1 21 2 32 33 34 35 36 37 38	tgbtwnexch	$⊢ (φ \land A \in (C I D)) \to A \in (C I B)$
40	39	orcd	$⊢ (φ \land A \in (C I D)) \to (A \in (C I B) \lor B \in (C I A))$
41	7	adantr	$⊢ (φ \land D \in (C I A)) \to G \in 𝒢_{Tarski}$
42	6	adantr	$⊢ (φ \land D \in (C I A)) \to C \in P$
43	8	adantr	$⊢ (φ \land D \in (C I A)) \to D \in P$
44	4	adantr	$⊢ (φ \land D \in (C I A)) \to A \in P$
45	5	adantr	$⊢ (φ \land D \in (C I A)) \to B \in P$
46	11	necomd	$⊢ φ \to C \neq D$
47	46	adantr	$⊢ (φ \land D \in (C I A)) \to C \neq D$
48		simpr	$⊢ (φ \land D \in (C I A)) \to D \in (C I A)$
49	9	adantr	$⊢ (φ \land D \in (C I A)) \to D \in (C I B)$
50	1 2 41 42 43 44 45 47 48 49	tgbtwnconn1	$⊢ (φ \land D \in (C I A)) \to (A \in (C I B) \lor B \in (C I A))$
51	40 50	jaodan	$⊢ (φ \land (A \in (C I D) \lor D \in (C I A))) \to (A \in (C I B) \lor B \in (C I A))$
52	31 51	impbida	$⊢ φ \to ((A \in (C I B) \lor B \in (C I A)) \leftrightarrow (A \in (C I D) \lor D \in (C I A)))$
53	12 52	3anbi23d	$⊢ φ \to ((A \neq C \land B \neq C \land (A \in (C I B) \lor B \in (C I A))) \leftrightarrow (A \neq C \land D \neq C \land (A \in (C I D) \lor D \in (C I A))))$
54	1 2 3 4 5 6 7	ishlg	$⊢ φ \to (A K (C) B \leftrightarrow (A \neq C \land B \neq C \land (A \in (C I B) \lor B \in (C I A))))$
55	1 2 3 4 8 6 7	ishlg	$⊢ φ \to (A K (C) D \leftrightarrow (A \neq C \land D \neq C \land (A \in (C I D) \lor D \in (C I A))))$
56	53 54 55	3bitr4d	$⊢ φ \to (A K (C) B \leftrightarrow A K (C) D)$

Metamath Proof Explorer

Theorem hlbtwn

Proof