Metamath Proof Explorer

Theorem colcom

Description: Swapping the points defining a line keeps it unchanged. Part of Theorem 4.11 of Schwabhauser p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019)

		Ref	Expression
	Hypotheses	tglngval.p	$⊢ P = {Base}_{G}$
		tglngval.l	$⊢ L = {Line}_{𝒢} (G)$
		tglngval.i	$⊢ I = Itv (G)$
		tglngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
		tglngval.x	$⊢ φ \to X \in P$
		tglngval.y	$⊢ φ \to Y \in P$
		tgcolg.z	$⊢ φ \to Z \in P$
		colrot	$⊢ φ \to (Z \in (X L Y) \lor X = Y)$
	Assertion	colcom	$⊢ φ \to (Z \in (Y L X) \lor Y = X)$

Proof

Step	Hyp	Ref	Expression
1		tglngval.p	$⊢ P = {Base}_{G}$
2		tglngval.l	$⊢ L = {Line}_{𝒢} (G)$
3		tglngval.i	$⊢ I = Itv (G)$
4		tglngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tglngval.x	$⊢ φ \to X \in P$
6		tglngval.y	$⊢ φ \to Y \in P$
7		tgcolg.z	$⊢ φ \to Z \in P$
8		colrot	$⊢ φ \to (Z \in (X L Y) \lor X = Y)$
9		3orcomb	$⊢ (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z)) \leftrightarrow (Z \in (X I Y) \lor Y \in (X I Z) \lor X \in (Z I Y))$
10		eqid	$⊢ dist (G) = dist (G)$
11	1 10 3 4 5 7 6	tgbtwncomb	$⊢ φ \to (Z \in (X I Y) \leftrightarrow Z \in (Y I X))$
12	1 10 3 4 5 6 7	tgbtwncomb	$⊢ φ \to (Y \in (X I Z) \leftrightarrow Y \in (Z I X))$
13	1 10 3 4 7 5 6	tgbtwncomb	$⊢ φ \to (X \in (Z I Y) \leftrightarrow X \in (Y I Z))$
14	11 12 13	3orbi123d	$⊢ φ \to ((Z \in (X I Y) \lor Y \in (X I Z) \lor X \in (Z I Y)) \leftrightarrow (Z \in (Y I X) \lor Y \in (Z I X) \lor X \in (Y I Z)))$
15	9 14	bitrid	$⊢ φ \to ((Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z)) \leftrightarrow (Z \in (Y I X) \lor Y \in (Z I X) \lor X \in (Y I Z)))$
16	1 2 3 4 5 6 7	tgcolg	$⊢ φ \to ((Z \in (X L Y) \lor X = Y) \leftrightarrow (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z)))$
17	1 2 3 4 6 5 7	tgcolg	$⊢ φ \to ((Z \in (Y L X) \lor Y = X) \leftrightarrow (Z \in (Y I X) \lor Y \in (Z I X) \lor X \in (Y I Z)))$
18	15 16 17	3bitr4d	$⊢ φ \to ((Z \in (X L Y) \lor X = Y) \leftrightarrow (Z \in (Y L X) \lor Y = X))$
19	8 18	mpbid	$⊢ φ \to (Z \in (Y L X) \lor Y = X)$