Theorem mirreu

Description: Any point has a unique antecedent through point inversion. Theorem 7.8 of Schwabhauser p. 50. (Contributed by Thierry Arnoux, 3-Jun-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 )
	mirmir.b	|- ( ph -> B e. P )
Assertion	mirreu	|- ( ph -> E! a e. P ( M ` a ) = B )

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		mirmir.b	|- ( ph -> B e. P )
10	1 2 3 4 5 6 7 8 9	mircl	|- ( ph -> ( M ` B ) e. P )
11	1 2 3 4 5 6 7 8 9	mirmir	|- ( ph -> ( M ` ( M ` B ) ) = B )
12	6	ad2antrr	|- ( ( ( ph /\ a e. P ) /\ ( M ` a ) = B ) -> G e. TarskiG )
13	7	ad2antrr	|- ( ( ( ph /\ a e. P ) /\ ( M ` a ) = B ) -> A e. P )
14		simplr	|- ( ( ( ph /\ a e. P ) /\ ( M ` a ) = B ) -> a e. P )
15	1 2 3 4 5 12 13 8 14	mirmir	|- ( ( ( ph /\ a e. P ) /\ ( M ` a ) = B ) -> ( M ` ( M ` a ) ) = a )
16		simpr	|- ( ( ( ph /\ a e. P ) /\ ( M ` a ) = B ) -> ( M ` a ) = B )
17	16	fveq2d	|- ( ( ( ph /\ a e. P ) /\ ( M ` a ) = B ) -> ( M ` ( M ` a ) ) = ( M ` B ) )
18	15 17	eqtr3d	|- ( ( ( ph /\ a e. P ) /\ ( M ` a ) = B ) -> a = ( M ` B ) )
19	18	ex	|- ( ( ph /\ a e. P ) -> ( ( M ` a ) = B -> a = ( M ` B ) ) )
20	19	ralrimiva	|- ( ph -> A. a e. P ( ( M ` a ) = B -> a = ( M ` B ) ) )
21		fveqeq2	|- ( a = ( M ` B ) -> ( ( M ` a ) = B <-> ( M ` ( M ` B ) ) = B ) )
22	21	eqreu	|- ( ( ( M ` B ) e. P /\ ( M ` ( M ` B ) ) = B /\ A. a e. P ( ( M ` a ) = B -> a = ( M ` B ) ) ) -> E! a e. P ( M ` a ) = B )
23	10 11 20 22	syl3anc	|- ( ph -> E! a e. P ( M ` a ) = B )