Theorem tgextaoa

Description: The two exterior angles at C are VERTICAL, hence congruent. Ray C D is opposite ray C B and ray C E is opposite ray C A , so <" B C E "> and <" A C D "> have both legs flipped. One sacgr (Schwabhaeuser 11.13, GeoCoq l11__13 ) does it in a single shot, because sacgr flips the first slot of each side independently: the premise it wants is <" D C E "> ( cgrAG ) <" E C D "> , a bare angle reversal by cgraswap , needing no non-collinearity at all. oacgr (11.14) would prove the same thing from two supplements and is not used. (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	tgextaoa.p	$$⊢P={\mathrm{Base}}_G$$
	tgextaoa.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	tgextaoa.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	tgextaoa.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
	tgextaoa.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	tgextaoa.a	$$⊢\phi \to A\in P$$
	tgextaoa.b	$$⊢\phi \to B\in P$$
	tgextaoa.c	$$⊢\phi \to C\in P$$
	tgextaoa.d	$$⊢\phi \to D\in P$$
	tgextaoa.e	$$⊢\phi \to E\in P$$
	tgextaoa.ext	$$⊢\phi \to C\in \left(BID\right)$$
	tgextaoa.ext2	$$⊢\phi \to C\in \left(AIE\right)$$
	tgextaoa.cb	$$⊢\phi \to C\ne B$$
	tgextaoa.ca	$$⊢\phi \to C\ne A$$
	tgextaoa.dc	$$⊢\phi \to D\ne C$$
	tgextaoa.ce	$$⊢\phi \to C\ne E$$
Assertion	tgextaoa	$$⊢\phi \to ⟨“BCE”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩$$

Proof

Step	Hyp	Ref	Expression
1		tgextaoa.p	$$⊢P={\mathrm{Base}}_G$$
2		tgextaoa.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		tgextaoa.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		tgextaoa.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
5		tgextaoa.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
6		tgextaoa.a	$$⊢\phi \to A\in P$$
7		tgextaoa.b	$$⊢\phi \to B\in P$$
8		tgextaoa.c	$$⊢\phi \to C\in P$$
9		tgextaoa.d	$$⊢\phi \to D\in P$$
10		tgextaoa.e	$$⊢\phi \to E\in P$$
11		tgextaoa.ext	$$⊢\phi \to C\in \left(BID\right)$$
12		tgextaoa.ext2	$$⊢\phi \to C\in \left(AIE\right)$$
13		tgextaoa.cb	$$⊢\phi \to C\ne B$$
14		tgextaoa.ca	$$⊢\phi \to C\ne A$$
15		tgextaoa.dc	$$⊢\phi \to D\ne C$$
16		tgextaoa.ce	$$⊢\phi \to C\ne E$$
17	1 3 5 4 9 8 10 15 16	cgraswap	$$⊢\phi \to ⟨“DCE”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ECD”⟩$$
18	1 2 3 5 7 8 9 11	tgbtwncom	$$⊢\phi \to C\in \left(DIB\right)$$
19	1 2 3 5 6 8 10 12	tgbtwncom	$$⊢\phi \to C\in \left(EIA\right)$$
20	1 3 2 5 9 8 10 10 8 9 7 6 17 18 19 13 14	sacgr	$$⊢\phi \to ⟨“BCE”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩$$