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={\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$$
	mircgrextend.1	$$⊢\phi \to A\underset{\dot{}}{-}B=X\underset{\dot{}}{-}Y$$
Assertion	mircgrextend	$$⊢\phi \to A\underset{\dot{}}{-}M\left(A\right)=X\underset{\dot{}}{-}N\left(X\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		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		mircgrextend.1	$$⊢\phi \to A\underset{\dot{}}{-}B=X\underset{\dot{}}{-}Y$$
15	1 2 3 4 5 6 11 8 10	mircl	$$⊢\phi \to M\left(A\right)\in P$$
16	1 2 3 4 5 6 13 9 12	mircl	$$⊢\phi \to N\left(X\right)\in P$$
17	1 2 3 4 5 6 11 8 10	mirbtwn	$$⊢\phi \to B\in \left(M\left(A\right)IA\right)$$
18	1 2 3 6 15 11 10 17	tgbtwncom	$$⊢\phi \to B\in \left(AIM\left(A\right)\right)$$
19	1 2 3 4 5 6 13 9 12	mirbtwn	$$⊢\phi \to Y\in \left(N\left(X\right)IX\right)$$
20	1 2 3 6 16 13 12 19	tgbtwncom	$$⊢\phi \to Y\in \left(XIN\left(X\right)\right)$$
21	1 2 3 6 10 11 12 13 14	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 10 11 15 12 13 16 18 20 14 24	tgcgrextend	$$⊢\phi \to A\underset{\dot{}}{-}M\left(A\right)=X\underset{\dot{}}{-}N\left(X\right)$$