Theorem mirfv

Description: Value of the point inversion function M . Definition 7.5 of Schwabhauser p. 49. (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)$$
	mirfv.b	$$⊢\phi \to B\in P$$
Assertion	mirfv	$$⊢\phi \to M\left(B\right)=\left(\iota z\in P|\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}B\wedge A\in \left(zIB\right)\right)\right)$$

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		mirfv.b	$$⊢\phi \to B\in P$$
10	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)$$
11	8 10	syl5eq	$$⊢\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)$$
12		simplr	$$⊢\left(\left(\phi \wedge y=B\right)\wedge z\in P\right)\to y=B$$
13	12	oveq2d	$$⊢\left(\left(\phi \wedge y=B\right)\wedge z\in P\right)\to A\underset{\dot{}}{-}y=A\underset{\dot{}}{-}B$$
14	13	eqeq2d	$$⊢\left(\left(\phi \wedge y=B\right)\wedge z\in P\right)\to \left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}y\leftrightarrow A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}B\right)$$
15	12	oveq2d	$$⊢\left(\left(\phi \wedge y=B\right)\wedge z\in P\right)\to zIy=zIB$$
16	15	eleq2d	$$⊢\left(\left(\phi \wedge y=B\right)\wedge z\in P\right)\to \left(A\in \left(zIy\right)\leftrightarrow A\in \left(zIB\right)\right)$$
17	14 16	anbi12d	$$⊢\left(\left(\phi \wedge y=B\right)\wedge z\in P\right)\to \left(\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}y\wedge A\in \left(zIy\right)\right)\leftrightarrow \left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}B\wedge A\in \left(zIB\right)\right)\right)$$
18	17	riotabidva	$$⊢\left(\phi \wedge y=B\right)\to \left(\iota z\in P|\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}y\wedge A\in \left(zIy\right)\right)\right)=\left(\iota z\in P|\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}B\wedge A\in \left(zIB\right)\right)\right)$$
19		riotaex	$$⊢\left(\iota z\in P|\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}B\wedge A\in \left(zIB\right)\right)\right)\in \mathrm{V}$$
20	19	a1i	$$⊢\phi \to \left(\iota z\in P|\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}B\wedge A\in \left(zIB\right)\right)\right)\in \mathrm{V}$$
21	11 18 9 20	fvmptd	$$⊢\phi \to M\left(B\right)=\left(\iota z\in P|\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}B\wedge A\in \left(zIB\right)\right)\right)$$