Theorem mirinv

Description: The only invariant point of a point inversion Theorem 7.3 of Schwabhauser p. 49, Theorem 7.10 of Schwabhauser p. 50. (Contributed by Thierry Arnoux, 30-Jul-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 )
	mirinv.b	|- ( ph -> B e. P )
Assertion	mirinv	|- ( ph -> ( ( M ` B ) = B <-> 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		mirinv.b	|- ( ph -> B e. P )
10	6	adantr	|- ( ( ph /\ ( M ` B ) = B ) -> G e. TarskiG )
11	9	adantr	|- ( ( ph /\ ( M ` B ) = B ) -> B e. P )
12	7	adantr	|- ( ( ph /\ ( M ` B ) = B ) -> A e. P )
13	1 2 3 4 5 10 12 8 11	mirbtwn	|- ( ( ph /\ ( M ` B ) = B ) -> A e. ( ( M ` B ) I B ) )
14		simpr	|- ( ( ph /\ ( M ` B ) = B ) -> ( M ` B ) = B )
15	14	oveq1d	|- ( ( ph /\ ( M ` B ) = B ) -> ( ( M ` B ) I B ) = ( B I B ) )
16	13 15	eleqtrd	|- ( ( ph /\ ( M ` B ) = B ) -> A e. ( B I B ) )
17	1 2 3 10 11 12 16	axtgbtwnid	|- ( ( ph /\ ( M ` B ) = B ) -> B = A )
18	17	eqcomd	|- ( ( ph /\ ( M ` B ) = B ) -> A = B )
19	6	adantr	|- ( ( ph /\ A = B ) -> G e. TarskiG )
20	7	adantr	|- ( ( ph /\ A = B ) -> A e. P )
21	9	adantr	|- ( ( ph /\ A = B ) -> B e. P )
22		eqidd	|- ( ( ph /\ A = B ) -> ( A .- B ) = ( A .- B ) )
23		simpr	|- ( ( ph /\ A = B ) -> A = B )
24	1 2 3 19 21 21	tgbtwntriv1	|- ( ( ph /\ A = B ) -> B e. ( B I B ) )
25	23 24	eqeltrd	|- ( ( ph /\ A = B ) -> A e. ( B I B ) )
26	1 2 3 4 5 19 20 8 21 21 22 25	ismir	|- ( ( ph /\ A = B ) -> B = ( M ` B ) )
27	26	eqcomd	|- ( ( ph /\ A = B ) -> ( M ` B ) = B )
28	18 27	impbida	|- ( ph -> ( ( M ` B ) = B <-> A = B ) )