ncolcom

Description: Swapping non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019)

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		ncolrot	$⊢ φ \to \neg (Z \in (X L Y) \lor X = Y)$
9	4	adantr	$⊢ (φ \land (Z \in (Y L X) \lor Y = X)) \to G \in 𝒢_{Tarski}$
10	6	adantr	$⊢ (φ \land (Z \in (Y L X) \lor Y = X)) \to Y \in P$
11	5	adantr	$⊢ (φ \land (Z \in (Y L X) \lor Y = X)) \to X \in P$
12	7	adantr	$⊢ (φ \land (Z \in (Y L X) \lor Y = X)) \to Z \in P$
13		simpr	$⊢ (φ \land (Z \in (Y L X) \lor Y = X)) \to (Z \in (Y L X) \lor Y = X)$
14	1 2 3 9 10 11 12 13	colcom	$⊢ (φ \land (Z \in (Y L X) \lor Y = X)) \to (Z \in (X L Y) \lor X = Y)$
15	8 14	mtand	$⊢ φ \to \neg (Z \in (Y L X) \lor Y = X)$

Metamath Proof Explorer