Theorem tgextalt2

Description: tgexta 's SECOND conjunct, strict, at a supplied second extension point E . This is NOT a permutation of the first conjunct: E is a new point, C between A and E , and tgextale / tgextancgra are applied a second time at the reconfigured triangle (the roles of A and B exchanged, exterior angle <" B C E "> ). tgextaoa then identifies <" B C E "> with <" A C D "> as vertical angles, and the two halves are transported across that congruence -- leacgra for leA , and cgratr under mtand for the negation, which leacgra cannot move. E is existentially constructed by tgexta , not here. (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	tgextalt2.p	$$⊢P={\mathrm{Base}}_G$$
	tgextalt2.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	tgextalt2.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	tgextalt2.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	tgextalt2.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
	tgextalt2.s	$$⊢\underset{\dot{}}{\le }={\le }_{𝒢}^{\angle }\left(G\right)$$
	tgextalt2.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	tgextalt2.a	$$⊢\phi \to A\in P$$
	tgextalt2.b	$$⊢\phi \to B\in P$$
	tgextalt2.c	$$⊢\phi \to C\in P$$
	tgextalt2.d	$$⊢\phi \to D\in P$$
	tgextalt2.e	$$⊢\phi \to E\in P$$
	tgextalt2.ext	$$⊢\phi \to C\in \left(BID\right)$$
	tgextalt2.ext2	$$⊢\phi \to C\in \left(AIE\right)$$
	tgextalt2.ncol	$$⊢\phi \to \neg \left(A\in \left(BLC\right)\vee B=C\right)$$
	tgextalt2.ne	$$⊢\phi \to C\ne D$$
	tgextalt2.ne2	$$⊢\phi \to C\ne E$$
Assertion	tgextalt2	$$⊢\phi \to \left(⟨“ABC”⟩\underset{\dot{}}{\le }⟨“ACD”⟩\wedge \neg ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		tgextalt2.p	$$⊢P={\mathrm{Base}}_G$$
2		tgextalt2.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		tgextalt2.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		tgextalt2.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
5		tgextalt2.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
6		tgextalt2.s	$$⊢\underset{\dot{}}{\le }={\le }_{𝒢}^{\angle }\left(G\right)$$
7		tgextalt2.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
8		tgextalt2.a	$$⊢\phi \to A\in P$$
9		tgextalt2.b	$$⊢\phi \to B\in P$$
10		tgextalt2.c	$$⊢\phi \to C\in P$$
11		tgextalt2.d	$$⊢\phi \to D\in P$$
12		tgextalt2.e	$$⊢\phi \to E\in P$$
13		tgextalt2.ext	$$⊢\phi \to C\in \left(BID\right)$$
14		tgextalt2.ext2	$$⊢\phi \to C\in \left(AIE\right)$$
15		tgextalt2.ncol	$$⊢\phi \to \neg \left(A\in \left(BLC\right)\vee B=C\right)$$
16		tgextalt2.ne	$$⊢\phi \to C\ne D$$
17		tgextalt2.ne2	$$⊢\phi \to C\ne E$$
18	1 4 3 7 9 10 8 15	ncolrot2	$$⊢\phi \to \neg \left(C\in \left(ALB\right)\vee A=B\right)$$
19	1 4 3 7 8 9 10 18	ncolcom	$$⊢\phi \to \neg \left(C\in \left(BLA\right)\vee B=A\right)$$
20	1 4 3 7 9 8 10 19	ncolrot1	$$⊢\phi \to \neg \left(B\in \left(ALC\right)\vee A=C\right)$$
21	1 2 3 4 5 7 9 8 10 12 14 20 17	tgextale	$$⊢\phi \to ⟨“CBA”⟩{\le }_{𝒢}^{\angle }\left(G\right)⟨“BCE”⟩$$
22	6	breqi	$$⊢⟨“CBA”⟩\underset{\dot{}}{\le }⟨“BCE”⟩\leftrightarrow ⟨“CBA”⟩{\le }_{𝒢}^{\angle }\left(G\right)⟨“BCE”⟩$$
23	21 22	sylibr	$$⊢\phi \to ⟨“CBA”⟩\underset{\dot{}}{\le }⟨“BCE”⟩$$
24	1 4 3 7 9 10 8 15	ncolrot1	$$⊢\phi \to \neg \left(B\in \left(CLA\right)\vee C=A\right)$$
25	1 3 4 7 9 10 8 24	ncolne1	$$⊢\phi \to B\ne C$$
26	25	necomd	$$⊢\phi \to C\ne B$$
27	1 3 4 7 8 9 10 15	ncolne1	$$⊢\phi \to A\ne B$$
28	27	necomd	$$⊢\phi \to B\ne A$$
29	1 3 7 5 10 9 8 26 28	cgraswap	$$⊢\phi \to ⟨“CBA”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ABC”⟩$$
30	1 3 4 7 8 9 10 15	ncolne2	$$⊢\phi \to A\ne C$$
31	30	necomd	$$⊢\phi \to C\ne A$$
32	16	necomd	$$⊢\phi \to D\ne C$$
33	1 2 3 5 7 8 9 10 11 12 13 14 26 31 32 17	tgextaoa	$$⊢\phi \to ⟨“BCE”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩$$
34	1 3 5 6 7 10 9 8 9 10 12 8 9 10 8 10 11 23 29 33	leacgra	$$⊢\phi \to ⟨“ABC”⟩\underset{\dot{}}{\le }⟨“ACD”⟩$$
35	1 2 3 4 5 7 9 8 10 12 14 20 17	tgextancgra	$$⊢\phi \to \neg ⟨“CBA”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“BCE”⟩$$
36	7	adantr	$$⊢\left(\phi \wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩\right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
37	10	adantr	$$⊢\left(\phi \wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩\right)\to C\in P$$
38	9	adantr	$$⊢\left(\phi \wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩\right)\to B\in P$$
39	8	adantr	$$⊢\left(\phi \wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩\right)\to A\in P$$
40	11	adantr	$$⊢\left(\phi \wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩\right)\to D\in P$$
41	29	adantr	$$⊢\left(\phi \wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩\right)\to ⟨“CBA”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ABC”⟩$$
42		simpr	$$⊢\left(\phi \wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩\right)\to ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩$$
43	1 3 36 5 37 38 39 39 38 37 41 39 37 40 42	cgratr	$$⊢\left(\phi \wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩\right)\to ⟨“CBA”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩$$
44	12	adantr	$$⊢\left(\phi \wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩\right)\to E\in P$$
45	1 3 7 5 9 10 12 8 10 11 33	cgracom	$$⊢\phi \to ⟨“ACD”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“BCE”⟩$$
46	45	adantr	$$⊢\left(\phi \wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩\right)\to ⟨“ACD”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“BCE”⟩$$
47	1 3 36 5 37 38 39 39 37 40 43 38 37 44 46	cgratr	$$⊢\left(\phi \wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩\right)\to ⟨“CBA”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“BCE”⟩$$
48	35 47	mtand	$$⊢\phi \to \neg ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩$$
49	34 48	jca	$$⊢\phi \to \left(⟨“ABC”⟩\underset{\dot{}}{\le }⟨“ACD”⟩\wedge \neg ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩\right)$$