Metamath Proof Explorer

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 = ( Base ` G )
mirplncl.h 
|- E = ( PlnG ` G )
mirplncl.s 
|- S = ( pInvG ` G )
mirplncl.1 
|- M = ( S ` X )
mirplncl.g 
|- ( ph -> G e. TarskiG )
mirplncl.2 
|- ( ph -> H e. ran E )
mirplncl.x 
|- ( ph -> X e. H )
mirplncl.y 
|- ( ph -> Y e. H )
Assertion mirplncl 
|- ( ph -> ( M ` Y ) e. H )

Proof

Step Hyp Ref Expression
1 mirplncl.p 
 |-  P = ( Base ` G )
2 mirplncl.h 
 |-  E = ( PlnG ` G )
3 mirplncl.s 
 |-  S = ( pInvG ` G )
4 mirplncl.1 
 |-  M = ( S ` X )
5 mirplncl.g 
 |-  ( ph -> G e. TarskiG )
6 mirplncl.2 
 |-  ( ph -> H e. ran E )
7 mirplncl.x 
 |-  ( ph -> X e. H )
8 mirplncl.y 
 |-  ( ph -> Y e. H )
9 simpr 
 |-  ( ( ph /\ X = Y ) -> X = Y )
10 9 fveq2d 
 |-  ( ( ph /\ X = Y ) -> ( M ` X ) = ( M ` Y ) )
11 eqid 
 |-  ( dist ` G ) = ( dist ` G )
12 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
13 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
14 5 adantr 
 |-  ( ( ph /\ X = Y ) -> G e. TarskiG )
15 1 12 13 2 5 6 7 plngrnssp 
 |-  ( ph -> X e. P )
16 15 adantr 
 |-  ( ( ph /\ X = Y ) -> X e. P )
17 1 11 12 13 3 14 16 4 mircinv 
 |-  ( ( ph /\ X = Y ) -> ( M ` X ) = X )
18 10 17 eqtr3d 
 |-  ( ( ph /\ X = Y ) -> ( M ` Y ) = X )
19 7 adantr 
 |-  ( ( ph /\ X = Y ) -> X e. H )
20 18 19 eqeltrd 
 |-  ( ( ph /\ X = Y ) -> ( M ` Y ) e. H )
21 5 adantr 
 |-  ( ( ph /\ X =/= Y ) -> G e. TarskiG )
22 6 adantr 
 |-  ( ( ph /\ X =/= Y ) -> H e. ran E )
23 7 adantr 
 |-  ( ( ph /\ X =/= Y ) -> X e. H )
24 8 adantr 
 |-  ( ( ph /\ X =/= Y ) -> Y e. H )
25 simpr 
 |-  ( ( ph /\ X =/= Y ) -> X =/= Y )
26 1 12 13 2 21 22 23 24 25 lnssplng1 
 |-  ( ( ph /\ X =/= Y ) -> ( X ( LineG ` G ) Y ) C_ H )
27 15 adantr 
 |-  ( ( ph /\ X =/= Y ) -> X e. P )
28 1 12 13 2 5 6 8 plngrnssp 
 |-  ( ph -> Y e. P )
29 28 adantr 
 |-  ( ( ph /\ X =/= Y ) -> Y e. P )
30 1 12 13 21 27 29 25 tgelrnln 
 |-  ( ( ph /\ X =/= Y ) -> ( X ( LineG ` G ) Y ) e. ran ( LineG ` G ) )
31 1 12 13 21 27 29 25 tglinerflx1 
 |-  ( ( ph /\ X =/= Y ) -> X e. ( X ( LineG ` G ) Y ) )
32 1 12 13 21 27 29 25 tglinerflx2 
 |-  ( ( ph /\ X =/= Y ) -> Y e. ( X ( LineG ` G ) Y ) )
33 1 11 12 13 3 21 4 30 31 32 mirln 
 |-  ( ( ph /\ X =/= Y ) -> ( M ` Y ) e. ( X ( LineG ` G ) Y ) )
34 26 33 sseldd 
 |-  ( ( ph /\ X =/= Y ) -> ( M ` Y ) e. H )
35 20 34 pm2.61dane 
 |-  ( ph -> ( M ` Y ) e. H )