Metamath Proof Explorer

Theorem tgextancgra

Description: The exterior angle is NOT congruent to the remote interior angle -- the strictness tgextale cannot give, and what tgaas 's contradiction branch needs. The exterior angle is <" A C D "> , at the extension of B C beyond C . The tail of GeoCoq's l11__41__aux , run through acopyeu rather than conga__cop__or__out__ts : a congruent exterior angle would, by angle-construction uniqueness, put the midpoint-reflected point of tgmircgra on the ray C D -- the two rays make congruent angles with the shared base ray C A and, by tgextahp and hpgid , lie on the same open half-plane of line A C -- which tgextamirnhl forbids. Both of acopyeu 's non-collinearity hypotheses are discharged, not assumed: source side by rotating the triangle's own ncol , target side by tgextancd . (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses tgextalem1inag.p 
|- P = ( Base ` G )
tgextalem1inag.m 
|- .- = ( dist ` G )
tgextalem1inag.i 
|- I = ( Itv ` G )
tgextalem1inag.l 
|- L = ( LineG ` G )
tgextalem1inag.k 
|- K = ( hlG ` G )
tgextalem1inag.g 
|- ( ph -> G e. TarskiG )
tgextalem1inag.a 
|- ( ph -> A e. P )
tgextalem1inag.b 
|- ( ph -> B e. P )
tgextalem1inag.c 
|- ( ph -> C e. P )
tgextalem1inag.d 
|- ( ph -> D e. P )
tgextalem1inag.ext 
|- ( ph -> C e. ( B I D ) )
tgextalem1inag.ncol 
|- ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
tgextalem1inag.ne 
|- ( ph -> C =/= D )
Assertion tgextancgra 
|- ( ph -> -. <" C A B "> ( cgrA ` G ) <" A C D "> )

Proof

Step Hyp Ref Expression
1 tgextalem1inag.p 
 |-  P = ( Base ` G )
2 tgextalem1inag.m 
 |-  .- = ( dist ` G )
3 tgextalem1inag.i 
 |-  I = ( Itv ` G )
4 tgextalem1inag.l 
 |-  L = ( LineG ` G )
5 tgextalem1inag.k 
 |-  K = ( hlG ` G )
6 tgextalem1inag.g 
 |-  ( ph -> G e. TarskiG )
7 tgextalem1inag.a 
 |-  ( ph -> A e. P )
8 tgextalem1inag.b 
 |-  ( ph -> B e. P )
9 tgextalem1inag.c 
 |-  ( ph -> C e. P )
10 tgextalem1inag.d 
 |-  ( ph -> D e. P )
11 tgextalem1inag.ext 
 |-  ( ph -> C e. ( B I D ) )
12 tgextalem1inag.ncol 
 |-  ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
13 tgextalem1inag.ne 
 |-  ( ph -> C =/= D )
14 1 2 3 4 5 6 7 8 9 10 11 12 13 tgextamirnhl 
 |-  ( ph -> -. D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) )
15 6 adantr 
 |-  ( ( ph /\ <" C A B "> ( cgrA ` G ) <" A C D "> ) -> G e. TarskiG )
16 9 adantr 
 |-  ( ( ph /\ <" C A B "> ( cgrA ` G ) <" A C D "> ) -> C e. P )
17 7 adantr 
 |-  ( ( ph /\ <" C A B "> ( cgrA ` G ) <" A C D "> ) -> A e. P )
18 8 adantr 
 |-  ( ( ph /\ <" C A B "> ( cgrA ` G ) <" A C D "> ) -> B e. P )
19 10 adantr 
 |-  ( ( ph /\ <" C A B "> ( cgrA ` G ) <" A C D "> ) -> D e. P )
20 1 4 3 6 8 9 7 12 ncolrot1 
 |-  ( ph -> -. ( B e. ( C L A ) \/ C = A ) )
21 1 4 3 6 9 7 8 20 ncolrot1 
 |-  ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
22 21 adantr 
 |-  ( ( ph /\ <" C A B "> ( cgrA ` G ) <" A C D "> ) -> -. ( C e. ( A L B ) \/ A = B ) )
23 1 2 3 4 6 7 8 9 10 11 12 13 tgextancd 
 |-  ( ph -> -. ( A e. ( C L D ) \/ C = D ) )
24 23 adantr 
 |-  ( ( ph /\ <" C A B "> ( cgrA ` G ) <" A C D "> ) -> -. ( A e. ( C L D ) \/ C = D ) )
25 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
26 1 4 3 6 8 9 7 12 ncoltgdim2 
 |-  ( ph -> G TarskiGDim>= 2 )
27 1 2 3 6 26 7 9 midcl 
 |-  ( ph -> ( A ( midG ` G ) C ) e. P )
28 eqid 
 |-  ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) = ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) )
29 1 2 3 4 25 6 27 28 8 mircl 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. P )
30 29 adantr 
 |-  ( ( ph /\ <" C A B "> ( cgrA ` G ) <" A C D "> ) -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. P )
31 simpr 
 |-  ( ( ph /\ <" C A B "> ( cgrA ` G ) <" A C D "> ) -> <" C A B "> ( cgrA ` G ) <" A C D "> )
32 1 2 3 4 6 7 8 9 12 tgmircgra 
 |-  ( ph -> <" C A B "> ( cgrA ` G ) <" A C ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) "> )
33 32 adantr 
 |-  ( ( ph /\ <" C A B "> ( cgrA ` G ) <" A C D "> ) -> <" C A B "> ( cgrA ` G ) <" A C ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) "> )
34 1 3 4 6 7 8 9 12 ncolne2 
 |-  ( ph -> A =/= C )
35 1 3 4 6 7 9 34 tgelrnln 
 |-  ( ph -> ( A L C ) e. ran L )
36 simpl 
 |-  ( ( u = a /\ v = b ) -> u = a )
37 36 eleq1d 
 |-  ( ( u = a /\ v = b ) -> ( u e. ( P \ ( A L C ) ) <-> a e. ( P \ ( A L C ) ) ) )
38 simpr 
 |-  ( ( u = a /\ v = b ) -> v = b )
39 38 eleq1d 
 |-  ( ( u = a /\ v = b ) -> ( v e. ( P \ ( A L C ) ) <-> b e. ( P \ ( A L C ) ) ) )
40 37 39 anbi12d 
 |-  ( ( u = a /\ v = b ) -> ( ( u e. ( P \ ( A L C ) ) /\ v e. ( P \ ( A L C ) ) ) <-> ( a e. ( P \ ( A L C ) ) /\ b e. ( P \ ( A L C ) ) ) ) )
41 simpr 
 |-  ( ( ( u = a /\ v = b ) /\ w = t ) -> w = t )
42 simpll 
 |-  ( ( ( u = a /\ v = b ) /\ w = t ) -> u = a )
43 simplr 
 |-  ( ( ( u = a /\ v = b ) /\ w = t ) -> v = b )
44 42 43 oveq12d 
 |-  ( ( ( u = a /\ v = b ) /\ w = t ) -> ( u I v ) = ( a I b ) )
45 41 44 eleq12d 
 |-  ( ( ( u = a /\ v = b ) /\ w = t ) -> ( w e. ( u I v ) <-> t e. ( a I b ) ) )
46 45 cbvrexdva 
 |-  ( ( u = a /\ v = b ) -> ( E. w e. ( A L C ) w e. ( u I v ) <-> E. t e. ( A L C ) t e. ( a I b ) ) )
47 40 46 anbi12d 
 |-  ( ( u = a /\ v = b ) -> ( ( ( u e. ( P \ ( A L C ) ) /\ v e. ( P \ ( A L C ) ) ) /\ E. w e. ( A L C ) w e. ( u I v ) ) <-> ( ( a e. ( P \ ( A L C ) ) /\ b e. ( P \ ( A L C ) ) ) /\ E. t e. ( A L C ) t e. ( a I b ) ) ) )
48 47 cbvopabv 
 |-  { <. u , v >. | ( ( u e. ( P \ ( A L C ) ) /\ v e. ( P \ ( A L C ) ) ) /\ E. w e. ( A L C ) w e. ( u I v ) ) } = { <. a , b >. | ( ( a e. ( P \ ( A L C ) ) /\ b e. ( P \ ( A L C ) ) ) /\ E. t e. ( A L C ) t e. ( a I b ) ) }
49 ioran 
 |-  ( -. ( A e. ( C L D ) \/ C = D ) <-> ( -. A e. ( C L D ) /\ -. C = D ) )
50 23 49 sylib 
 |-  ( ph -> ( -. A e. ( C L D ) /\ -. C = D ) )
51 50 simpld 
 |-  ( ph -> -. A e. ( C L D ) )
52 34 necomd 
 |-  ( ph -> C =/= A )
53 1 3 4 6 9 7 52 tglinerflx2 
 |-  ( ph -> A e. ( C L A ) )
54 53 adantr 
 |-  ( ( ph /\ D e. ( A L C ) ) -> A e. ( C L A ) )
55 6 adantr 
 |-  ( ( ph /\ D e. ( A L C ) ) -> G e. TarskiG )
56 9 adantr 
 |-  ( ( ph /\ D e. ( A L C ) ) -> C e. P )
57 7 adantr 
 |-  ( ( ph /\ D e. ( A L C ) ) -> A e. P )
58 52 adantr 
 |-  ( ( ph /\ D e. ( A L C ) ) -> C =/= A )
59 10 adantr 
 |-  ( ( ph /\ D e. ( A L C ) ) -> D e. P )
60 13 necomd 
 |-  ( ph -> D =/= C )
61 60 adantr 
 |-  ( ( ph /\ D e. ( A L C ) ) -> D =/= C )
62 simpr 
 |-  ( ( ph /\ D e. ( A L C ) ) -> D e. ( A L C ) )
63 34 adantr 
 |-  ( ( ph /\ D e. ( A L C ) ) -> A =/= C )
64 1 3 4 55 57 56 63 tglinecom 
 |-  ( ( ph /\ D e. ( A L C ) ) -> ( A L C ) = ( C L A ) )
65 62 64 eleqtrd 
 |-  ( ( ph /\ D e. ( A L C ) ) -> D e. ( C L A ) )
66 1 3 4 55 56 57 58 59 61 65 tglineelsb2 
 |-  ( ( ph /\ D e. ( A L C ) ) -> ( C L A ) = ( C L D ) )
67 54 66 eleqtrd 
 |-  ( ( ph /\ D e. ( A L C ) ) -> A e. ( C L D ) )
68 51 67 mtand 
 |-  ( ph -> -. D e. ( A L C ) )
69 1 3 4 6 35 10 48 68 hpgid 
 |-  ( ph -> D ( ( hpG ` G ) ` ( A L C ) ) D )
70 69 adantr 
 |-  ( ( ph /\ <" C A B "> ( cgrA ` G ) <" A C D "> ) -> D ( ( hpG ` G ) ` ( A L C ) ) D )
71 1 2 3 4 5 6 7 8 9 10 11 12 13 tgextahp 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ( ( hpG ` G ) ` ( A L C ) ) D )
72 71 adantr 
 |-  ( ( ph /\ <" C A B "> ( cgrA ` G ) <" A C D "> ) -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ( ( hpG ` G ) ` ( A L C ) ) D )
73 1 3 2 15 16 17 18 17 16 19 4 22 24 19 30 5 31 33 70 72 acopyeu 
 |-  ( ( ph /\ <" C A B "> ( cgrA ` G ) <" A C D "> ) -> D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) )
74 14 73 mtand 
 |-  ( ph -> -. <" C A B "> ( cgrA ` G ) <" A C D "> )