Theorem lmif1o

Description: The line mirroring function M is a bijection. Theorem 10.9 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 )
Assertion	lmif1o	|- ( ph -> M : P -1-1-onto-> P )

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	lmif	|- ( ph -> M : P --> P )
10	9	ffnd	|- ( ph -> M Fn P )
11	4	adantr	|- ( ( ph /\ b e. P ) -> G e. TarskiG )
12	5	adantr	|- ( ( ph /\ b e. P ) -> G TarskiGDim>= 2 )
13	8	adantr	|- ( ( ph /\ b e. P ) -> D e. ran L )
14		simpr	|- ( ( ph /\ b e. P ) -> b e. P )
15	1 2 3 11 12 6 7 13 14	lmilmi	|- ( ( ph /\ b e. P ) -> ( M ` ( M ` b ) ) = b )
16	15	ralrimiva	|- ( ph -> A. b e. P ( M ` ( M ` b ) ) = b )
17		nvocnv	|- ( ( M : P --> P /\ A. b e. P ( M ` ( M ` b ) ) = b ) -> `' M = M )
18	9 16 17	syl2anc	|- ( ph -> `' M = M )
19		nvof1o	|- ( ( M Fn P /\ `' M = M ) -> M : P -1-1-onto-> P )
20	10 18 19	syl2anc	|- ( ph -> M : P -1-1-onto-> P )