Theorem 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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	mirval.d	⊢ − = ( dist ‘ 𝐺 )
	mirval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	mirval.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	mirval.s	⊢ 𝑆 = ( pInvG ‘ 𝐺 )
	mirval.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	mirln2.m	⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
	mirln2.d	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
	mirln2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	mirln2.1	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
	mirln2.2	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) ∈ 𝐷 )
Assertion	mirln2	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		mirval.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		mirval.d	⊢ − = ( dist ‘ 𝐺 )
3		mirval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		mirval.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		mirval.s	⊢ 𝑆 = ( pInvG ‘ 𝐺 )
6		mirval.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7		mirln2.m	⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
8		mirln2.d	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
9		mirln2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
10		mirln2.1	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
11		mirln2.2	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) ∈ 𝐷 )
12	1 4 3 6 8 10	tglnpt	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
13	1 2 3 4 5 6 9 7 12	mirinv	⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐵 ) = 𝐵 ↔ 𝐴 = 𝐵 ) )
14	13	biimpa	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) = 𝐵 ) → 𝐴 = 𝐵 )
15	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) = 𝐵 ) → 𝐵 ∈ 𝐷 )
16	14 15	eqeltrd	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) = 𝐵 ) → 𝐴 ∈ 𝐷 )
17	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) ≠ 𝐵 ) → 𝐺 ∈ TarskiG )
18	1 4 3 6 8 11	tglnpt	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) ∈ 𝑃 )
19	18	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) ≠ 𝐵 ) → ( 𝑀 ‘ 𝐵 ) ∈ 𝑃 )
20	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) ≠ 𝐵 ) → 𝐵 ∈ 𝑃 )
21	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) ≠ 𝐵 ) → 𝐴 ∈ 𝑃 )
22		simpr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) ≠ 𝐵 ) → ( 𝑀 ‘ 𝐵 ) ≠ 𝐵 )
23	1 2 3 4 5 17 21 7 20	mirbtwn	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) ≠ 𝐵 ) → 𝐴 ∈ ( ( 𝑀 ‘ 𝐵 ) 𝐼 𝐵 ) )
24	1 3 4 17 19 20 21 22 23	btwnlng1	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) ≠ 𝐵 ) → 𝐴 ∈ ( ( 𝑀 ‘ 𝐵 ) 𝐿 𝐵 ) )
25	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) ≠ 𝐵 ) → 𝐷 ∈ ran 𝐿 )
26	11	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) ≠ 𝐵 ) → ( 𝑀 ‘ 𝐵 ) ∈ 𝐷 )
27	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) ≠ 𝐵 ) → 𝐵 ∈ 𝐷 )
28	1 3 4 17 19 20 22 22 25 26 27	tglinethru	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) ≠ 𝐵 ) → 𝐷 = ( ( 𝑀 ‘ 𝐵 ) 𝐿 𝐵 ) )
29	24 28	eleqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) ≠ 𝐵 ) → 𝐴 ∈ 𝐷 )
30	16 29	pm2.61dane	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )