Metamath Proof Explorer

Theorem 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 ⊢ P = Base G
tgmircgrg.m ⊢ - ˙ = dist ⁡ G
tgmircgrg.i ⊢ I = Itv ⁡ G
tgmircgrg.l ⊢ L = Line 𝒢 ⁡ G
tgmircgrg.g ⊢ φ → G ∈ 𝒢 Tarski
tgmircgrg.a ⊢ φ → A ∈ P
tgmircgrg.b ⊢ φ → B ∈ P
tgmircgrg.c ⊢ φ → C ∈ P
tgmircgrg.ncol ⊢ φ → ¬ A ∈ B L C ∨ B = C
Assertion tgextamirn ⊢ φ → ¬ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ A L C

Proof

Step Hyp Ref Expression
1 tgmircgrg.p ⊢ P = Base G
2 tgmircgrg.m ⊢ - ˙ = dist ⁡ G
3 tgmircgrg.i ⊢ I = Itv ⁡ G
4 tgmircgrg.l ⊢ L = Line 𝒢 ⁡ G
5 tgmircgrg.g ⊢ φ → G ∈ 𝒢 Tarski
6 tgmircgrg.a ⊢ φ → A ∈ P
7 tgmircgrg.b ⊢ φ → B ∈ P
8 tgmircgrg.c ⊢ φ → C ∈ P
9 tgmircgrg.ncol ⊢ φ → ¬ A ∈ B L C ∨ B = C
10 1 4 3 5 7 8 6 9 ncolrot1 ⊢ φ → ¬ B ∈ C L A ∨ C = A
11 1 4 3 5 8 6 7 10 ncolcom ⊢ φ → ¬ B ∈ A L C ∨ A = C
12 ioran ⊢ ¬ B ∈ A L C ∨ A = C ↔ ¬ B ∈ A L C ∧ ¬ A = C
13 11 12 sylib ⊢ φ → ¬ B ∈ A L C ∧ ¬ A = C
14 13 simpld ⊢ φ → ¬ B ∈ A L C
15 eqid ⊢ pInv 𝒢 ⁡ G = pInv 𝒢 ⁡ G
16 5 adantr ⊢ φ ∧ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ A L C → G ∈ 𝒢 Tarski
17 1 4 3 5 7 8 6 9 ncoltgdim2 ⊢ φ → G Dim 𝒢 ≥ 2
18 1 2 3 5 17 6 8 midcl ⊢ φ → A mid 𝒢 ⁡ G C ∈ P
19 18 adantr ⊢ φ ∧ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ A L C → A mid 𝒢 ⁡ G C ∈ P
20 eqid ⊢ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C = pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C
21 7 adantr ⊢ φ ∧ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ A L C → B ∈ P
22 1 2 3 4 15 16 19 20 21 mirmir ⊢ φ ∧ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ A L C → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B = B
23 1 3 4 5 6 7 8 9 ncolne2 ⊢ φ → A ≠ C
24 1 3 4 5 6 8 23 tgelrnln ⊢ φ → A L C ∈ ran ⁡ L
25 24 adantr ⊢ φ ∧ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ A L C → A L C ∈ ran ⁡ L
26 1 2 3 5 17 6 8 midbtwn ⊢ φ → A mid 𝒢 ⁡ G C ∈ A I C
27 1 4 3 5 6 8 18 26 btwncolg1 ⊢ φ → A mid 𝒢 ⁡ G C ∈ A L C ∨ A = C
28 23 neneqd ⊢ φ → ¬ A = C
29 27 28 olcnd ⊢ φ → A mid 𝒢 ⁡ G C ∈ A L C
30 29 adantr ⊢ φ ∧ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ A L C → A mid 𝒢 ⁡ G C ∈ A L C
31 simpr ⊢ φ ∧ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ A L C → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ A L C
32 1 2 3 4 15 16 20 25 30 31 mirln ⊢ φ ∧ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ A L C → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ A L C
33 22 32 eqeltrrd ⊢ φ ∧ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ A L C → B ∈ A L C
34 14 33 mtand ⊢ φ → ¬ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ A L C