Theorem mirln

Description: If two points are on the same line, so is the mirror point of one through the other. (Contributed by Thierry Arnoux, 21-Dec-2019)

	Ref	Expression
Hypotheses	mirval.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	mirval.d	⊢ − = ( dist ‘ 𝐺 )
	mirval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	mirval.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	mirval.s	⊢ 𝑆 = ( pInvG ‘ 𝐺 )
	mirval.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	mirln.m	⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
	mirln.1	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
	mirln.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
	mirln.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
Assertion	mirln	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) ∈ 𝐷 )

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		mirln.m	⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
8		mirln.1	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
9		mirln.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
10		mirln.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
11		simpr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
12	11	fveq2d	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝑀 ‘ 𝐴 ) = ( 𝑀 ‘ 𝐵 ) )
13	6	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐺 ∈ TarskiG )
14	1 4 3 6 8 9	tglnpt	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 ∈ 𝑃 )
16	1 2 3 4 5 13 15 7	mircinv	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝑀 ‘ 𝐴 ) = 𝐴 )
17	12 16	eqtr3d	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝑀 ‘ 𝐵 ) = 𝐴 )
18	9	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 ∈ 𝐷 )
19	17 18	eqeltrd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝑀 ‘ 𝐵 ) ∈ 𝐷 )
20	6	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐺 ∈ TarskiG )
21	14	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ 𝑃 )
22	1 4 3 6 8 10	tglnpt	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ 𝑃 )
24	1 2 3 4 5 20 21 7 23	mircl	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( 𝑀 ‘ 𝐵 ) ∈ 𝑃 )
25		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ≠ 𝐵 )
26	1 2 3 4 5 6 14 7 22	mirbtwn	⊢ ( 𝜑 → 𝐴 ∈ ( ( 𝑀 ‘ 𝐵 ) 𝐼 𝐵 ) )
27	26	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ ( ( 𝑀 ‘ 𝐵 ) 𝐼 𝐵 ) )
28	1 3 4 20 21 23 24 25 27	btwnlng2	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( 𝑀 ‘ 𝐵 ) ∈ ( 𝐴 𝐿 𝐵 ) )
29	8	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐷 ∈ ran 𝐿 )
30	9	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ 𝐷 )
31	10	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ 𝐷 )
32	1 3 4 20 21 23 25 25 29 30 31	tglinethru	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐷 = ( 𝐴 𝐿 𝐵 ) )
33	28 32	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( 𝑀 ‘ 𝐵 ) ∈ 𝐷 )
34	19 33	pm2.61dane	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) ∈ 𝐷 )