Metamath Proof Explorer

Theorem tgmircgrg

Description: Reflecting B through the midpoint of A and C carries triangle C A B onto A C P , where P is the reflected point. The dimension condition the mid* family carries is discharged from the non-collinearity through ncoltgdim2 , not taken as a hypothesis. (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 tgmircgrg ⊢ φ → ⟨“ CAB ”⟩ ∼ 𝒢 ⁡ G ⟨“ AC pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ”⟩

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 eqid ⊢ ∼ 𝒢 ⁡ G = ∼ 𝒢 ⁡ G
11 eqid ⊢ pInv 𝒢 ⁡ G = pInv 𝒢 ⁡ G
12 1 4 3 5 7 8 6 9 ncoltgdim2 ⊢ φ → G Dim 𝒢 ≥ 2
13 1 2 3 5 12 6 8 midcl ⊢ φ → A mid 𝒢 ⁡ G C ∈ P
14 eqid ⊢ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C = pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C
15 1 2 3 4 11 5 13 14 7 mircl ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ P
16 eqidd ⊢ φ → A - ˙ C = A - ˙ C
17 1 2 3 5 6 8 6 8 16 tgcgrcoml ⊢ φ → C - ˙ A = A - ˙ C
18 eqidd ⊢ φ → A mid 𝒢 ⁡ G C = A mid 𝒢 ⁡ G C
19 1 2 3 5 12 6 8 11 13 ismidb ⊢ φ → C = pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ A ↔ A mid 𝒢 ⁡ G C = A mid 𝒢 ⁡ G C
20 18 19 mpbird ⊢ φ → C = pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ A
21 20 oveq1d ⊢ φ → C - ˙ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B = pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ A - ˙ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
22 1 2 3 4 11 5 13 14 6 7 miriso ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ A - ˙ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B = A - ˙ B
23 21 22 eqtrd ⊢ φ → C - ˙ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B = A - ˙ B
24 23 eqcomd ⊢ φ → A - ˙ B = C - ˙ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
25 1 2 3 4 11 5 13 14 7 8 miriso ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B - ˙ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ C = B - ˙ C
26 20 fveq2d ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ C = pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ A
27 1 2 3 4 11 5 13 14 6 mirmir ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ A = A
28 26 27 eqtrd ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ C = A
29 28 oveq2d ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B - ˙ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ C = pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B - ˙ A
30 25 29 eqtr3d ⊢ φ → B - ˙ C = pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B - ˙ A
31 1 2 10 5 8 6 7 6 8 15 17 24 30 trgcgr ⊢ φ → ⟨“ CAB ”⟩ ∼ 𝒢 ⁡ G ⟨“ AC pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ”⟩