Theorem mirmir2

Description: Point inversion of a point inversion through another point. (Contributed by Thierry Arnoux, 3-Nov-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)$$
	miriso.1	$$⊢\phi \to X\in P$$
	miriso.2	$$⊢\phi \to Y\in P$$
Assertion	mirmir2	$$⊢\phi \to M\left(S\left(Y\right)\left(X\right)\right)=S\left(M\left(Y\right)\right)\left(M\left(X\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		miriso.1	$$⊢\phi \to X\in P$$
10		miriso.2	$$⊢\phi \to Y\in P$$
11	1 2 3 4 5 6 7 8 10	mircl	$$⊢\phi \to M\left(Y\right)\in P$$
12		eqid	$$⊢S\left(M\left(Y\right)\right)=S\left(M\left(Y\right)\right)$$
13	1 2 3 4 5 6 7 8 9	mircl	$$⊢\phi \to M\left(X\right)\in P$$
14		eqid	$$⊢S\left(Y\right)=S\left(Y\right)$$
15	1 2 3 4 5 6 10 14 9	mircl	$$⊢\phi \to S\left(Y\right)\left(X\right)\in P$$
16	1 2 3 4 5 6 7 8 15	mircl	$$⊢\phi \to M\left(S\left(Y\right)\left(X\right)\right)\in P$$
17	1 2 3 4 5 6 10 14 9	mircgr	$$⊢\phi \to Y\underset{\dot{}}{-}S\left(Y\right)\left(X\right)=Y\underset{\dot{}}{-}X$$
18	1 2 3 4 5 6 7 8 10 15 10 9 17	mircgrs	$$⊢\phi \to M\left(Y\right)\underset{\dot{}}{-}M\left(S\left(Y\right)\left(X\right)\right)=M\left(Y\right)\underset{\dot{}}{-}M\left(X\right)$$
19	1 2 3 4 5 6 10 14 9	mirbtwn	$$⊢\phi \to Y\in \left(S\left(Y\right)\left(X\right)IX\right)$$
20	1 2 3 4 5 6 7 8 15 10 9 19	mirbtwni	$$⊢\phi \to M\left(Y\right)\in \left(M\left(S\left(Y\right)\left(X\right)\right)IM\left(X\right)\right)$$
21	1 2 3 4 5 6 11 12 13 16 18 20	ismir	$$⊢\phi \to M\left(S\left(Y\right)\left(X\right)\right)=S\left(M\left(Y\right)\right)\left(M\left(X\right)\right)$$