mirln2

Description: If a point and its mirror point are both on the same line, so is the center of the point inversion. (Contributed by Thierry Arnoux, 3-Mar-2020)

	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 )
	mirln2.m	\|- M = ( S ` A )
	mirln2.d	\|- ( ph -> D e. ran L )
	mirln2.a	\|- ( ph -> A e. P )
	mirln2.1	\|- ( ph -> B e. D )
	mirln2.2	\|- ( ph -> ( M ` B ) e. D )
Assertion	mirln2	\|- ( ph -> A e. D )

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		mirln2.m	\|- M = ( S ` A )
8		mirln2.d	\|- ( ph -> D e. ran L )
9		mirln2.a	\|- ( ph -> A e. P )
10		mirln2.1	\|- ( ph -> B e. D )
11		mirln2.2	\|- ( ph -> ( M ` B ) e. D )
12	1 4 3 6 8 10	tglnpt	\|- ( ph -> B e. P )
13	1 2 3 4 5 6 9 7 12	mirinv	\|- ( ph -> ( ( M ` B ) = B <-> A = B ) )
14	13	biimpa	\|- ( ( ph /\ ( M ` B ) = B ) -> A = B )
15	10	adantr	\|- ( ( ph /\ ( M ` B ) = B ) -> B e. D )
16	14 15	eqeltrd	\|- ( ( ph /\ ( M ` B ) = B ) -> A e. D )
17	6	adantr	\|- ( ( ph /\ ( M ` B ) =/= B ) -> G e. TarskiG )
18	1 4 3 6 8 11	tglnpt	\|- ( ph -> ( M ` B ) e. P )
19	18	adantr	\|- ( ( ph /\ ( M ` B ) =/= B ) -> ( M ` B ) e. P )
20	12	adantr	\|- ( ( ph /\ ( M ` B ) =/= B ) -> B e. P )
21	9	adantr	\|- ( ( ph /\ ( M ` B ) =/= B ) -> A e. P )
22		simpr	\|- ( ( ph /\ ( M ` B ) =/= B ) -> ( M ` B ) =/= B )
23	1 2 3 4 5 17 21 7 20	mirbtwn	\|- ( ( ph /\ ( M ` B ) =/= B ) -> A e. ( ( M ` B ) I B ) )
24	1 3 4 17 19 20 21 22 23	btwnlng1	\|- ( ( ph /\ ( M ` B ) =/= B ) -> A e. ( ( M ` B ) L B ) )
25	8	adantr	\|- ( ( ph /\ ( M ` B ) =/= B ) -> D e. ran L )
26	11	adantr	\|- ( ( ph /\ ( M ` B ) =/= B ) -> ( M ` B ) e. D )
27	10	adantr	\|- ( ( ph /\ ( M ` B ) =/= B ) -> B e. D )
28	1 3 4 17 19 20 22 22 25 26 27	tglinethru	\|- ( ( ph /\ ( M ` B ) =/= B ) -> D = ( ( M ` B ) L B ) )
29	24 28	eleqtrrd	\|- ( ( ph /\ ( M ` B ) =/= B ) -> A e. D )
30	16 29	pm2.61dane	\|- ( ph -> A e. D )

Metamath Proof Explorer

Theorem mirln2

Proof