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	|- .- = ( dist ` G )
	ismid.i	|- I = ( Itv ` G )
	ismid.g	|- ( ph -> G e. TarskiG )
	ismid.1	|- ( ph -> G TarskiGDim>= 2 )
	lmif.m	|- M = ( ( lInvG ` G ) ` D )
	lmif.l	|- L = ( LineG ` G )
	lmif.d	|- ( ph -> D e. ran L )
	lmiiso.1	|- ( ph -> A e. P )
	lmiiso.2	|- ( ph -> B e. P )
Assertion	lmiiso	|- ( ph -> ( ( M ` A ) .- ( M ` B ) ) = ( A .- B ) )

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	|- ( ph -> G e. TarskiG )
5		ismid.1	|- ( ph -> G TarskiGDim>= 2 )
6		lmif.m	|- M = ( ( lInvG ` G ) ` D )
7		lmif.l	|- L = ( LineG ` G )
8		lmif.d	|- ( ph -> D e. ran L )
9		lmiiso.1	|- ( ph -> A e. P )
10		lmiiso.2	|- ( ph -> B e. P )
11		eqid	|- ( ( pInvG ` G ) ` ( ( A ( midG ` G ) ( M ` A ) ) ( midG ` G ) ( B ( midG ` G ) ( M ` B ) ) ) ) = ( ( pInvG ` G ) ` ( ( A ( midG ` G ) ( M ` A ) ) ( midG ` G ) ( B ( midG ` G ) ( M ` B ) ) ) )
12		eqid	|- ( ( A ( midG ` G ) ( M ` A ) ) ( midG ` G ) ( B ( midG ` G ) ( M ` B ) ) ) = ( ( A ( midG ` G ) ( M ` A ) ) ( midG ` G ) ( B ( midG ` G ) ( M ` B ) ) )
13	1 2 3 4 5 6 7 8 9 10 11 12	lmiisolem	|- ( ph -> ( ( M ` A ) .- ( M ` B ) ) = ( A .- B ) )