Metamath Proof Explorer


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 φ G 𝒢 Tarski
ismid.1 φ G Dim 𝒢 2
lmif.m M = lInv 𝒢 G D
lmif.l L = Line 𝒢 G
lmif.d φ D ran L
Assertion lmif1o φ 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 φ G 𝒢 Tarski
5 ismid.1 φ G Dim 𝒢 2
6 lmif.m M = lInv 𝒢 G D
7 lmif.l L = Line 𝒢 G
8 lmif.d φ D ran L
9 1 2 3 4 5 6 7 8 lmif φ M : P P
10 9 ffnd φ M Fn P
11 4 adantr φ b P G 𝒢 Tarski
12 5 adantr φ b P G Dim 𝒢 2
13 8 adantr φ b P D ran L
14 simpr φ b P b P
15 1 2 3 11 12 6 7 13 14 lmilmi φ b P M M b = b
16 15 ralrimiva φ b P M M b = b
17 nvocnv M : P P b P M M b = b M -1 = M
18 9 16 17 syl2anc φ M -1 = M
19 nvof1o M Fn P M -1 = M M : P 1-1 onto P
20 10 18 19 syl2anc φ M : P 1-1 onto P