Metamath Proof Explorer

Theorem tgextalem1inag

Description: The point obtained by reflecting B through the midpoint of A and C lies inside the exterior angle <" A C D "> . Proved by Pasch on the midpoint and the extension, turned into an in-angle statement with isinagd and moved from ray C M to ray C A by inaghl . (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 tgextalem1inag 
|- ( ph -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ( inA ` 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 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
15 1 4 3 6 8 9 7 12 ncolrot2 
 |-  ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
16 1 4 3 6 7 8 9 15 ncolcom 
 |-  ( ph -> -. ( C e. ( B L A ) \/ B = A ) )
17 1 4 3 6 8 7 9 16 ncolrot1 
 |-  ( ph -> -. ( B e. ( A L C ) \/ A = C ) )
18 1 4 3 6 7 9 8 17 ncoltgdim2 
 |-  ( ph -> G TarskiGDim>= 2 )
19 1 2 3 6 18 7 9 midcl 
 |-  ( ph -> ( A ( midG ` G ) C ) e. P )
20 eqid 
 |-  ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) = ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) )
21 1 2 3 4 14 6 19 20 8 mircl 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. P )
22 21 adantr 
 |-  ( ( ph /\ q e. P ) -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. P )
23 22 adantr 
 |-  ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. P )
24 19 adantr 
 |-  ( ( ph /\ q e. P ) -> ( A ( midG ` G ) C ) e. P )
25 24 adantr 
 |-  ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) -> ( A ( midG ` G ) C ) e. P )
26 9 adantr 
 |-  ( ( ph /\ q e. P ) -> C e. P )
27 26 adantr 
 |-  ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) -> C e. P )
28 10 adantr 
 |-  ( ( ph /\ q e. P ) -> D e. P )
29 28 adantr 
 |-  ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) -> D e. P )
30 6 adantr 
 |-  ( ( ph /\ q e. P ) -> G e. TarskiG )
31 30 adantr 
 |-  ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) -> G e. TarskiG )
32 31 elexd 
 |-  ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) -> G e. _V )
33 simpl 
 |-  ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) -> ( ph /\ q e. P ) )
34 33 simprd 
 |-  ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) -> q e. P )
35 ioran 
 |-  ( -. ( B e. ( A L C ) \/ A = C ) <-> ( -. B e. ( A L C ) /\ -. A = C ) )
36 17 35 sylib 
 |-  ( ph -> ( -. B e. ( A L C ) /\ -. A = C ) )
37 36 simprd 
 |-  ( ph -> -. A = C )
38 6 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) C ) = C ) -> G e. TarskiG )
39 19 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) C ) = C ) -> ( A ( midG ` G ) C ) e. P )
40 9 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) C ) = C ) -> C e. P )
41 7 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) C ) = C ) -> A e. P )
42 eqidd 
 |-  ( ph -> ( A ( midG ` G ) C ) = ( A ( midG ` G ) C ) )
43 1 2 3 6 18 7 9 42 midcgr 
 |-  ( ph -> ( ( A ( midG ` G ) C ) .- A ) = ( ( A ( midG ` G ) C ) .- C ) )
44 43 eqcomd 
 |-  ( ph -> ( ( A ( midG ` G ) C ) .- C ) = ( ( A ( midG ` G ) C ) .- A ) )
45 44 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) C ) = C ) -> ( ( A ( midG ` G ) C ) .- C ) = ( ( A ( midG ` G ) C ) .- A ) )
46 simpr 
 |-  ( ( ph /\ ( A ( midG ` G ) C ) = C ) -> ( A ( midG ` G ) C ) = C )
47 1 2 3 38 39 40 39 41 45 46 tgcgreq 
 |-  ( ( ph /\ ( A ( midG ` G ) C ) = C ) -> ( A ( midG ` G ) C ) = A )
48 47 46 eqtr3d 
 |-  ( ( ph /\ ( A ( midG ` G ) C ) = C ) -> A = C )
49 48 ex 
 |-  ( ph -> ( ( A ( midG ` G ) C ) = C -> A = C ) )
50 49 necon3bd 
 |-  ( ph -> ( -. A = C -> ( A ( midG ` G ) C ) =/= C ) )
