Theorem mirf1o

Description: The point inversion function M is a bijection. Theorem 7.11 of Schwabhauser p. 50. (Contributed by Thierry Arnoux, 6-Jun-2019)

	Ref	Expression
Hypotheses	mirval.p	$$⊢P={\mathrm{Base}}_G$$
	mirval.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	mirval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	mirval.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	mirval.s	$$⊢S={pInv}_{𝒢}\left(G\right)$$
	mirval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	mirval.a	$$⊢\phi \to A\in P$$
	mirfv.m	$$⊢M=S\left(A\right)$$
Assertion	mirf1o	$$⊢\phi \to M:P\underset{1-1\; onto}{⟶}P$$

Proof

Step	Hyp	Ref	Expression
1		mirval.p	$$⊢P={\mathrm{Base}}_G$$
2		mirval.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		mirval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		mirval.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
5		mirval.s	$$⊢S={pInv}_{𝒢}\left(G\right)$$
6		mirval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
7		mirval.a	$$⊢\phi \to A\in P$$
8		mirfv.m	$$⊢M=S\left(A\right)$$
9	1 2 3 4 5 6 7 8	mirf	$$⊢\phi \to M:P⟶P$$
10	9	ffnd	$$⊢\phi \to MFnP$$
11	6	adantr	$$⊢\left(\phi \wedge a\in P\right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
12	7	adantr	$$⊢\left(\phi \wedge a\in P\right)\to A\in P$$
13		simpr	$$⊢\left(\phi \wedge a\in P\right)\to a\in P$$
14	1 2 3 4 5 11 12 8 13	mirmir	$$⊢\left(\phi \wedge a\in P\right)\to M\left(M\left(a\right)\right)=a$$
15	14	ralrimiva	$$⊢\phi \to \forall a\in PM\left(M\left(a\right)\right)=a$$
16		nvocnv	$$⊢\left(M:P⟶P\wedge \forall a\in PM\left(M\left(a\right)\right)=a\right)\to M^{-1}=M$$
17	9 15 16	syl2anc	$$⊢\phi \to M^{-1}=M$$
18		nvof1o	$$⊢\left(MFnP\wedge M^{-1}=M\right)\to M:P\underset{1-1\; onto}{⟶}P$$
19	10 17 18	syl2anc	$$⊢\phi \to M:P\underset{1-1\; onto}{⟶}P$$