tgaasncol

Description: Slide a non-collinearity along the line it is off: if X is off line Y Z and W is a point of that line other than Z , then X is off line Z W too. Lines Z Y and Z W coincide ( tglineeltr ), which is what the exterior-angle hypothesis of tgaasexc needs at the moving point. (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	tgaasncol.p	$⊢ P = {Base}_{G}$
	tgaasncol.i	$⊢ I = Itv (G)$
	tgaasncol.l	$⊢ L = {Line}_{𝒢} (G)$
	tgaasncol.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgaasncol.x	$⊢ φ \to X \in P$
	tgaasncol.y	$⊢ φ \to Y \in P$
	tgaasncol.z	$⊢ φ \to Z \in P$
	tgaasncol.w	$⊢ φ \to W \in P$
	tgaasncol.1	$⊢ φ \to \neg (X \in (Y L Z) \lor Y = Z)$
	tgaasncol.2	$⊢ φ \to (W \in (Z L Y) \lor Z = Y)$
	tgaasncol.3	$⊢ φ \to W \neq Z$
Assertion	tgaasncol	$⊢ φ \to \neg (X \in (Z L W) \lor Z = W)$

Proof

Step	Hyp	Ref	Expression
1		tgaasncol.p	$⊢ P = {Base}_{G}$
2		tgaasncol.i	$⊢ I = Itv (G)$
3		tgaasncol.l	$⊢ L = {Line}_{𝒢} (G)$
4		tgaasncol.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tgaasncol.x	$⊢ φ \to X \in P$
6		tgaasncol.y	$⊢ φ \to Y \in P$
7		tgaasncol.z	$⊢ φ \to Z \in P$
8		tgaasncol.w	$⊢ φ \to W \in P$
9		tgaasncol.1	$⊢ φ \to \neg (X \in (Y L Z) \lor Y = Z)$
10		tgaasncol.2	$⊢ φ \to (W \in (Z L Y) \lor Z = Y)$
11		tgaasncol.3	$⊢ φ \to W \neq Z$
12	1 3 2 4 6 7 5 9	ncolcom	$⊢ φ \to \neg (X \in (Z L Y) \lor Z = Y)$
13	4	adantr	$⊢ (φ \land (X \in (Z L W) \lor Z = W)) \to G \in 𝒢_{Tarski}$
14	7	adantr	$⊢ (φ \land (X \in (Z L W) \lor Z = W)) \to Z \in P$
15	6	adantr	$⊢ (φ \land (X \in (Z L W) \lor Z = W)) \to Y \in P$
16	1 3 2 4 6 7 5 9	ncolrot1	$⊢ φ \to \neg (Y \in (Z L X) \lor Z = X)$
17	1 2 3 4 6 7 5 16	ncolne1	$⊢ φ \to Y \neq Z$
18	17	necomd	$⊢ φ \to Z \neq Y$
19	18	adantr	$⊢ (φ \land (X \in (Z L W) \lor Z = W)) \to Z \neq Y$
20	8	adantr	$⊢ (φ \land (X \in (Z L W) \lor Z = W)) \to W \in P$
21	11	adantr	$⊢ (φ \land (X \in (Z L W) \lor Z = W)) \to W \neq Z$
22	18	neneqd	$⊢ φ \to \neg Z = Y$
23	10 22	olcnd	$⊢ φ \to W \in (Z L Y)$
24	23	adantr	$⊢ (φ \land (X \in (Z L W) \lor Z = W)) \to W \in (Z L Y)$
25	5	adantr	$⊢ (φ \land (X \in (Z L W) \lor Z = W)) \to X \in P$
26		simpr	$⊢ (φ \land (X \in (Z L W) \lor Z = W)) \to (X \in (Z L W) \lor Z = W)$
27	21	necomd	$⊢ (φ \land (X \in (Z L W) \lor Z = W)) \to Z \neq W$
28	27	neneqd	$⊢ (φ \land (X \in (Z L W) \lor Z = W)) \to \neg Z = W$
29	26 28	olcnd	$⊢ (φ \land (X \in (Z L W) \lor Z = W)) \to X \in (Z L W)$
30	1 2 3 13 14 15 19 20 21 24 25 29	tglineeltr	$⊢ (φ \land (X \in (Z L W) \lor Z = W)) \to X \in (Z L Y)$
31	30	orcd	$⊢ (φ \land (X \in (Z L W) \lor Z = W)) \to (X \in (Z L Y) \lor Z = Y)$
32	12 31	mtand	$⊢ φ \to \neg (X \in (Z L W) \lor Z = W)$

Metamath Proof Explorer

Theorem tgaasncol

Proof