Metamath Proof Explorer

Theorem tgextamirnhl

Description: The midpoint-reflected point is not on the ray from C through D . If it were, then -- ray C D being the extension of B C -- it would lie on line C B ; mirln2 , the converse of the mirln used in tgextamirn , would put the midpoint of A and C on that line too; and the midpoint is collinear with A and C , so A would land on line C B , contradicting the triangle's non-collinearity. M =/= C comes from ismidb / mirinv / mirne , not from midbtwn . (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 tgextamirnhl 
|- ( ph -> -. D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) )

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 4 3 6 8 9 7 12 ncolcom 
 |-  ( ph -> -. ( A e. ( C L B ) \/ C = B ) )
15 ioran 
 |-  ( -. ( A e. ( C L B ) \/ C = B ) <-> ( -. A e. ( C L B ) /\ -. C = B ) )
16 14 15 sylib 
 |-  ( ph -> ( -. A e. ( C L B ) /\ -. C = B ) )
17 16 simpld 
 |-  ( ph -> -. A e. ( C L B ) )
18 6 adantr 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> G e. TarskiG )
19 9 adantr 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> C e. P )
20 1 4 3 6 8 9 7 12 ncoltgdim2 
 |-  ( ph -> G TarskiGDim>= 2 )
21 1 2 3 6 20 7 9 midcl 
 |-  ( ph -> ( A ( midG ` G ) C ) e. P )
22 21 adantr 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> ( A ( midG ` G ) C ) e. P )
23 7 adantr 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> A e. P )
24 1 2 3 6 20 7 9 midbtwn 
 |-  ( ph -> ( A ( midG ` G ) C ) e. ( A I C ) )
25 1 2 3 6 7 21 9 24 tgbtwncom 
 |-  ( ph -> ( A ( midG ` G ) C ) e. ( C I A ) )
26 25 adantr 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> ( A ( midG ` G ) C ) e. ( C I A ) )
27 1 4 3 18 19 22 23 26 btwncolg3 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> ( A e. ( C L ( A ( midG ` G ) C ) ) \/ C = ( A ( midG ` G ) C ) ) )
28 eqidd 
 |-  ( ph -> ( A ( midG ` G ) C ) = ( A ( midG ` G ) C ) )
29 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
30 1 2 3 6 20 7 9 29 21 ismidb 
 |-  ( ph -> ( C = ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` A ) <-> ( A ( midG ` G ) C ) = ( A ( midG ` G ) C ) ) )
31 28 30 mpbird 
 |-  ( ph -> C = ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` A ) )
32 eqid 
 |-  ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) = ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) )
33 1 3 4 6 7 8 9 12 ncolne2 
 |-  ( ph -> A =/= C )
34 33 necomd 
 |-  ( ph -> C =/= A )
35 31 eqeq1d 
 |-  ( ph -> ( C = A <-> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` A ) = A ) )
36 1 2 3 4 29 6 21 32 7 mirinv 
 |-  ( ph -> ( ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` A ) = A <-> ( A ( midG ` G ) C ) = A ) )
37 35 36 bitrd 
 |-  ( ph -> ( C = A <-> ( A ( midG ` G ) C ) = A ) )
38 37 necon3bid 
 |-  ( ph -> ( C =/= A <-> ( A ( midG ` G ) C ) =/= A ) )
39 34 38 mpbid 
 |-  ( ph -> ( A ( midG ` G ) C ) =/= A )
40 39 necomd 
 |-  ( ph -> A =/= ( A ( midG ` G ) C ) )
41 1 2 3 4 29 6 21 32 7 40 mirne 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` A ) =/= ( A ( midG ` G ) C ) )
42 31 41 eqnetrd 
 |-  ( ph -> C =/= ( A ( midG ` G ) C ) )
43 42 neneqd 
 |-  ( ph -> -. C = ( A ( midG ` G ) C ) )
44 43 adantr 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> -. C = ( A ( midG ` G ) C ) )
45 27 44 olcnd 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> A e. ( C L ( A ( midG ` G ) C ) ) )
46 8 adantr 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> B e. P )
47 16 simprd 
 |-  ( ph -> -. C = B )
48 47 neqned 
 |-  ( ph -> C =/= B )
49 48 adantr 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> C =/= B )
50 42 necomd 
 |-  ( ph -> ( A ( midG ` G ) C ) =/= C )
51 50 adantr 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> ( A ( midG ` G ) C ) =/= C )
52 1 3 4 6 9 8 48 tgelrnln 
 |-  ( ph -> ( C L B ) e. ran L )
53 52 adantr 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> ( C L B ) e. ran L )
54 1 3 4 6 9 8 48 tglinerflx2 
 |-  ( ph -> B e. ( C L B ) )
55 54 adantr 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> B e. ( C L B ) )
56 1 2 3 4 29 6 21 32 8 mircl 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. P )
57 56 adantr 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. P )
58 10 adantr 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> D e. P )
59 simpr 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) )
60 1 3 5 58 57 19 18 59 hlcomd 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ( K ` C ) D )
61 1 3 5 57 58 19 18 4 60 hlln 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. ( D L C ) )
62 13 necomd 
 |-  ( ph -> D =/= C )
63 62 adantr 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> D =/= C )
64 1 3 4 18 58 19 63 tglinecom 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> ( D L C ) = ( C L D ) )
65 61 64 eleqtrd 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. ( C L D ) )
66 1 2 3 6 8 9 10 11 tgbtwncom 
 |-  ( ph -> C e. ( D I B ) )
67 1 4 3 6 9 8 10 66 btwncolg2 
 |-  ( ph -> ( D e. ( C L B ) \/ C = B ) )
68 67 47 olcnd 
 |-  ( ph -> D e. ( C L B ) )
69 1 3 4 6 9 8 48 10 62 68 tglineelsb2 
 |-  ( ph -> ( C L B ) = ( C L D ) )
70 69 adantr 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> ( C L B ) = ( C L D ) )
71 65 70 eleqtrrd 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. ( C L B ) )
72 1 2 3 4 29 18 32 53 22 55 71 mirln2 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> ( A ( midG ` G ) C ) e. ( C L B ) )
73 1 3 4 18 19 46 49 22 51 72 tglineelsb2 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> ( C L B ) = ( C L ( A ( midG ` G ) C ) ) )
74 45 73 eleqtrrd 
 |-  ( ( ph /\ D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> A e. ( C L B ) )
75 17 74 mtand 
 |-  ( ph -> -. D ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) )