Theorem mircgrextend

Description: Link congruence over a pair of mirror points. cf tgcgrextend . (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 )
	mircgrextend.1	|- ( ph -> ( A .- B ) = ( X .- Y ) )
Assertion	mircgrextend	|- ( ph -> ( A .- ( M ` A ) ) = ( X .- ( N ` X ) ) )

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		mircgrextend.1	|- ( ph -> ( A .- B ) = ( X .- Y ) )
15	1 2 3 4 5 6 11 8 10	mircl	|- ( ph -> ( M ` A ) e. P )
16	1 2 3 4 5 6 13 9 12	mircl	|- ( ph -> ( N ` X ) e. P )
17	1 2 3 4 5 6 11 8 10	mirbtwn	|- ( ph -> B e. ( ( M ` A ) I A ) )
18	1 2 3 6 15 11 10 17	tgbtwncom	|- ( ph -> B e. ( A I ( M ` A ) ) )
19	1 2 3 4 5 6 13 9 12	mirbtwn	|- ( ph -> Y e. ( ( N ` X ) I X ) )
20	1 2 3 6 16 13 12 19	tgbtwncom	|- ( ph -> Y e. ( X I ( N ` X ) ) )
21	1 2 3 6 10 11 12 13 14	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 10 11 15 12 13 16 18 20 14 24	tgcgrextend	|- ( ph -> ( A .- ( M ` A ) ) = ( X .- ( N ` X ) ) )