Theorem mirplncl

Description: The mirror of a point with regard to another point is in the same plane as the two points. (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	mirplncl.p	$$⊢P={\mathrm{Base}}_G$$
	mirplncl.h	No typesetting found for |- E = ( PlnG ` G ) with typecode |-
	mirplncl.s	$$⊢S={pInv}_{𝒢}\left(G\right)$$
	mirplncl.1	$$⊢M=S\left(X\right)$$
	mirplncl.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	mirplncl.2	$$⊢\phi \to H\in \mathrm{ran}E$$
	mirplncl.x	$$⊢\phi \to X\in H$$
	mirplncl.y	$$⊢\phi \to Y\in H$$
Assertion	mirplncl	$$⊢\phi \to M\left(Y\right)\in H$$

Proof

Step	Hyp	Ref	Expression
1		mirplncl.p	$$⊢P={\mathrm{Base}}_G$$
2		mirplncl.h	Could not format E = ( PlnG ` G ) : No typesetting found for |- E = ( PlnG ` G ) with typecode |-
3		mirplncl.s	$$⊢S={pInv}_{𝒢}\left(G\right)$$
4		mirplncl.1	$$⊢M=S\left(X\right)$$
5		mirplncl.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
6		mirplncl.2	$$⊢\phi \to H\in \mathrm{ran}E$$
7		mirplncl.x	$$⊢\phi \to X\in H$$
8		mirplncl.y	$$⊢\phi \to Y\in H$$
9		simpr	$$⊢\left(\phi \wedge X=Y\right)\to X=Y$$
10	9	fveq2d	$$⊢\left(\phi \wedge X=Y\right)\to M\left(X\right)=M\left(Y\right)$$
11		eqid	$$⊢\mathrm{dist}\left(G\right)=\mathrm{dist}\left(G\right)$$
12		eqid	$$⊢\mathrm{Itv}\left(G\right)=\mathrm{Itv}\left(G\right)$$
13		eqid	$$⊢{Line}_{𝒢}\left(G\right)={Line}_{𝒢}\left(G\right)$$
14	5	adantr	$$⊢\left(\phi \wedge X=Y\right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
15	1 12 13 2 5 6 7	plngrnssp	$$⊢\phi \to X\in P$$
16	15	adantr	$$⊢\left(\phi \wedge X=Y\right)\to X\in P$$
17	1 11 12 13 3 14 16 4	mircinv	$$⊢\left(\phi \wedge X=Y\right)\to M\left(X\right)=X$$
18	10 17	eqtr3d	$$⊢\left(\phi \wedge X=Y\right)\to M\left(Y\right)=X$$
19	7	adantr	$$⊢\left(\phi \wedge X=Y\right)\to X\in H$$
20	18 19	eqeltrd	$$⊢\left(\phi \wedge X=Y\right)\to M\left(Y\right)\in H$$
21	5	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
22	6	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to H\in \mathrm{ran}E$$
23	7	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to X\in H$$
24	8	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to Y\in H$$
25		simpr	$$⊢\left(\phi \wedge X\ne Y\right)\to X\ne Y$$
26	1 12 13 2 21 22 23 24 25	lnssplng1	$$⊢\left(\phi \wedge X\ne Y\right)\to X{Line}_{𝒢}\left(G\right)Y\subseteq H$$
27	15	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to X\in P$$
28	1 12 13 2 5 6 8	plngrnssp	$$⊢\phi \to Y\in P$$
29	28	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to Y\in P$$
30	1 12 13 21 27 29 25	tgelrnln	$$⊢\left(\phi \wedge X\ne Y\right)\to X{Line}_{𝒢}\left(G\right)Y\in \mathrm{ran}{Line}_{𝒢}\left(G\right)$$
31	1 12 13 21 27 29 25	tglinerflx1	$$⊢\left(\phi \wedge X\ne Y\right)\to X\in \left(X{Line}_{𝒢}\left(G\right)Y\right)$$
32	1 12 13 21 27 29 25	tglinerflx2	$$⊢\left(\phi \wedge X\ne Y\right)\to Y\in \left(X{Line}_{𝒢}\left(G\right)Y\right)$$
33	1 11 12 13 3 21 4 30 31 32	mirln	$$⊢\left(\phi \wedge X\ne Y\right)\to M\left(Y\right)\in \left(X{Line}_{𝒢}\left(G\right)Y\right)$$
34	26 33	sseldd	$$⊢\left(\phi \wedge X\ne Y\right)\to M\left(Y\right)\in H$$
35	20 34	pm2.61dane	$$⊢\phi \to M\left(Y\right)\in H$$