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

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 1 2 3 4 5 6 7 8 lmif ( 𝜑𝑀 : 𝑃𝑃 )
10 9 ffnd ( 𝜑𝑀 Fn 𝑃 )
11 4 adantr ( ( 𝜑𝑏𝑃 ) → 𝐺 ∈ TarskiG )
12 5 adantr ( ( 𝜑𝑏𝑃 ) → 𝐺 DimTarskiG≥ 2 )
13 8 adantr ( ( 𝜑𝑏𝑃 ) → 𝐷 ∈ ran 𝐿 )
14 simpr ( ( 𝜑𝑏𝑃 ) → 𝑏𝑃 )
15 1 2 3 11 12 6 7 13 14 lmilmi ( ( 𝜑𝑏𝑃 ) → ( 𝑀 ‘ ( 𝑀𝑏 ) ) = 𝑏 )
16 15 ralrimiva ( 𝜑 → ∀ 𝑏𝑃 ( 𝑀 ‘ ( 𝑀𝑏 ) ) = 𝑏 )
17 nvocnv ( ( 𝑀 : 𝑃𝑃 ∧ ∀ 𝑏𝑃 ( 𝑀 ‘ ( 𝑀𝑏 ) ) = 𝑏 ) → 𝑀 = 𝑀 )
18 9 16 17 syl2anc ( 𝜑 𝑀 = 𝑀 )
19 nvof1o ( ( 𝑀 Fn 𝑃 𝑀 = 𝑀 ) → 𝑀 : 𝑃1-1-onto𝑃 )
20 10 18 19 syl2anc ( 𝜑𝑀 : 𝑃1-1-onto𝑃 )