51 37 50 mpd 
 |-  ( ph -> ( A ( midG ` G ) C ) =/= C )
52 51 adantr 
 |-  ( ( ph /\ q e. P ) -> ( A ( midG ` G ) C ) =/= C )
53 52 adantr 
 |-  ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) -> ( A ( midG ` G ) C ) =/= C )
54 13 necomd 
 |-  ( ph -> D =/= C )
55 54 adantr 
 |-  ( ( ph /\ q e. P ) -> D =/= C )
56 55 adantr 
 |-  ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) -> D =/= C )
57 1 2 3 6 7 19 axtgcgrrflx 
 |-  ( ph -> ( A .- ( A ( midG ` G ) C ) ) = ( ( A ( midG ` G ) C ) .- A ) )
58 57 43 eqtrd 
 |-  ( ph -> ( A .- ( A ( midG ` G ) C ) ) = ( ( A ( midG ` G ) C ) .- C ) )
59 1 2 3 6 9 19 axtgcgrrflx 
 |-  ( ph -> ( C .- ( A ( midG ` G ) C ) ) = ( ( A ( midG ` G ) C ) .- C ) )
60 59 eqcomd 
 |-  ( ph -> ( ( A ( midG ` G ) C ) .- C ) = ( C .- ( A ( midG ` G ) C ) ) )
61 58 60 eqtrd 
 |-  ( ph -> ( A .- ( A ( midG ` G ) C ) ) = ( C .- ( A ( midG ` G ) C ) ) )
62 1 2 3 6 18 7 9 midbtwn 
 |-  ( ph -> ( A ( midG ` G ) C ) e. ( A I C ) )
63 1 2 3 4 14 6 19 20 8 mirbtwn 
 |-  ( ph -> ( A ( midG ` G ) C ) e. ( ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) I B ) )
64 1 2 3 6 21 19 8 63 tgbtwncom 
 |-  ( ph -> ( A ( midG ` G ) C ) e. ( B I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) )
65 simpr 
 |-  ( ( ph /\ ( A ( midG ` G ) C ) = A ) -> ( A ( midG ` G ) C ) = A )
66 6 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) C ) = A ) -> G e. TarskiG )
67 19 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) C ) = A ) -> ( A ( midG ` G ) C ) e. P )
68 7 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) C ) = A ) -> A e. P )
69 9 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) C ) = A ) -> C e. P )
70 43 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) C ) = A ) -> ( ( A ( midG ` G ) C ) .- A ) = ( ( A ( midG ` G ) C ) .- C ) )
71 1 2 3 66 67 68 67 69 70 65 tgcgreq 
 |-  ( ( ph /\ ( A ( midG ` G ) C ) = A ) -> ( A ( midG ` G ) C ) = C )
72 65 71 eqtr3d 
 |-  ( ( ph /\ ( A ( midG ` G ) C ) = A ) -> A = C )
73 72 ex 
 |-  ( ph -> ( ( A ( midG ` G ) C ) = A -> A = C ) )
74 73 necon3bd 
 |-  ( ph -> ( -. A = C -> ( A ( midG ` G ) C ) =/= A ) )
75 37 74 mpd 
 |-  ( ph -> ( A ( midG ` G ) C ) =/= A )
76 37 neqned 
 |-  ( ph -> A =/= C )
77 1 3 4 6 7 9 19 76 62 btwnlng1 
 |-  ( ph -> ( A ( midG ` G ) C ) e. ( A L C ) )
78 36 simpld 
 |-  ( ph -> -. B e. ( A L C ) )
79 77 78 jca 
 |-  ( ph -> ( ( A ( midG ` G ) C ) e. ( A L C ) /\ -. B e. ( A L C ) ) )
80 nelne2 
 |-  ( ( ( A ( midG ` G ) C ) e. ( A L C ) /\ -. B e. ( A L C ) ) -> ( A ( midG ` G ) C ) =/= B )
81 79 80 syl 
 |-  ( ph -> ( A ( midG ` G ) C ) =/= B )
