Metamath Proof Explorer


Theorem mirf

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

Ref Expression
Hypotheses mirval.p P=BaseG
mirval.d -˙=distG
mirval.i I=ItvG
mirval.l L=Line𝒢G
mirval.s S=pInv𝒢G
mirval.g φG𝒢Tarski
mirval.a φAP
mirfv.m M=SA
Assertion mirf φM:PP

Proof

Step Hyp Ref Expression
1 mirval.p P=BaseG
2 mirval.d -˙=distG
3 mirval.i I=ItvG
4 mirval.l L=Line𝒢G
5 mirval.s S=pInv𝒢G
6 mirval.g φG𝒢Tarski
7 mirval.a φAP
8 mirfv.m M=SA
9 riotaex ιzP|A-˙z=A-˙yAzIyV
10 9 a1i φyPιzP|A-˙z=A-˙yAzIyV
11 1 2 3 4 5 6 7 mirval φSA=yPιzP|A-˙z=A-˙yAzIy
12 8 11 eqtrid φM=yPιzP|A-˙z=A-˙yAzIy
13 6 adantr φxPG𝒢Tarski
14 7 adantr φxPAP
15 simpr φxPxP
16 1 2 3 4 5 13 14 8 15 mirfv φxPMx=ιzP|A-˙z=A-˙xAzIx
17 1 2 3 13 15 14 mirreu3 φxP∃!zPA-˙z=A-˙xAzIx
18 riotacl ∃!zPA-˙z=A-˙xAzIxιzP|A-˙z=A-˙xAzIxP
19 17 18 syl φxPιzP|A-˙z=A-˙xAzIxP
20 16 19 eqeltrd φxPMxP
21 10 12 20 fmpt2d φM:PP