Metamath Proof Explorer

Theorem mirleqb

Description: Equality theorem for point mirroring. (Contributed by Thierry Arnoux, 13-Jul-2026)

Ref Expression
Hypotheses mirleqb.p ⊢ P = Base G
mirleqb.s ⊢ S = pInv 𝒢 ⁡ G
mirleqb.m ⊢ M = S ⁡ A
mirleqb.g ⊢ φ → G ∈ 𝒢 Tarski
mirleqb.a ⊢ φ → A ∈ P
mirleqb.x ⊢ φ → X ∈ P
mirleqb.y ⊢ φ → Y ∈ P
Assertion mirleqb ⊢ φ → X = Y ↔ M ⁡ X = M ⁡ Y

Proof

Step Hyp Ref Expression
1 mirleqb.p ⊢ P = Base G
2 mirleqb.s ⊢ S = pInv 𝒢 ⁡ G
3 mirleqb.m ⊢ M = S ⁡ A
4 mirleqb.g ⊢ φ → G ∈ 𝒢 Tarski
5 mirleqb.a ⊢ φ → A ∈ P
6 mirleqb.x ⊢ φ → X ∈ P
7 mirleqb.y ⊢ φ → Y ∈ P
8 fveq2 ⊢ X = Y → M ⁡ X = M ⁡ Y
9 8 adantl ⊢ φ ∧ X = Y → M ⁡ X = M ⁡ Y
10 eqid ⊢ dist ⁡ G = dist ⁡ G
11 eqid ⊢ Itv ⁡ G = Itv ⁡ G
12 4 adantr ⊢ φ ∧ M ⁡ X = M ⁡ Y → G ∈ 𝒢 Tarski
13 eqid ⊢ Line 𝒢 ⁡ G = Line 𝒢 ⁡ G
14 1 10 11 13 2 4 5 3 6 mircl ⊢ φ → M ⁡ X ∈ P
15 14 adantr ⊢ φ ∧ M ⁡ X = M ⁡ Y → M ⁡ X ∈ P
16 1 10 11 13 2 4 5 3 7 mircl ⊢ φ → M ⁡ Y ∈ P
17 16 adantr ⊢ φ ∧ M ⁡ X = M ⁡ Y → M ⁡ Y ∈ P
18 6 adantr ⊢ φ ∧ M ⁡ X = M ⁡ Y → X ∈ P
19 7 adantr ⊢ φ ∧ M ⁡ X = M ⁡ Y → Y ∈ P
20 1 10 11 13 2 4 5 3 6 7 miriso ⊢ φ → M ⁡ X dist ⁡ G M ⁡ Y = X dist ⁡ G Y
21 20 adantr ⊢ φ ∧ M ⁡ X = M ⁡ Y → M ⁡ X dist ⁡ G M ⁡ Y = X dist ⁡ G Y
22 simpr ⊢ φ ∧ M ⁡ X = M ⁡ Y → M ⁡ X = M ⁡ Y
23 1 10 11 12 15 17 18 19 21 22 tgcgreq ⊢ φ ∧ M ⁡ X = M ⁡ Y → X = Y
24 9 23 impbida ⊢ φ → X = Y ↔ M ⁡ X = M ⁡ Y