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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tgextaoa.m	⊢ − = ( dist ‘ 𝐺 )
	tgextaoa.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tgextaoa.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	tgextaoa.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tgextaoa.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	tgextaoa.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	tgextaoa.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	tgextaoa.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	tgextaoa.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
	tgextaoa.ext	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
	tgextaoa.ext2	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐸 ) )
	tgextaoa.cb	⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
	tgextaoa.ca	⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
	tgextaoa.dc	⊢ ( 𝜑 → 𝐷 ≠ 𝐶 )
	tgextaoa.ce	⊢ ( 𝜑 → 𝐶 ≠ 𝐸 )
Assertion	tgextaoa	⊢ ( 𝜑 → ⟨“ 𝐵 𝐶 𝐸 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )

Proof

Step	Hyp	Ref	Expression
1		tgextaoa.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tgextaoa.m	⊢ − = ( dist ‘ 𝐺 )
3		tgextaoa.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		tgextaoa.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
5		tgextaoa.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6		tgextaoa.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7		tgextaoa.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8		tgextaoa.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9		tgextaoa.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
10		tgextaoa.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
11		tgextaoa.ext	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
12		tgextaoa.ext2	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐸 ) )
13		tgextaoa.cb	⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
14		tgextaoa.ca	⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
15		tgextaoa.dc	⊢ ( 𝜑 → 𝐷 ≠ 𝐶 )
16		tgextaoa.ce	⊢ ( 𝜑 → 𝐶 ≠ 𝐸 )
17	1 3 5 4 9 8 10 15 16	cgraswap	⊢ ( 𝜑 → ⟨“ 𝐷 𝐶 𝐸 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐶 𝐷 ”⟩ )
18	1 2 3 5 7 8 9 11	tgbtwncom	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) )
19	1 2 3 5 6 8 10 12	tgbtwncom	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐸 𝐼 𝐴 ) )
20	1 3 2 5 9 8 10 10 8 9 7 6 17 18 19 13 14	sacgr	⊢ ( 𝜑 → ⟨“ 𝐵 𝐶 𝐸 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )