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 𝑃 = ( Base ‘ 𝐺 )
ismid.d = ( dist ‘ 𝐺 )
ismid.i 𝐼 = ( Itv ‘ 𝐺 )
ismid.g ( 𝜑𝐺 ∈ TarskiG )
ismid.1 ( 𝜑𝐺 DimTarskiG≥ 2 )
lmif.m 𝑀 = ( ( lInvG ‘ 𝐺 ) ‘ 𝐷 )
lmif.l 𝐿 = ( LineG ‘ 𝐺 )
lmif.d ( 𝜑𝐷 ∈ ran 𝐿 )
lmiiso.1 ( 𝜑𝐴𝑃 )
lmiiso.2 ( 𝜑𝐵𝑃 )
Assertion lmiiso ( 𝜑 → ( ( 𝑀𝐴 ) ( 𝑀𝐵 ) ) = ( 𝐴 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ismid.p 𝑃 = ( Base ‘ 𝐺 )
2 ismid.d = ( dist ‘ 𝐺 )
3 ismid.i 𝐼 = ( Itv ‘ 𝐺 )
4 ismid.g ( 𝜑𝐺 ∈ TarskiG )
5 ismid.1 ( 𝜑𝐺 DimTarskiG≥ 2 )
6 lmif.m 𝑀 = ( ( lInvG ‘ 𝐺 ) ‘ 𝐷 )
7 lmif.l 𝐿 = ( LineG ‘ 𝐺 )
8 lmif.d ( 𝜑𝐷 ∈ ran 𝐿 )
9 lmiiso.1 ( 𝜑𝐴𝑃 )
10 lmiiso.2 ( 𝜑𝐵𝑃 )
11 eqid ( ( pInvG ‘ 𝐺 ) ‘ ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀𝐴 ) ) ( midG ‘ 𝐺 ) ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀𝐵 ) ) ) ) = ( ( pInvG ‘ 𝐺 ) ‘ ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀𝐴 ) ) ( midG ‘ 𝐺 ) ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀𝐵 ) ) ) )
12 eqid ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀𝐴 ) ) ( midG ‘ 𝐺 ) ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀𝐵 ) ) ) = ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀𝐴 ) ) ( midG ‘ 𝐺 ) ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀𝐵 ) ) )
13 1 2 3 4 5 6 7 8 9 10 11 12 lmiisolem ( 𝜑 → ( ( 𝑀𝐴 ) ( 𝑀𝐵 ) ) = ( 𝐴 𝐵 ) )