tgbtwnouttr2

Description: Outer transitivity law for betweenness. Left-hand side of Theorem 3.7 of Schwabhauser p. 30. (Contributed by Thierry Arnoux, 18-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$
	tgbtwnouttr2.1	$⊢ φ \to B \neq C$
	tgbtwnouttr2.2	$⊢ φ \to B \in (A I C)$
	tgbtwnouttr2.3	$⊢ φ \to C \in (B I D)$
Assertion	tgbtwnouttr2	$⊢ φ \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		tgbtwnouttr2.1	$⊢ φ \to B \neq C$
10		tgbtwnouttr2.2	$⊢ φ \to B \in (A I C)$
11		tgbtwnouttr2.3	$⊢ φ \to C \in (B I D)$
12		simprl	$⊢ ((φ \land x \in P) \land (C \in (A I x) \land C \underset{˙}{-} x = C \underset{˙}{-} D)) \to C \in (A I x)$
13	4	ad2antrr	$⊢ ((φ \land x \in P) \land (C \in (A I x) \land C \underset{˙}{-} x = C \underset{˙}{-} D)) \to G \in 𝒢_{Tarski}$
14	7	ad2antrr	$⊢ ((φ \land x \in P) \land (C \in (A I x) \land C \underset{˙}{-} x = C \underset{˙}{-} D)) \to C \in P$
15	8	ad2antrr	$⊢ ((φ \land x \in P) \land (C \in (A I x) \land C \underset{˙}{-} x = C \underset{˙}{-} D)) \to D \in P$
16	6	ad2antrr	$⊢ ((φ \land x \in P) \land (C \in (A I x) \land C \underset{˙}{-} x = C \underset{˙}{-} D)) \to B \in P$
17		simplr	$⊢ ((φ \land x \in P) \land (C \in (A I x) \land C \underset{˙}{-} x = C \underset{˙}{-} D)) \to x \in P$
18	9	ad2antrr	$⊢ ((φ \land x \in P) \land (C \in (A I x) \land C \underset{˙}{-} x = C \underset{˙}{-} D)) \to B \neq C$
19	5	ad2antrr	$⊢ ((φ \land x \in P) \land (C \in (A I x) \land C \underset{˙}{-} x = C \underset{˙}{-} D)) \to A \in P$
20	10	ad2antrr	$⊢ ((φ \land x \in P) \land (C \in (A I x) \land C \underset{˙}{-} x = C \underset{˙}{-} D)) \to B \in (A I C)$
21	1 2 3 13 19 16 14 17 20 12	tgbtwnexch3	$⊢ ((φ \land x \in P) \land (C \in (A I x) \land C \underset{˙}{-} x = C \underset{˙}{-} D)) \to C \in (B I x)$
22	11	ad2antrr	$⊢ ((φ \land x \in P) \land (C \in (A I x) \land C \underset{˙}{-} x = C \underset{˙}{-} D)) \to C \in (B I D)$
23		simprr	$⊢ ((φ \land x \in P) \land (C \in (A I x) \land C \underset{˙}{-} x = C \underset{˙}{-} D)) \to C \underset{˙}{-} x = C \underset{˙}{-} D$
24		eqidd	$⊢ ((φ \land x \in P) \land (C \in (A I x) \land C \underset{˙}{-} x = C \underset{˙}{-} D)) \to C \underset{˙}{-} D = C \underset{˙}{-} D$
25	1 2 3 13 14 14 15 16 17 15 18 21 22 23 24	tgsegconeq	$⊢ ((φ \land x \in P) \land (C \in (A I x) \land C \underset{˙}{-} x = C \underset{˙}{-} D)) \to x = D$
26	25	oveq2d	$⊢ ((φ \land x \in P) \land (C \in (A I x) \land C \underset{˙}{-} x = C \underset{˙}{-} D)) \to A I x = A I D$
27	12 26	eleqtrd	$⊢ ((φ \land x \in P) \land (C \in (A I x) \land C \underset{˙}{-} x = C \underset{˙}{-} D)) \to C \in (A I D)$
28	1 2 3 4 5 7 7 8	axtgsegcon	$⊢ φ \to \exists x \in P (C \in (A I x) \land C \underset{˙}{-} x = C \underset{˙}{-} D)$
29	27 28	r19.29a	$⊢ φ \to C \in (A I D)$

Metamath Proof Explorer

Theorem tgbtwnouttr2

Proof