Theorem mirf

Description: Point inversion as function. (Contributed by Thierry Arnoux, 30-May-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	mirf	$$⊢\phi \to M:P⟶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		riotaex	$$⊢\left(\iota z\in P|\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}y\wedge A\in \left(zIy\right)\right)\right)\in \mathrm{V}$$
10	9	a1i	$$⊢\left(\phi \wedge y\in P\right)\to \left(\iota z\in P|\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}y\wedge A\in \left(zIy\right)\right)\right)\in \mathrm{V}$$
11	1 2 3 4 5 6 7	mirval	$$⊢\phi \to S\left(A\right)=\left(y\in P⟼\left(\iota z\in P|\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}y\wedge A\in \left(zIy\right)\right)\right)\right)$$
12	8 11	eqtrid	$$⊢\phi \to M=\left(y\in P⟼\left(\iota z\in P|\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}y\wedge A\in \left(zIy\right)\right)\right)\right)$$
13	6	adantr	$$⊢\left(\phi \wedge x\in P\right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
14	7	adantr	$$⊢\left(\phi \wedge x\in P\right)\to A\in P$$
15		simpr	$$⊢\left(\phi \wedge x\in P\right)\to x\in P$$
16	1 2 3 4 5 13 14 8 15	mirfv	$$⊢\left(\phi \wedge x\in P\right)\to M\left(x\right)=\left(\iota z\in P|\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}x\wedge A\in \left(zIx\right)\right)\right)$$
17	1 2 3 13 15 14	mirreu3	$$⊢\left(\phi \wedge x\in P\right)\to \exists !z\in P\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}x\wedge A\in \left(zIx\right)\right)$$
18		riotacl	$$⊢\exists !z\in P\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}x\wedge A\in \left(zIx\right)\right)\to \left(\iota z\in P|\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}x\wedge A\in \left(zIx\right)\right)\right)\in P$$
19	17 18	syl	$$⊢\left(\phi \wedge x\in P\right)\to \left(\iota z\in P|\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}x\wedge A\in \left(zIx\right)\right)\right)\in P$$
20	16 19	eqeltrd	$$⊢\left(\phi \wedge x\in P\right)\to M\left(x\right)\in P$$
21	10 12 20	fmpt2d	$$⊢\phi \to M:P⟶P$$