Theorem mirmir

Description: The point inversion function is an involution. Theorem 7.7 of Schwabhauser p. 49. (Contributed by Thierry Arnoux, 3-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)$$
	mirmir.b	$$⊢\phi \to B\in P$$
Assertion	mirmir	$$⊢\phi \to M\left(M\left(B\right)\right)=B$$

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		mirmir.b	$$⊢\phi \to B\in P$$
10	1 2 3 4 5 6 7 8 9	mircl	$$⊢\phi \to M\left(B\right)\in P$$
11	1 2 3 4 5 6 7 8 9	mircgr	$$⊢\phi \to A\underset{\dot{}}{-}M\left(B\right)=A\underset{\dot{}}{-}B$$
12	11	eqcomd	$$⊢\phi \to A\underset{\dot{}}{-}B=A\underset{\dot{}}{-}M\left(B\right)$$
13	1 2 3 4 5 6 7 8 9	mirbtwn	$$⊢\phi \to A\in \left(M\left(B\right)IB\right)$$
14	1 2 3 6 10 7 9 13	tgbtwncom	$$⊢\phi \to A\in \left(BIM\left(B\right)\right)$$
15	1 2 3 4 5 6 7 8 10 9 12 14	ismir	$$⊢\phi \to B=M\left(M\left(B\right)\right)$$
16	15	eqcomd	$$⊢\phi \to M\left(M\left(B\right)\right)=B$$