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	eqtrid	|- ( 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 )