tgextamirn

Description: The midpoint-reflected point is off line A C . If it were on that line, mirln -- whose centre-on-the-line hypothesis is the midpoint, itself on A C -- would put its reflection there too, and mirmir says that reflection is B , contradicting the triangle's non-collinearity. This is the strengthening inA cannot give: it is what turns "inside the angle" into an open half-plane fact. (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	tgmircgrg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tgmircgrg.m	⊢ − = ( dist ‘ 𝐺 )
	tgmircgrg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tgmircgrg.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tgmircgrg.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tgmircgrg.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	tgmircgrg.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	tgmircgrg.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	tgmircgrg.ncol	⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
Assertion	tgextamirn	⊢ ( 𝜑 → ¬ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ ( 𝐴 𝐿 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		tgmircgrg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tgmircgrg.m	⊢ − = ( dist ‘ 𝐺 )
3		tgmircgrg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		tgmircgrg.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		tgmircgrg.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6		tgmircgrg.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7		tgmircgrg.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8		tgmircgrg.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9		tgmircgrg.ncol	⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
10	1 4 3 5 7 8 6 9	ncolrot1	⊢ ( 𝜑 → ¬ ( 𝐵 ∈ ( 𝐶 𝐿 𝐴 ) ∨ 𝐶 = 𝐴 ) )
11	1 4 3 5 8 6 7 10	ncolcom	⊢ ( 𝜑 → ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) )
12		ioran	⊢ ( ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) ↔ ( ¬ 𝐵 ∈ ( 𝐴 𝐿 𝐶 ) ∧ ¬ 𝐴 = 𝐶 ) )
13	11 12	sylib	⊢ ( 𝜑 → ( ¬ 𝐵 ∈ ( 𝐴 𝐿 𝐶 ) ∧ ¬ 𝐴 = 𝐶 ) )
14	13	simpld	⊢ ( 𝜑 → ¬ 𝐵 ∈ ( 𝐴 𝐿 𝐶 ) )
15		eqid	⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
16	5	adantr	⊢ ( ( 𝜑 ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝐺 ∈ TarskiG )
17	1 4 3 5 7 8 6 9	ncoltgdim2	⊢ ( 𝜑 → 𝐺 Dim_TarskiG≥ 2 )
18	1 2 3 5 17 6 8	midcl	⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ 𝑃 )
19	18	adantr	⊢ ( ( 𝜑 ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ ( 𝐴 𝐿 𝐶 ) ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ 𝑃 )
20		eqid	⊢ ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) = ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) )
21	7	adantr	⊢ ( ( 𝜑 ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝐵 ∈ 𝑃 )
22	1 2 3 4 15 16 19 20 21	mirmir	⊢ ( ( 𝜑 ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ ( 𝐴 𝐿 𝐶 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) = 𝐵 )
23	1 3 4 5 6 7 8 9	ncolne2	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
24	1 3 4 5 6 8 23	tgelrnln	⊢ ( 𝜑 → ( 𝐴 𝐿 𝐶 ) ∈ ran 𝐿 )
25	24	adantr	⊢ ( ( 𝜑 ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ ( 𝐴 𝐿 𝐶 ) ) → ( 𝐴 𝐿 𝐶 ) ∈ ran 𝐿 )
26	1 2 3 5 17 6 8	midbtwn	⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ ( 𝐴 𝐼 𝐶 ) )
27	1 4 3 5 6 8 18 26	btwncolg1	⊢ ( 𝜑 → ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) )
28	23	neneqd	⊢ ( 𝜑 → ¬ 𝐴 = 𝐶 )
29	27 28	olcnd	⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ ( 𝐴 𝐿 𝐶 ) )
30	29	adantr	⊢ ( ( 𝜑 ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ ( 𝐴 𝐿 𝐶 ) ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ ( 𝐴 𝐿 𝐶 ) )
31		simpr	⊢ ( ( 𝜑 ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ ( 𝐴 𝐿 𝐶 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ ( 𝐴 𝐿 𝐶 ) )
32	1 2 3 4 15 16 20 25 30 31	mirln	⊢ ( ( 𝜑 ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ ( 𝐴 𝐿 𝐶 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ∈ ( 𝐴 𝐿 𝐶 ) )
33	22 32	eqeltrrd	⊢ ( ( 𝜑 ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝐵 ∈ ( 𝐴 𝐿 𝐶 ) )
34	14 33	mtand	⊢ ( 𝜑 → ¬ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ ( 𝐴 𝐿 𝐶 ) )

Metamath Proof Explorer

Theorem tgextamirn

Proof