Metamath Proof Explorer

Theorem lmiiso

Description: The line mirroring function is an isometry, i.e. it is conserves congruence. Because it is also a bijection, it is also a motion. Theorem 10.10 of Schwabhauser p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019)

		Ref	Expression
	Hypotheses	ismid.p	$⊢ P = {Base}_{G}$
		ismid.d	$⊢ \underset{˙}{-} = dist (G)$
		ismid.i	$⊢ I = Itv (G)$
		ismid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
		ismid.1	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
		lmif.m	$⊢ M = {lInv}_{𝒢} (G) (D)$
		lmif.l	$⊢ L = {Line}_{𝒢} (G)$
		lmif.d	$⊢ φ \to D \in ran L$
		lmiiso.1	$⊢ φ \to A \in P$
		lmiiso.2	$⊢ φ \to B \in P$
	Assertion	lmiiso	$⊢ φ \to M (A) \underset{˙}{-} M (B) = A \underset{˙}{-} B$

Proof

Step	Hyp	Ref	Expression
1		ismid.p	$⊢ P = {Base}_{G}$
2		ismid.d	$⊢ \underset{˙}{-} = dist (G)$
3		ismid.i	$⊢ I = Itv (G)$
4		ismid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		ismid.1	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
6		lmif.m	$⊢ M = {lInv}_{𝒢} (G) (D)$
7		lmif.l	$⊢ L = {Line}_{𝒢} (G)$
8		lmif.d	$⊢ φ \to D \in ran L$
9		lmiiso.1	$⊢ φ \to A \in P$
10		lmiiso.2	$⊢ φ \to B \in P$
11		eqid	$⊢ {pInv}_{𝒢} (G) ((A {mid}_{𝒢} (G) M (A)) {mid}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B))) = {pInv}_{𝒢} (G) ((A {mid}_{𝒢} (G) M (A)) {mid}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B)))$
12		eqid	$⊢ (A {mid}_{𝒢} (G) M (A)) {mid}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B)) = (A {mid}_{𝒢} (G) M (A)) {mid}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B))$
13	1 2 3 4 5 6 7 8 9 10 11 12	lmiisolem	$⊢ φ \to M (A) \underset{˙}{-} M (B) = A \underset{˙}{-} B$