Metamath Proof Explorer

Theorem mirleqb

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

Ref Expression
Hypotheses mirleqb.p 
|- P = ( Base ` G )
mirleqb.s 
|- S = ( pInvG ` G )
mirleqb.m 
|- M = ( S ` A )
mirleqb.g 
|- ( ph -> G e. TarskiG )
mirleqb.a 
|- ( ph -> A e. P )
mirleqb.x 
|- ( ph -> X e. P )
mirleqb.y 
|- ( ph -> Y e. P )
Assertion mirleqb 
|- ( ph -> ( X = Y <-> ( M ` X ) = ( M ` Y ) ) )

Proof

Step Hyp Ref Expression
1 mirleqb.p 
 |-  P = ( Base ` G )
2 mirleqb.s 
 |-  S = ( pInvG ` G )
3 mirleqb.m 
 |-  M = ( S ` A )
4 mirleqb.g 
 |-  ( ph -> G e. TarskiG )
5 mirleqb.a 
 |-  ( ph -> A e. P )
6 mirleqb.x 
 |-  ( ph -> X e. P )
7 mirleqb.y 
 |-  ( ph -> Y e. P )
8 fveq2 
 |-  ( X = Y -> ( M ` X ) = ( M ` Y ) )
9 8 adantl 
 |-  ( ( ph /\ X = Y ) -> ( M ` X ) = ( M ` Y ) )
10 eqid 
 |-  ( dist ` G ) = ( dist ` G )
11 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
12 4 adantr 
 |-  ( ( ph /\ ( M ` X ) = ( M ` Y ) ) -> G e. TarskiG )
13 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
14 1 10 11 13 2 4 5 3 6 mircl 
 |-  ( ph -> ( M ` X ) e. P )
15 14 adantr 
 |-  ( ( ph /\ ( M ` X ) = ( M ` Y ) ) -> ( M ` X ) e. P )
16 1 10 11 13 2 4 5 3 7 mircl 
 |-  ( ph -> ( M ` Y ) e. P )
17 16 adantr 
 |-  ( ( ph /\ ( M ` X ) = ( M ` Y ) ) -> ( M ` Y ) e. P )
18 6 adantr 
 |-  ( ( ph /\ ( M ` X ) = ( M ` Y ) ) -> X e. P )
19 7 adantr 
 |-  ( ( ph /\ ( M ` X ) = ( M ` Y ) ) -> Y e. P )
20 1 10 11 13 2 4 5 3 6 7 miriso 
 |-  ( ph -> ( ( M ` X ) ( dist ` G ) ( M ` Y ) ) = ( X ( dist ` G ) Y ) )
21 20 adantr 
 |-  ( ( ph /\ ( M ` X ) = ( M ` Y ) ) -> ( ( M ` X ) ( dist ` G ) ( M ` Y ) ) = ( X ( dist ` G ) Y ) )
22 simpr 
 |-  ( ( ph /\ ( M ` X ) = ( M ` Y ) ) -> ( M ` X ) = ( M ` Y ) )
23 1 10 11 12 15 17 18 19 21 22 tgcgreq 
 |-  ( ( ph /\ ( M ` X ) = ( M ` Y ) ) -> X = Y )
24 9 23 impbida 
 |-  ( ph -> ( X = Y <-> ( M ` X ) = ( M ` Y ) ) )