Metamath Proof Explorer

Theorem lmiinv

Description: The invariants of the line mirroring lie on the mirror line. Theorem 10.8 of Schwabhauser p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019)

Ref Expression
Hypotheses ismid.p ⊢ P = Base G
ismid.d ⊢ - ˙ = dist ⁡ G
ismid.i ⊢ I = Itv ⁡ G
ismid.g ⊢ φ → G ∈ 𝒢 Tarski
ismid.1 ⊢ φ → G Dim 𝒢 ≥ 2
lmif.m ⊢ M = lInv 𝒢 ⁡ G ⁡ D
lmif.l ⊢ L = Line 𝒢 ⁡ G
lmif.d ⊢ φ → D ∈ ran ⁡ L
lmicl.1 ⊢ φ → A ∈ P
Assertion lmiinv ⊢ φ → M ⁡ A = A ↔ A ∈ D

Proof

Step Hyp Ref Expression
1 ismid.p ⊢ P = Base G
2 ismid.d ⊢ - ˙ = dist ⁡ G
3 ismid.i ⊢ I = Itv ⁡ G
4 ismid.g ⊢ φ → G ∈ 𝒢 Tarski
5 ismid.1 ⊢ φ → G Dim 𝒢 ≥ 2
6 lmif.m ⊢ M = lInv 𝒢 ⁡ G ⁡ D
7 lmif.l ⊢ L = Line 𝒢 ⁡ G
8 lmif.d ⊢ φ → D ∈ ran ⁡ L
9 lmicl.1 ⊢ φ → A ∈ P
10 1 2 3 4 5 6 7 8 9 9 islmib ⊢ φ → A = M ⁡ A ↔ A mid 𝒢 ⁡ G A ∈ D ∧ D ⟂ 𝒢 ⁡ G A L A ∨ A = A
11 eqcom ⊢ A = M ⁡ A ↔ M ⁡ A = A
12 11 a1i ⊢ φ → A = M ⁡ A ↔ M ⁡ A = A
13 eqidd ⊢ φ → A = A
14 13 olcd ⊢ φ → D ⟂ 𝒢 ⁡ G A L A ∨ A = A
15 14 biantrud ⊢ φ → A mid 𝒢 ⁡ G A ∈ D ↔ A mid 𝒢 ⁡ G A ∈ D ∧ D ⟂ 𝒢 ⁡ G A L A ∨ A = A
16 1 2 3 4 5 9 9 midid ⊢ φ → A mid 𝒢 ⁡ G A = A
17 16 eleq1d ⊢ φ → A mid 𝒢 ⁡ G A ∈ D ↔ A ∈ D
18 15 17 bitr3d ⊢ φ → A mid 𝒢 ⁡ G A ∈ D ∧ D ⟂ 𝒢 ⁡ G A L A ∨ A = A ↔ A ∈ D
19 10 12 18 3bitr3d ⊢ φ → M ⁡ A = A ↔ A ∈ D