Theorem lmimot

Description: Line mirroring is a motion of the geometric space. Theorem 10.11 of Schwabhauser p. 90. (Contributed by Thierry Arnoux, 15-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 )
Assertion	lmimot	|- ( ph -> M e. ( G Ismt G ) )

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	1 2 3 4 5 6 7 8	lmif1o	|- ( ph -> M : P -1-1-onto-> P )
10	4	adantr	|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> G e. TarskiG )
11	5	adantr	|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> G TarskiGDim>= 2 )
12	8	adantr	|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> D e. ran L )
13		simprl	|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> a e. P )
14		simprr	|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> b e. P )
15	1 2 3 10 11 6 7 12 13 14	lmiiso	|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( M ` a ) .- ( M ` b ) ) = ( a .- b ) )
16	15	ralrimivva	|- ( ph -> A. a e. P A. b e. P ( ( M ` a ) .- ( M ` b ) ) = ( a .- b ) )
17	1 2	ismot	|- ( G e. TarskiG -> ( M e. ( G Ismt G ) <-> ( M : P -1-1-onto-> P /\ A. a e. P A. b e. P ( ( M ` a ) .- ( M ` b ) ) = ( a .- b ) ) ) )
18	4 17	syl	|- ( ph -> ( M e. ( G Ismt G ) <-> ( M : P -1-1-onto-> P /\ A. a e. P A. b e. P ( ( M ` a ) .- ( M ` b ) ) = ( a .- b ) ) ) )
19	9 16 18	mpbir2and	|- ( ph -> M e. ( G Ismt G ) )