82 81 necomd 
 |-  ( ph -> B =/= ( A ( midG ` G ) C ) )
83 1 2 3 4 14 6 19 20 8 82 mirne 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) =/= ( A ( midG ` G ) C ) )
84 83 necomd 
 |-  ( ph -> ( A ( midG ` G ) C ) =/= ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) )
85 1 3 2 6 7 19 8 9 7 21 62 64 75 81 51 84 oacgr 
 |-  ( ph -> <" A ( A ( midG ` G ) C ) B "> ( cgrA ` G ) <" C ( A ( midG ` G ) C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) "> )
86 1 2 3 4 14 6 19 20 8 mircgr 
 |-  ( ph -> ( ( A ( midG ` G ) C ) .- ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) = ( ( A ( midG ` G ) C ) .- B ) )
87 86 eqcomd 
 |-  ( ph -> ( ( A ( midG ` G ) C ) .- B ) = ( ( A ( midG ` G ) C ) .- ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) )
88 1 3 4 6 7 8 9 12 ncolne1 
 |-  ( ph -> A =/= B )
89 1 2 3 6 7 19 8 9 19 21 61 85 87 88 tgsas2 
 |-  ( ph -> <" B A ( A ( midG ` G ) C ) "> ( cgrA ` G ) <" ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) C ( A ( midG ` G ) C ) "> )
90 1 3 5 6 8 7 19 21 9 19 89 cgrane3 
 |-  ( ph -> C =/= ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) )
91 90 necomd 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) =/= C )
92 91 adantr 
 |-  ( ( ph /\ q e. P ) -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) =/= C )
93 92 adantr 
 |-  ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) =/= C )
94 simpr 
 |-  ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) -> ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) )
95 94 simpld 
 |-  ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) -> q e. ( ( A ( midG ` G ) C ) I D ) )
96 27 adantr 
 |-  ( ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) /\ -. q = C ) -> C e. P )
97 23 adantr 
 |-  ( ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) /\ -. q = C ) -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. P )
98 34 adantr 
 |-  ( ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) /\ -. q = C ) -> q e. P )
99 31 adantr 
 |-  ( ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) /\ -. q = C ) -> G e. TarskiG )
100 94 simprd 
 |-  ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) -> q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) )
101 100 adantr 
 |-  ( ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) /\ -. q = C ) -> q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) )
102 93 necomd 
 |-  ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) -> C =/= ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) )
103 102 adantr 
 |-  ( ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) /\ -. q = C ) -> C =/= ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) )
104 simpr 
 |-  ( ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) /\ -. q = C ) -> -. q = C )
105 104 neqned 
 |-  ( ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) /\ -. q = C ) -> q =/= C )
106 1 3 5 96 97 98 99 98 101 103 105 btwnhl1 
 |-  ( ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) /\ -. q = C ) -> q ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) )
107 106 ex 
 |-  ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) -> ( -. q = C -> q ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) )
108 107 orrd 
 |-  ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) -> ( q = C \/ q ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) )
109 1 3 5 23 25 27 29 32 34 53 56 93 95 108 isinagd 
 |-  ( ( ( ph /\ q e. P ) /\ ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ( inA ` G ) <" ( A ( midG ` G ) C ) C D "> )
110 1 2 3 6 8 9 10 11 tgbtwncom 
 |-  ( ph -> C e. ( D I B ) )
111 1 2 3 6 21 10 8 19 9 63 110 axtgpasch 
 |-  ( ph -> E. q e. P ( q e. ( ( A ( midG ` G ) C ) I D ) /\ q e. ( C I ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) )
112 109 111 r19.29a 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ( inA ` G ) <" ( A ( midG ` G ) C ) C D "> )
113 1 3 5 7 9 19 6 10 62 76 51 btwnhl2 
 |-  ( ph -> ( A ( midG ` G ) C ) ( K ` C ) A )
114 1 3 5 19 7 9 6 113 hlcomd 
 |-  ( ph -> A ( K ` C ) ( A ( midG ` G ) C ) )
115 1 3 5 10 10 9 6 54 hlid 
 |-  ( ph -> D ( K ` C ) D )
116 1 3 5 21 21 9 6 91 hlid 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) )
117 1 3 5 21 19 9 10 6 112 7 10 21 114 115 116 inaghl 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ( inA ` G ) <" A C D "> )