Theorem mirauto

Description: Point inversion preserves point inversion. (Contributed by Thierry Arnoux, 30-Jul-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}}$$
	mirauto.m	$$⊢M=S\left(T\right)$$
	mirauto.x	$$⊢X=M\left(A\right)$$
	mirauto.y	$$⊢Y=M\left(B\right)$$
	mirauto.z	$$⊢Z=M\left(C\right)$$
	mirauto.0	$$⊢\phi \to T\in P$$
	mirauto.1	$$⊢\phi \to A\in P$$
	mirauto.2	$$⊢\phi \to B\in P$$
	mirauto.3	$$⊢\phi \to C\in P$$
	mirauto.4	$$⊢\phi \to S\left(A\right)\left(B\right)=C$$
Assertion	mirauto	$$⊢\phi \to S\left(X\right)\left(Y\right)=Z$$

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		mirauto.m	$$⊢M=S\left(T\right)$$
8		mirauto.x	$$⊢X=M\left(A\right)$$
9		mirauto.y	$$⊢Y=M\left(B\right)$$
10		mirauto.z	$$⊢Z=M\left(C\right)$$
11		mirauto.0	$$⊢\phi \to T\in P$$
12		mirauto.1	$$⊢\phi \to A\in P$$
13		mirauto.2	$$⊢\phi \to B\in P$$
14		mirauto.3	$$⊢\phi \to C\in P$$
15		mirauto.4	$$⊢\phi \to S\left(A\right)\left(B\right)=C$$
16	1 2 3 4 5 6 11 7	mirf	$$⊢\phi \to M:P⟶P$$
17	16 12	ffvelrnd	$$⊢\phi \to M\left(A\right)\in P$$
18	8 17	eqeltrid	$$⊢\phi \to X\in P$$
19		eqid	$$⊢S\left(X\right)=S\left(X\right)$$
20	16 13	ffvelrnd	$$⊢\phi \to M\left(B\right)\in P$$
21	9 20	eqeltrid	$$⊢\phi \to Y\in P$$
22	16 14	ffvelrnd	$$⊢\phi \to M\left(C\right)\in P$$
23	10 22	eqeltrid	$$⊢\phi \to Z\in P$$
24	15 14	eqeltrd	$$⊢\phi \to S\left(A\right)\left(B\right)\in P$$
25		eqid	$$⊢S\left(A\right)=S\left(A\right)$$
26	1 2 3 4 5 6 12 25 13	mircgr	$$⊢\phi \to A\underset{\dot{}}{-}S\left(A\right)\left(B\right)=A\underset{\dot{}}{-}B$$
27	1 2 3 4 5 6 11 7 12 24 12 13 26	mircgrs	$$⊢\phi \to M\left(A\right)\underset{\dot{}}{-}M\left(S\left(A\right)\left(B\right)\right)=M\left(A\right)\underset{\dot{}}{-}M\left(B\right)$$
28	8	a1i	$$⊢\phi \to X=M\left(A\right)$$
29	15	fveq2d	$$⊢\phi \to M\left(S\left(A\right)\left(B\right)\right)=M\left(C\right)$$
30	10 29	eqtr4id	$$⊢\phi \to Z=M\left(S\left(A\right)\left(B\right)\right)$$
31	28 30	oveq12d	$$⊢\phi \to X\underset{\dot{}}{-}Z=M\left(A\right)\underset{\dot{}}{-}M\left(S\left(A\right)\left(B\right)\right)$$
32	8 9	oveq12i	$$⊢X\underset{\dot{}}{-}Y=M\left(A\right)\underset{\dot{}}{-}M\left(B\right)$$
33	32	a1i	$$⊢\phi \to X\underset{\dot{}}{-}Y=M\left(A\right)\underset{\dot{}}{-}M\left(B\right)$$
34	27 31 33	3eqtr4d	$$⊢\phi \to X\underset{\dot{}}{-}Z=X\underset{\dot{}}{-}Y$$
35	1 2 3 4 5 6 12 25 13	mirbtwn	$$⊢\phi \to A\in \left(S\left(A\right)\left(B\right)IB\right)$$
36	15	oveq1d	$$⊢\phi \to S\left(A\right)\left(B\right)IB=CIB$$
37	35 36	eleqtrd	$$⊢\phi \to A\in \left(CIB\right)$$
38	1 2 3 4 5 6 11 7 14 12 13 37	mirbtwni	$$⊢\phi \to M\left(A\right)\in \left(M\left(C\right)IM\left(B\right)\right)$$
39	10 9	oveq12i	$$⊢ZIY=M\left(C\right)IM\left(B\right)$$
40	38 8 39	3eltr4g	$$⊢\phi \to X\in \left(ZIY\right)$$
41	1 2 3 4 5 6 18 19 21 23 34 40	ismir	$$⊢\phi \to Z=S\left(X\right)\left(Y\right)$$
42	41	eqcomd	$$⊢\phi \to S\left(X\right)\left(Y\right)=Z$$