tgbtwncom

Description: Betweenness commutes. Theorem 3.2 of Schwabhauser p. 30. (Contributed by Thierry Arnoux, 15-Mar-2019)

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		tgbtwntriv2.1	$⊢ φ \to A \in P$
6		tgbtwntriv2.2	$⊢ φ \to B \in P$
7		tgbtwncom.3	$⊢ φ \to C \in P$
8		tgbtwncom.4	$⊢ φ \to B \in (A I C)$
9	4	ad2antrr	$⊢ ((φ \land x \in P) \land (x \in (B I B) \land x \in (C I A))) \to G \in 𝒢_{Tarski}$
10	6	ad2antrr	$⊢ ((φ \land x \in P) \land (x \in (B I B) \land x \in (C I A))) \to B \in P$
11		simplr	$⊢ ((φ \land x \in P) \land (x \in (B I B) \land x \in (C I A))) \to x \in P$
12		simprl	$⊢ ((φ \land x \in P) \land (x \in (B I B) \land x \in (C I A))) \to x \in (B I B)$
13	1 2 3 9 10 11 12	axtgbtwnid	$⊢ ((φ \land x \in P) \land (x \in (B I B) \land x \in (C I A))) \to B = x$
14		simprr	$⊢ ((φ \land x \in P) \land (x \in (B I B) \land x \in (C I A))) \to x \in (C I A)$
15	13 14	eqeltrd	$⊢ ((φ \land x \in P) \land (x \in (B I B) \land x \in (C I A))) \to B \in (C I A)$
16	1 2 3 4 6 7	tgbtwntriv2	$⊢ φ \to C \in (B I C)$
17	1 2 3 4 5 6 7 6 7 8 16	axtgpasch	$⊢ φ \to \exists x \in P (x \in (B I B) \land x \in (C I A))$
18	15 17	r19.29a	$⊢ φ \to B \in (C I A)$

Metamath Proof Explorer