Metamath Proof Explorer

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 = ( Base ` G )
tgextaoa.m 
|- .- = ( dist ` G )
tgextaoa.i 
|- I = ( Itv ` G )
tgextaoa.k 
|- K = ( hlG ` G )
tgextaoa.g 
|- ( ph -> G e. TarskiG )
tgextaoa.a 
|- ( ph -> A e. P )
tgextaoa.b 
|- ( ph -> B e. P )
tgextaoa.c 
|- ( ph -> C e. P )
tgextaoa.d 
|- ( ph -> D e. P )
tgextaoa.e 
|- ( ph -> E e. P )
tgextaoa.ext 
|- ( ph -> C e. ( B I D ) )
tgextaoa.ext2 
|- ( ph -> C e. ( A I E ) )
tgextaoa.cb 
|- ( ph -> C =/= B )
tgextaoa.ca 
|- ( ph -> C =/= A )
tgextaoa.dc 
|- ( ph -> D =/= C )
tgextaoa.ce 
|- ( ph -> C =/= E )
Assertion tgextaoa 
|- ( ph -> <" B C E "> ( cgrA ` G ) <" A C D "> )

Proof

Step Hyp Ref Expression
1 tgextaoa.p 
 |-  P = ( Base ` G )
2 tgextaoa.m 
 |-  .- = ( dist ` G )
3 tgextaoa.i 
 |-  I = ( Itv ` G )
4 tgextaoa.k 
 |-  K = ( hlG ` G )
5 tgextaoa.g 
 |-  ( ph -> G e. TarskiG )
6 tgextaoa.a 
 |-  ( ph -> A e. P )
7 tgextaoa.b 
 |-  ( ph -> B e. P )
8 tgextaoa.c 
 |-  ( ph -> C e. P )
9 tgextaoa.d 
 |-  ( ph -> D e. P )
10 tgextaoa.e 
 |-  ( ph -> E e. P )
11 tgextaoa.ext 
 |-  ( ph -> C e. ( B I D ) )
12 tgextaoa.ext2 
 |-  ( ph -> C e. ( A I E ) )
13 tgextaoa.cb 
 |-  ( ph -> C =/= B )
14 tgextaoa.ca 
 |-  ( ph -> C =/= A )
15 tgextaoa.dc 
 |-  ( ph -> D =/= C )
16 tgextaoa.ce 
 |-  ( ph -> C =/= E )
17 1 3 5 4 9 8 10 15 16 cgraswap 
 |-  ( ph -> <" D C E "> ( cgrA ` G ) <" E C D "> )
18 1 2 3 5 7 8 9 11 tgbtwncom 
 |-  ( ph -> C e. ( D I B ) )
19 1 2 3 5 6 8 10 12 tgbtwncom 
 |-  ( ph -> C e. ( E I A ) )
20 1 3 2 5 9 8 10 10 8 9 7 6 17 18 19 13 14 sacgr 
 |-  ( ph -> <" B C E "> ( cgrA ` G ) <" A C D "> )