tgbtwnexch2

Description: Exchange the outer point of two betweenness statements. Right-hand side of Theorem 3.5 of Schwabhauser p. 30. (Contributed by Thierry Arnoux, 23-Mar-2019)

	Ref	Expression
Hypotheses	tkgeom.p	$⊢ P = {Base}_{G}$
	tkgeom.d	$⊢ \underset{˙}{-} = dist (G)$
	tkgeom.i	$⊢ I = Itv (G)$
	tkgeom.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgbtwnintr.1	$⊢ φ \to A \in P$
	tgbtwnintr.2	$⊢ φ \to B \in P$
	tgbtwnintr.3	$⊢ φ \to C \in P$
	tgbtwnintr.4	$⊢ φ \to D \in P$
	tgbtwnexch2.1	$⊢ φ \to B \in (A I D)$
	tgbtwnexch2.2	$⊢ φ \to C \in (B I D)$
Assertion	tgbtwnexch2	$⊢ φ \to C \in (A I D)$

Proof

Step	Hyp	Ref	Expression
1		tkgeom.p	$⊢ P = {Base}_{G}$
2		tkgeom.d	$⊢ \underset{˙}{-} = dist (G)$
3		tkgeom.i	$⊢ I = Itv (G)$
4		tkgeom.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tgbtwnintr.1	$⊢ φ \to A \in P$
6		tgbtwnintr.2	$⊢ φ \to B \in P$
7		tgbtwnintr.3	$⊢ φ \to C \in P$
8		tgbtwnintr.4	$⊢ φ \to D \in P$
9		tgbtwnexch2.1	$⊢ φ \to B \in (A I D)$
10		tgbtwnexch2.2	$⊢ φ \to C \in (B I D)$
11		simpr	$⊢ (φ \land B = C) \to B = C$
12	9	adantr	$⊢ (φ \land B = C) \to B \in (A I D)$
13	11 12	eqeltrrd	$⊢ (φ \land B = C) \to C \in (A I D)$
14	4	adantr	$⊢ (φ \land B \neq C) \to G \in 𝒢_{Tarski}$
15	5	adantr	$⊢ (φ \land B \neq C) \to A \in P$
16	6	adantr	$⊢ (φ \land B \neq C) \to B \in P$
17	7	adantr	$⊢ (φ \land B \neq C) \to C \in P$
18	8	adantr	$⊢ (φ \land B \neq C) \to D \in P$
19		simpr	$⊢ (φ \land B \neq C) \to B \neq C$
20	10	adantr	$⊢ (φ \land B \neq C) \to C \in (B I D)$
21	9	adantr	$⊢ (φ \land B \neq C) \to B \in (A I D)$
22	1 2 3 14 17 16 15 18 20 21	tgbtwnintr	$⊢ (φ \land B \neq C) \to B \in (C I A)$
23	1 2 3 14 17 16 15 22	tgbtwncom	$⊢ (φ \land B \neq C) \to B \in (A I C)$
24	1 2 3 14 15 16 17 18 19 23 20	tgbtwnouttr2	$⊢ (φ \land B \neq C) \to C \in (A I D)$
25	13 24	pm2.61dane	$⊢ φ \to C \in (A I D)$

Metamath Proof Explorer

Theorem tgbtwnexch2

Proof