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 = ( Base ` G )
	mirval.d	|- .- = ( dist ` G )
	mirval.i	|- I = ( Itv ` G )
	mirval.l	|- L = ( LineG ` G )
	mirval.s	|- S = ( pInvG ` G )
	mirval.g	|- ( ph -> G e. TarskiG )
	mirtrcgr.e	|- .~ = ( cgrG ` G )
	mirtrcgr.m	|- M = ( S ` B )
	mirtrcgr.n	|- N = ( S ` Y )
	mirtrcgr.a	|- ( ph -> A e. P )
	mirtrcgr.b	|- ( ph -> B e. P )
	mirtrcgr.x	|- ( ph -> X e. P )
	mirtrcgr.y	|- ( ph -> Y e. P )
	mirtrcgr.c	|- ( ph -> C e. P )
	mirtrcgr.z	|- ( ph -> Z e. P )
	mirtrcgr.1	|- ( ph -> A =/= B )
	mirtrcgr.2	|- ( ph -> <" A B C "> .~ <" X Y Z "> )
Assertion	mirtrcgr	|- ( ph -> <" ( M ` A ) B C "> .~ <" ( N ` X ) Y Z "> )

Proof

Step	Hyp	Ref	Expression
1		mirval.p	|- P = ( Base ` G )
2		mirval.d	|- .- = ( dist ` G )
3		mirval.i	|- I = ( Itv ` G )
4		mirval.l	|- L = ( LineG ` G )
5		mirval.s	|- S = ( pInvG ` G )
6		mirval.g	|- ( ph -> G e. TarskiG )
7		mirtrcgr.e	|- .~ = ( cgrG ` G )
8		mirtrcgr.m	|- M = ( S ` B )
9		mirtrcgr.n	|- N = ( S ` Y )
10		mirtrcgr.a	|- ( ph -> A e. P )
11		mirtrcgr.b	|- ( ph -> B e. P )
12		mirtrcgr.x	|- ( ph -> X e. P )
13		mirtrcgr.y	|- ( ph -> Y e. P )
14		mirtrcgr.c	|- ( ph -> C e. P )
15		mirtrcgr.z	|- ( ph -> Z e. P )
16		mirtrcgr.1	|- ( ph -> A =/= B )
17		mirtrcgr.2	|- ( ph -> <" A B C "> .~ <" X Y Z "> )
18	1 2 3 4 5 6 11 8 10	mircl	|- ( ph -> ( M ` A ) e. P )
19	1 2 3 4 5 6 13 9 12	mircl	|- ( ph -> ( N ` X ) e. P )
20	1 2 3 7 6 10 11 14 12 13 15 17	cgr3simp1	|- ( ph -> ( A .- B ) = ( X .- Y ) )
21	1 2 3 6 10 11 12 13 20	tgcgrcomlr	|- ( ph -> ( B .- A ) = ( Y .- X ) )
22	1 2 3 4 5 6 11 8 10	mircgr	|- ( ph -> ( B .- ( M ` A ) ) = ( B .- A ) )
23	1 2 3 4 5 6 13 9 12	mircgr	|- ( ph -> ( Y .- ( N ` X ) ) = ( Y .- X ) )
24	21 22 23	3eqtr4d	|- ( ph -> ( B .- ( M ` A ) ) = ( Y .- ( N ` X ) ) )
25	1 2 3 6 11 18 13 19 24	tgcgrcomlr	|- ( ph -> ( ( M ` A ) .- B ) = ( ( N ` X ) .- Y ) )
26	1 2 3 7 6 10 11 14 12 13 15 17	cgr3simp2	|- ( ph -> ( B .- C ) = ( Y .- Z ) )
27	1 2 3 4 5 6 11 8 10	mirbtwn	|- ( ph -> B e. ( ( M ` A ) I A ) )
28	1 4 3 6 18 10 11 27	btwncolg1	|- ( ph -> ( B e. ( ( M ` A ) L A ) \/ ( M ` A ) = A ) )
29	1 4 3 6 18 10 11 28	colcom	|- ( ph -> ( B e. ( A L ( M ` A ) ) \/ A = ( M ` A ) ) )
30	1 2 3 4 5 6 7 8 9 10 11 12 13 20	mircgrextend	|- ( ph -> ( A .- ( M ` A ) ) = ( X .- ( N ` X ) ) )
31	1 2 3 6 10 18 12 19 30	tgcgrcomlr	|- ( ph -> ( ( M ` A ) .- A ) = ( ( N ` X ) .- X ) )
32	1 2 7 6 10 11 18 12 13 19 20 24 31	trgcgr	|- ( ph -> <" A B ( M ` A ) "> .~ <" X Y ( N ` X ) "> )
33	1 2 3 7 6 10 11 14 12 13 15 17	cgr3simp3	|- ( ph -> ( C .- A ) = ( Z .- X ) )
34	1 2 3 6 14 10 15 12 33	tgcgrcomlr	|- ( ph -> ( A .- C ) = ( X .- Z ) )
35	1 4 3 6 10 11 18 7 12 13 2 14 19 15 29 32 34 26 16	tgfscgr	|- ( ph -> ( ( M ` A ) .- C ) = ( ( N ` X ) .- Z ) )
36	1 2 3 6 18 14 19 15 35	tgcgrcomlr	|- ( ph -> ( C .- ( M ` A ) ) = ( Z .- ( N ` X ) ) )
37	1 2 7 6 18 11 14 19 13 15 25 26 36	trgcgr	|- ( ph -> <" ( M ` A ) B C "> .~ <" ( N ` X ) Y Z "> )