Theorem mirleqb

Description: Equality theorem for point mirroring. (Contributed by Thierry Arnoux, 13-Jul-2026)

	Ref	Expression
Hypotheses	mirleqb.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	mirleqb.s	⊢ 𝑆 = ( pInvG ‘ 𝐺 )
	mirleqb.m	⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
	mirleqb.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	mirleqb.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	mirleqb.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	mirleqb.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
Assertion	mirleqb	⊢ ( 𝜑 → ( 𝑋 = 𝑌 ↔ ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mirleqb.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		mirleqb.s	⊢ 𝑆 = ( pInvG ‘ 𝐺 )
3		mirleqb.m	⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
4		mirleqb.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		mirleqb.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6		mirleqb.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
7		mirleqb.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
8		fveq2	⊢ ( 𝑋 = 𝑌 → ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑌 ) )
9	8	adantl	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑌 ) )
10		eqid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
11		eqid	⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
12	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑌 ) ) → 𝐺 ∈ TarskiG )
13		eqid	⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
14	1 10 11 13 2 4 5 3 6	mircl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ∈ 𝑃 )
15	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑌 ) ) → ( 𝑀 ‘ 𝑋 ) ∈ 𝑃 )
16	1 10 11 13 2 4 5 3 7	mircl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ∈ 𝑃 )
17	16	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑌 ) ) → ( 𝑀 ‘ 𝑌 ) ∈ 𝑃 )
18	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑌 ) ) → 𝑋 ∈ 𝑃 )
19	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑌 ) ) → 𝑌 ∈ 𝑃 )
20	1 10 11 13 2 4 5 3 6 7	miriso	⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) ( dist ‘ 𝐺 ) ( 𝑀 ‘ 𝑌 ) ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) )
21	20	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑌 ) ) → ( ( 𝑀 ‘ 𝑋 ) ( dist ‘ 𝐺 ) ( 𝑀 ‘ 𝑌 ) ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) )
22		simpr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑌 ) ) → ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑌 ) )
23	1 10 11 12 15 17 18 19 21 22	tgcgreq	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑌 ) ) → 𝑋 = 𝑌 )
24	9 23	impbida	⊢ ( 𝜑 → ( 𝑋 = 𝑌 ↔ ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑌 ) ) )