Metamath Proof Explorer


Theorem mirf

Description: Point inversion as function. (Contributed by Thierry Arnoux, 30-May-2019)

Ref Expression
Hypotheses mirval.p
|- P = ( Base ` G )
mirval.d
|- .- = ( dist ` G )
mirval.i
|- I = ( Itv ` G )
mirval.l
|- L = ( LineG ` G )
mirval.s
|- S = ( pInvG ` G )
mirval.g
|- ( ph -> G e. TarskiG )
mirval.a
|- ( ph -> A e. P )
mirfv.m
|- M = ( S ` A )
Assertion mirf
|- ( ph -> M : P --> P )

Proof

Step Hyp Ref Expression
1 mirval.p
 |-  P = ( Base ` G )
2 mirval.d
 |-  .- = ( dist ` G )
3 mirval.i
 |-  I = ( Itv ` G )
4 mirval.l
 |-  L = ( LineG ` G )
5 mirval.s
 |-  S = ( pInvG ` G )
6 mirval.g
 |-  ( ph -> G e. TarskiG )
7 mirval.a
 |-  ( ph -> A e. P )
8 mirfv.m
 |-  M = ( S ` A )
9 riotaex
 |-  ( iota_ z e. P ( ( A .- z ) = ( A .- y ) /\ A e. ( z I y ) ) ) e. _V
10 9 a1i
 |-  ( ( ph /\ y e. P ) -> ( iota_ z e. P ( ( A .- z ) = ( A .- y ) /\ A e. ( z I y ) ) ) e. _V )
11 1 2 3 4 5 6 7 mirval
 |-  ( ph -> ( S ` A ) = ( y e. P |-> ( iota_ z e. P ( ( A .- z ) = ( A .- y ) /\ A e. ( z I y ) ) ) ) )
12 8 11 syl5eq
 |-  ( ph -> M = ( y e. P |-> ( iota_ z e. P ( ( A .- z ) = ( A .- y ) /\ A e. ( z I y ) ) ) ) )
13 6 adantr
 |-  ( ( ph /\ x e. P ) -> G e. TarskiG )
14 7 adantr
 |-  ( ( ph /\ x e. P ) -> A e. P )
15 simpr
 |-  ( ( ph /\ x e. P ) -> x e. P )
16 1 2 3 4 5 13 14 8 15 mirfv
 |-  ( ( ph /\ x e. P ) -> ( M ` x ) = ( iota_ z e. P ( ( A .- z ) = ( A .- x ) /\ A e. ( z I x ) ) ) )
17 1 2 3 13 15 14 mirreu3
 |-  ( ( ph /\ x e. P ) -> E! z e. P ( ( A .- z ) = ( A .- x ) /\ A e. ( z I x ) ) )
18 riotacl
 |-  ( E! z e. P ( ( A .- z ) = ( A .- x ) /\ A e. ( z I x ) ) -> ( iota_ z e. P ( ( A .- z ) = ( A .- x ) /\ A e. ( z I x ) ) ) e. P )
19 17 18 syl
 |-  ( ( ph /\ x e. P ) -> ( iota_ z e. P ( ( A .- z ) = ( A .- x ) /\ A e. ( z I x ) ) ) e. P )
20 16 19 eqeltrd
 |-  ( ( ph /\ x e. P ) -> ( M ` x ) e. P )
21 10 12 20 fmpt2d
 |-  ( ph -> M : P --> P )