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 = Line 𝒢 ⁡ G
tgextalem1inag.k ⊢ K = hl 𝒢 ⁡ G
tgextalem1inag.g ⊢ φ → G ∈ 𝒢 Tarski
tgextalem1inag.a ⊢ φ → A ∈ P
tgextalem1inag.b ⊢ φ → B ∈ P
tgextalem1inag.c ⊢ φ → C ∈ P
tgextalem1inag.d ⊢ φ → D ∈ P
tgextalem1inag.ext ⊢ φ → C ∈ B I D
tgextalem1inag.ncol ⊢ φ → ¬ A ∈ B L C ∨ B = C
tgextalem1inag.ne ⊢ φ → C ≠ D
Assertion tgextamirnhl ⊢ φ → ¬ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ 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 = Line 𝒢 ⁡ G
5 tgextalem1inag.k ⊢ K = hl 𝒢 ⁡ G
6 tgextalem1inag.g ⊢ φ → G ∈ 𝒢 Tarski
7 tgextalem1inag.a ⊢ φ → A ∈ P
8 tgextalem1inag.b ⊢ φ → B ∈ P
9 tgextalem1inag.c ⊢ φ → C ∈ P
10 tgextalem1inag.d ⊢ φ → D ∈ P
11 tgextalem1inag.ext ⊢ φ → C ∈ B I D
12 tgextalem1inag.ncol ⊢ φ → ¬ A ∈ B L C ∨ B = C
13 tgextalem1inag.ne ⊢ φ → C ≠ D
14 1 4 3 6 8 9 7 12 ncolcom ⊢ φ → ¬ A ∈ C L B ∨ C = B
15 ioran ⊢ ¬ A ∈ C L B ∨ C = B ↔ ¬ A ∈ C L B ∧ ¬ C = B
16 14 15 sylib ⊢ φ → ¬ A ∈ C L B ∧ ¬ C = B
17 16 simpld ⊢ φ → ¬ A ∈ C L B
18 6 adantr ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → G ∈ 𝒢 Tarski
19 9 adantr ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → C ∈ P
20 1 4 3 6 8 9 7 12 ncoltgdim2 ⊢ φ → G Dim 𝒢 ≥ 2
21 1 2 3 6 20 7 9 midcl ⊢ φ → A mid 𝒢 ⁡ G C ∈ P
22 21 adantr ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → A mid 𝒢 ⁡ G C ∈ P
23 7 adantr ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → A ∈ P
24 1 2 3 6 20 7 9 midbtwn ⊢ φ → A mid 𝒢 ⁡ G C ∈ A I C
25 1 2 3 6 7 21 9 24 tgbtwncom ⊢ φ → A mid 𝒢 ⁡ G C ∈ C I A
26 25 adantr ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → A mid 𝒢 ⁡ G C ∈ C I A
27 1 4 3 18 19 22 23 26 btwncolg3 ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → A ∈ C L A mid 𝒢 ⁡ G C ∨ C = A mid 𝒢 ⁡ G C
28 eqidd ⊢ φ → A mid 𝒢 ⁡ G C = A mid 𝒢 ⁡ G C
29 eqid ⊢ pInv 𝒢 ⁡ G = pInv 𝒢 ⁡ G
30 1 2 3 6 20 7 9 29 21 ismidb ⊢ φ → C = pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ A ↔ A mid 𝒢 ⁡ G C = A mid 𝒢 ⁡ G C
31 28 30 mpbird ⊢ φ → C = pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ A
32 eqid ⊢ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C = pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C
33 1 3 4 6 7 8 9 12 ncolne2 ⊢ φ → A ≠ C
34 33 necomd ⊢ φ → C ≠ A
35 31 eqeq1d ⊢ φ → C = A ↔ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ A = A
36 1 2 3 4 29 6 21 32 7 mirinv ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ A = A ↔ A mid 𝒢 ⁡ G C = A
37 35 36 bitrd ⊢ φ → C = A ↔ A mid 𝒢 ⁡ G C = A
38 37 necon3bid ⊢ φ → C ≠ A ↔ A mid 𝒢 ⁡ G C ≠ A
39 34 38 mpbid ⊢ φ → A mid 𝒢 ⁡ G C ≠ A
40 39 necomd ⊢ φ → A ≠ A mid 𝒢 ⁡ G C
41 1 2 3 4 29 6 21 32 7 40 mirne ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ A ≠ A mid 𝒢 ⁡ G C
42 31 41 eqnetrd ⊢ φ → C ≠ A mid 𝒢 ⁡ G C
43 42 neneqd ⊢ φ → ¬ C = A mid 𝒢 ⁡ G C
44 43 adantr ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → ¬ C = A mid 𝒢 ⁡ G C
45 27 44 olcnd ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → A ∈ C L A mid 𝒢 ⁡ G C
46 8 adantr ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → B ∈ P
47 16 simprd ⊢ φ → ¬ C = B
48 47 neqned ⊢ φ → C ≠ B
49 48 adantr ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → C ≠ B
50 42 necomd ⊢ φ → A mid 𝒢 ⁡ G C ≠ C
51 50 adantr ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → A mid 𝒢 ⁡ G C ≠ C
52 1 3 4 6 9 8 48 tgelrnln ⊢ φ → C L B ∈ ran ⁡ L
53 52 adantr ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → C L B ∈ ran ⁡ L
54 1 3 4 6 9 8 48 tglinerflx2 ⊢ φ → B ∈ C L B
55 54 adantr ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → B ∈ C L B
56 1 2 3 4 29 6 21 32 8 mircl ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ P
57 56 adantr ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ P
58 10 adantr ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → D ∈ P
59 simpr ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
60 1 3 5 58 57 19 18 59 hlcomd ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B K ⁡ C D
61 1 3 5 57 58 19 18 4 60 hlln ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ D L C
62 13 necomd ⊢ φ → D ≠ C
63 62 adantr ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → D ≠ C
64 1 3 4 18 58 19 63 tglinecom ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → D L C = C L D
65 61 64 eleqtrd ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ C L D
66 1 2 3 6 8 9 10 11 tgbtwncom ⊢ φ → C ∈ D I B
67 1 4 3 6 9 8 10 66 btwncolg2 ⊢ φ → D ∈ C L B ∨ C = B
68 67 47 olcnd ⊢ φ → D ∈ C L B
69 1 3 4 6 9 8 48 10 62 68 tglineelsb2 ⊢ φ → C L B = C L D
70 69 adantr ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → C L B = C L D
71 65 70 eleqtrrd ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ C L B
72 1 2 3 4 29 18 32 53 22 55 71 mirln2 ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → A mid 𝒢 ⁡ G C ∈ C L B
73 1 3 4 18 19 46 49 22 51 72 tglineelsb2 ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → C L B = C L A mid 𝒢 ⁡ G C
74 45 73 eleqtrrd ⊢ φ ∧ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → A ∈ C L B
75 17 74 mtand ⊢ φ → ¬ D K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B