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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
mirplncl.h ⊢ 𝐸 = ( hlG ‘ 𝐺 )
mirplncl.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
mirplncl.1 ⊢ 𝑀 = ( 𝑆 ‘ 𝑋 )
mirplncl.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
mirplncl.2 ⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
mirplncl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐻 )
mirplncl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐻 )
Assertion mirplncl ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ∈ 𝐻 )

Proof

Step Hyp Ref Expression
1 mirplncl.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 mirplncl.h ⊢ 𝐸 = ( hlG ‘ 𝐺 )
3 mirplncl.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
4 mirplncl.1 ⊢ 𝑀 = ( 𝑆 ‘ 𝑋 )
5 mirplncl.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 mirplncl.2 ⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
7 mirplncl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐻 )
8 mirplncl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐻 )
9 simpr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 = 𝑌 )
10 9 fveq2d ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑌 ) )
11 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
12 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
13 eqid ⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
14 5 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝐺 ∈ TarskiG )
15 1 12 13 2 5 6 7 plngrnssp ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 ∈ 𝑃 )
17 1 11 12 13 3 14 16 4 mircinv ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝑀 ‘ 𝑋 ) = 𝑋 )
18 10 17 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝑀 ‘ 𝑌 ) = 𝑋 )
19 7 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 ∈ 𝐻 )
20 18 19 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝑀 ‘ 𝑌 ) ∈ 𝐻 )
21 5 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝐺 ∈ TarskiG )
22 6 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝐻 ∈ ran 𝐸 )
23 7 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ∈ 𝐻 )
24 8 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑌 ∈ 𝐻 )
25 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ≠ 𝑌 )
26 1 12 13 2 21 22 23 24 25 lnssplng1 ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 ( LineG ‘ 𝐺 ) 𝑌 ) ⊆ 𝐻 )
27 15 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ∈ 𝑃 )
28 1 12 13 2 5 6 8 plngrnssp ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑌 ∈ 𝑃 )
30 1 12 13 21 27 29 25 tgelrnln ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 ( LineG ‘ 𝐺 ) 𝑌 ) ∈ ran ( LineG ‘ 𝐺 ) )
31 1 12 13 21 27 29 25 tglinerflx1 ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ∈ ( 𝑋 ( LineG ‘ 𝐺 ) 𝑌 ) )
32 1 12 13 21 27 29 25 tglinerflx2 ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑌 ∈ ( 𝑋 ( LineG ‘ 𝐺 ) 𝑌 ) )
33 1 11 12 13 3 21 4 30 31 32 mirln ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑀 ‘ 𝑌 ) ∈ ( 𝑋 ( LineG ‘ 𝐺 ) 𝑌 ) )
34 26 33 sseldd ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑀 ‘ 𝑌 ) ∈ 𝐻 )
35 20 34 pm2.61dane ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ∈ 𝐻 )