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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tgextalem1inag.m	⊢ − = ( dist ‘ 𝐺 )
	tgextalem1inag.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tgextalem1inag.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tgextalem1inag.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	tgextalem1inag.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tgextalem1inag.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	tgextalem1inag.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	tgextalem1inag.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	tgextalem1inag.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	tgextalem1inag.ext	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
	tgextalem1inag.ncol	⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
	tgextalem1inag.ne	⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )
Assertion	tgextamirnhl	⊢ ( 𝜑 → ¬ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		tgextalem1inag.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tgextalem1inag.m	⊢ − = ( dist ‘ 𝐺 )
3		tgextalem1inag.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		tgextalem1inag.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		tgextalem1inag.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
6		tgextalem1inag.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7		tgextalem1inag.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8		tgextalem1inag.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9		tgextalem1inag.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
10		tgextalem1inag.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
11		tgextalem1inag.ext	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
12		tgextalem1inag.ncol	⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
13		tgextalem1inag.ne	⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )
14	1 4 3 6 8 9 7 12	ncolcom	⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐵 ) ∨ 𝐶 = 𝐵 ) )
15		ioran	⊢ ( ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐵 ) ∨ 𝐶 = 𝐵 ) ↔ ( ¬ 𝐴 ∈ ( 𝐶 𝐿 𝐵 ) ∧ ¬ 𝐶 = 𝐵 ) )
16	14 15	sylib	⊢ ( 𝜑 → ( ¬ 𝐴 ∈ ( 𝐶 𝐿 𝐵 ) ∧ ¬ 𝐶 = 𝐵 ) )
17	16	simpld	⊢ ( 𝜑 → ¬ 𝐴 ∈ ( 𝐶 𝐿 𝐵 ) )
18	6	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → 𝐺 ∈ TarskiG )
19	9	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → 𝐶 ∈ 𝑃 )
20	1 4 3 6 8 9 7 12	ncoltgdim2	⊢ ( 𝜑 → 𝐺 Dim_TarskiG≥ 2 )
21	1 2 3 6 20 7 9	midcl	⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ 𝑃 )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ 𝑃 )
23	7	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → 𝐴 ∈ 𝑃 )
24	1 2 3 6 20 7 9	midbtwn	⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ ( 𝐴 𝐼 𝐶 ) )
25	1 2 3 6 7 21 9 24	tgbtwncom	⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ ( 𝐶 𝐼 𝐴 ) )
26	25	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ ( 𝐶 𝐼 𝐴 ) )
27	1 4 3 18 19 22 23 26	btwncolg3	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → ( 𝐴 ∈ ( 𝐶 𝐿 ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ∨ 𝐶 = ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) )
28		eqidd	⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) )
29		eqid	⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
30	1 2 3 6 20 7 9 29 21	ismidb	⊢ ( 𝜑 → ( 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐴 ) ↔ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) )
31	28 30	mpbird	⊢ ( 𝜑 → 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐴 ) )
32		eqid	⊢ ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) = ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) )
33	1 3 4 6 7 8 9 12	ncolne2	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
34	33	necomd	⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
35	31	eqeq1d	⊢ ( 𝜑 → ( 𝐶 = 𝐴 ↔ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐴 ) = 𝐴 ) )
36	1 2 3 4 29 6 21 32 7	mirinv	⊢ ( 𝜑 → ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐴 ) = 𝐴 ↔ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐴 ) )
37	35 36	bitrd	⊢ ( 𝜑 → ( 𝐶 = 𝐴 ↔ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐴 ) )
38	37	necon3bid	⊢ ( 𝜑 → ( 𝐶 ≠ 𝐴 ↔ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ≠ 𝐴 ) )
39	34 38	mpbid	⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ≠ 𝐴 )
40	39	necomd	⊢ ( 𝜑 → 𝐴 ≠ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) )
41	1 2 3 4 29 6 21 32 7 40	mirne	⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐴 ) ≠ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) )
42	31 41	eqnetrd	⊢ ( 𝜑 → 𝐶 ≠ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) )
43	42	neneqd	⊢ ( 𝜑 → ¬ 𝐶 = ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) )
44	43	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → ¬ 𝐶 = ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) )
45	27 44	olcnd	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → 𝐴 ∈ ( 𝐶 𝐿 ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) )
46	8	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → 𝐵 ∈ 𝑃 )
47	16	simprd	⊢ ( 𝜑 → ¬ 𝐶 = 𝐵 )
48	47	neqned	⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
49	48	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → 𝐶 ≠ 𝐵 )
50	42	necomd	⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ≠ 𝐶 )
51	50	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ≠ 𝐶 )
52	1 3 4 6 9 8 48	tgelrnln	⊢ ( 𝜑 → ( 𝐶 𝐿 𝐵 ) ∈ ran 𝐿 )
53	52	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → ( 𝐶 𝐿 𝐵 ) ∈ ran 𝐿 )
54	1 3 4 6 9 8 48	tglinerflx2	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐶 𝐿 𝐵 ) )
55	54	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → 𝐵 ∈ ( 𝐶 𝐿 𝐵 ) )
56	1 2 3 4 29 6 21 32 8	mircl	⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ 𝑃 )
57	56	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ 𝑃 )
58	10	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → 𝐷 ∈ 𝑃 )
59		simpr	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) )
60	1 3 5 58 57 19 18 59	hlcomd	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ( 𝐾 ‘ 𝐶 ) 𝐷 )
61	1 3 5 57 58 19 18 4 60	hlln	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ ( 𝐷 𝐿 𝐶 ) )
62	13	necomd	⊢ ( 𝜑 → 𝐷 ≠ 𝐶 )
63	62	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → 𝐷 ≠ 𝐶 )
64	1 3 4 18 58 19 63	tglinecom	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → ( 𝐷 𝐿 𝐶 ) = ( 𝐶 𝐿 𝐷 ) )
65	61 64	eleqtrd	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ ( 𝐶 𝐿 𝐷 ) )
66	1 2 3 6 8 9 10 11	tgbtwncom	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) )
67	1 4 3 6 9 8 10 66	btwncolg2	⊢ ( 𝜑 → ( 𝐷 ∈ ( 𝐶 𝐿 𝐵 ) ∨ 𝐶 = 𝐵 ) )
68	67 47	olcnd	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 𝐿 𝐵 ) )
69	1 3 4 6 9 8 48 10 62 68	tglineelsb2	⊢ ( 𝜑 → ( 𝐶 𝐿 𝐵 ) = ( 𝐶 𝐿 𝐷 ) )
70	69	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → ( 𝐶 𝐿 𝐵 ) = ( 𝐶 𝐿 𝐷 ) )
71	65 70	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ ( 𝐶 𝐿 𝐵 ) )
72	1 2 3 4 29 18 32 53 22 55 71	mirln2	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ ( 𝐶 𝐿 𝐵 ) )
73	1 3 4 18 19 46 49 22 51 72	tglineelsb2	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → ( 𝐶 𝐿 𝐵 ) = ( 𝐶 𝐿 ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) )
74	45 73	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → 𝐴 ∈ ( 𝐶 𝐿 𝐵 ) )
75	17 74	mtand	⊢ ( 𝜑 → ¬ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) )

Metamath Proof Explorer

Theorem tgextamirnhl

Proof