Theorem 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 = ( LineG ` G )
	tgaasncol.g	|- ( ph -> G e. TarskiG )
	tgaasncol.x	|- ( ph -> X e. P )
	tgaasncol.y	|- ( ph -> Y e. P )
	tgaasncol.z	|- ( ph -> Z e. P )
	tgaasncol.w	|- ( ph -> W e. P )
	tgaasncol.1	|- ( ph -> -. ( X e. ( Y L Z ) \/ Y = Z ) )
	tgaasncol.2	|- ( ph -> ( W e. ( Z L Y ) \/ Z = Y ) )
	tgaasncol.3	|- ( ph -> W =/= Z )
Assertion	tgaasncol	|- ( ph -> -. ( X e. ( Z L W ) \/ Z = W ) )

Proof

Step	Hyp	Ref	Expression
1		tgaasncol.p	|- P = ( Base ` G )
2		tgaasncol.i	|- I = ( Itv ` G )
3		tgaasncol.l	|- L = ( LineG ` G )
4		tgaasncol.g	|- ( ph -> G e. TarskiG )
5		tgaasncol.x	|- ( ph -> X e. P )
6		tgaasncol.y	|- ( ph -> Y e. P )
7		tgaasncol.z	|- ( ph -> Z e. P )
8		tgaasncol.w	|- ( ph -> W e. P )
9		tgaasncol.1	|- ( ph -> -. ( X e. ( Y L Z ) \/ Y = Z ) )
10		tgaasncol.2	|- ( ph -> ( W e. ( Z L Y ) \/ Z = Y ) )
11		tgaasncol.3	|- ( ph -> W =/= Z )
12	1 3 2 4 6 7 5 9	ncolcom	|- ( ph -> -. ( X e. ( Z L Y ) \/ Z = Y ) )
13	4	adantr	|- ( ( ph /\ ( X e. ( Z L W ) \/ Z = W ) ) -> G e. TarskiG )
14	7	adantr	|- ( ( ph /\ ( X e. ( Z L W ) \/ Z = W ) ) -> Z e. P )
15	6	adantr	|- ( ( ph /\ ( X e. ( Z L W ) \/ Z = W ) ) -> Y e. P )
16	1 3 2 4 6 7 5 9	ncolrot1	|- ( ph -> -. ( Y e. ( Z L X ) \/ Z = X ) )
17	1 2 3 4 6 7 5 16	ncolne1	|- ( ph -> Y =/= Z )
18	17	necomd	|- ( ph -> Z =/= Y )
19	18	adantr	|- ( ( ph /\ ( X e. ( Z L W ) \/ Z = W ) ) -> Z =/= Y )
20	8	adantr	|- ( ( ph /\ ( X e. ( Z L W ) \/ Z = W ) ) -> W e. P )
21	11	adantr	|- ( ( ph /\ ( X e. ( Z L W ) \/ Z = W ) ) -> W =/= Z )
22	18	neneqd	|- ( ph -> -. Z = Y )
23	10 22	olcnd	|- ( ph -> W e. ( Z L Y ) )
24	23	adantr	|- ( ( ph /\ ( X e. ( Z L W ) \/ Z = W ) ) -> W e. ( Z L Y ) )
25	5	adantr	|- ( ( ph /\ ( X e. ( Z L W ) \/ Z = W ) ) -> X e. P )
26		simpr	|- ( ( ph /\ ( X e. ( Z L W ) \/ Z = W ) ) -> ( X e. ( Z L W ) \/ Z = W ) )
27	21	necomd	|- ( ( ph /\ ( X e. ( Z L W ) \/ Z = W ) ) -> Z =/= W )
28	27	neneqd	|- ( ( ph /\ ( X e. ( Z L W ) \/ Z = W ) ) -> -. Z = W )
29	26 28	olcnd	|- ( ( ph /\ ( X e. ( Z L W ) \/ Z = W ) ) -> X e. ( Z L W ) )
30	1 2 3 13 14 15 19 20 21 24 25 29	tglineeltr	|- ( ( ph /\ ( X e. ( Z L W ) \/ Z = W ) ) -> X e. ( Z L Y ) )
31	30	orcd	|- ( ( ph /\ ( X e. ( Z L W ) \/ Z = W ) ) -> ( X e. ( Z L Y ) \/ Z = Y ) )
32	12 31	mtand	|- ( ph -> -. ( X e. ( Z L W ) \/ Z = W ) )