Theorem mirtrcgr

Description: Point inversion of one point of a triangle around another point preserves triangle congruence. (Contributed by Thierry Arnoux, 4-Oct-2020)

	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}}$$
	mirtrcgr.e	$$⊢\underset{\dot{}}{\sim }={\sim }_{𝒢}\left(G\right)$$
	mirtrcgr.m	$$⊢M=S\left(B\right)$$
	mirtrcgr.n	$$⊢N=S\left(Y\right)$$
	mirtrcgr.a	$$⊢\phi \to A\in P$$
	mirtrcgr.b	$$⊢\phi \to B\in P$$
	mirtrcgr.x	$$⊢\phi \to X\in P$$
	mirtrcgr.y	$$⊢\phi \to Y\in P$$
	mirtrcgr.c	$$⊢\phi \to C\in P$$
	mirtrcgr.z	$$⊢\phi \to Z\in P$$
	mirtrcgr.1	$$⊢\phi \to A\ne B$$
	mirtrcgr.2	$$⊢\phi \to ⟨“ABC”⟩\underset{\dot{}}{\sim }⟨“XYZ”⟩$$
Assertion	mirtrcgr	$$⊢\phi \to ⟨“M\left(A\right)BC”⟩\underset{\dot{}}{\sim }⟨“N\left(X\right)YZ”⟩$$

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		mirtrcgr.e	$$⊢\underset{\dot{}}{\sim }={\sim }_{𝒢}\left(G\right)$$
8		mirtrcgr.m	$$⊢M=S\left(B\right)$$
9		mirtrcgr.n	$$⊢N=S\left(Y\right)$$
10		mirtrcgr.a	$$⊢\phi \to A\in P$$
11		mirtrcgr.b	$$⊢\phi \to B\in P$$
12		mirtrcgr.x	$$⊢\phi \to X\in P$$
13		mirtrcgr.y	$$⊢\phi \to Y\in P$$
14		mirtrcgr.c	$$⊢\phi \to C\in P$$
15		mirtrcgr.z	$$⊢\phi \to Z\in P$$
16		mirtrcgr.1	$$⊢\phi \to A\ne B$$
17		mirtrcgr.2	$$⊢\phi \to ⟨“ABC”⟩\underset{\dot{}}{\sim }⟨“XYZ”⟩$$
18	1 2 3 4 5 6 11 8 10	mircl	$$⊢\phi \to M\left(A\right)\in P$$
19	1 2 3 4 5 6 13 9 12	mircl	$$⊢\phi \to N\left(X\right)\in P$$
20	1 2 3 7 6 10 11 14 12 13 15 17	cgr3simp1	$$⊢\phi \to A\underset{\dot{}}{-}B=X\underset{\dot{}}{-}Y$$
21	1 2 3 6 10 11 12 13 20	tgcgrcomlr	$$⊢\phi \to B\underset{\dot{}}{-}A=Y\underset{\dot{}}{-}X$$
22	1 2 3 4 5 6 11 8 10	mircgr	$$⊢\phi \to B\underset{\dot{}}{-}M\left(A\right)=B\underset{\dot{}}{-}A$$
23	1 2 3 4 5 6 13 9 12	mircgr	$$⊢\phi \to Y\underset{\dot{}}{-}N\left(X\right)=Y\underset{\dot{}}{-}X$$
24	21 22 23	3eqtr4d	$$⊢\phi \to B\underset{\dot{}}{-}M\left(A\right)=Y\underset{\dot{}}{-}N\left(X\right)$$
25	1 2 3 6 11 18 13 19 24	tgcgrcomlr	$$⊢\phi \to M\left(A\right)\underset{\dot{}}{-}B=N\left(X\right)\underset{\dot{}}{-}Y$$
26	1 2 3 7 6 10 11 14 12 13 15 17	cgr3simp2	$$⊢\phi \to B\underset{\dot{}}{-}C=Y\underset{\dot{}}{-}Z$$
27	1 2 3 4 5 6 11 8 10	mirbtwn	$$⊢\phi \to B\in \left(M\left(A\right)IA\right)$$
28	1 4 3 6 18 10 11 27	btwncolg1	$$⊢\phi \to \left(B\in \left(M\left(A\right)LA\right)\vee M\left(A\right)=A\right)$$
29	1 4 3 6 18 10 11 28	colcom	$$⊢\phi \to \left(B\in \left(ALM\left(A\right)\right)\vee A=M\left(A\right)\right)$$
30	1 2 3 4 5 6 7 8 9 10 11 12 13 20	mircgrextend	$$⊢\phi \to A\underset{\dot{}}{-}M\left(A\right)=X\underset{\dot{}}{-}N\left(X\right)$$
31	1 2 3 6 10 18 12 19 30	tgcgrcomlr	$$⊢\phi \to M\left(A\right)\underset{\dot{}}{-}A=N\left(X\right)\underset{\dot{}}{-}X$$
32	1 2 7 6 10 11 18 12 13 19 20 24 31	trgcgr	$$⊢\phi \to ⟨“ABM\left(A\right)”⟩\underset{\dot{}}{\sim }⟨“XYN\left(X\right)”⟩$$
33	1 2 3 7 6 10 11 14 12 13 15 17	cgr3simp3	$$⊢\phi \to C\underset{\dot{}}{-}A=Z\underset{\dot{}}{-}X$$
34	1 2 3 6 14 10 15 12 33	tgcgrcomlr	$$⊢\phi \to A\underset{\dot{}}{-}C=X\underset{\dot{}}{-}Z$$
35	1 4 3 6 10 11 18 7 12 13 2 14 19 15 29 32 34 26 16	tgfscgr	$$⊢\phi \to M\left(A\right)\underset{\dot{}}{-}C=N\left(X\right)\underset{\dot{}}{-}Z$$
36	1 2 3 6 18 14 19 15 35	tgcgrcomlr	$$⊢\phi \to C\underset{\dot{}}{-}M\left(A\right)=Z\underset{\dot{}}{-}N\left(X\right)$$
37	1 2 7 6 18 11 14 19 13 15 25 26 36	trgcgr	$$⊢\phi \to ⟨“M\left(A\right)BC”⟩\underset{\dot{}}{\sim }⟨“N\left(X\right)YZ”⟩$$