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

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		mirval.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8		mirfv.m	⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
9		mirinv.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
10	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) = 𝐵 ) → 𝐺 ∈ TarskiG )
11	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) = 𝐵 ) → 𝐵 ∈ 𝑃 )
12	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) = 𝐵 ) → 𝐴 ∈ 𝑃 )
13	1 2 3 4 5 10 12 8 11	mirbtwn	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) = 𝐵 ) → 𝐴 ∈ ( ( 𝑀 ‘ 𝐵 ) 𝐼 𝐵 ) )
14		simpr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) = 𝐵 ) → ( 𝑀 ‘ 𝐵 ) = 𝐵 )
15	14	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) = 𝐵 ) → ( ( 𝑀 ‘ 𝐵 ) 𝐼 𝐵 ) = ( 𝐵 𝐼 𝐵 ) )
16	13 15	eleqtrd	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) = 𝐵 ) → 𝐴 ∈ ( 𝐵 𝐼 𝐵 ) )
17	1 2 3 10 11 12 16	axtgbtwnid	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) = 𝐵 ) → 𝐵 = 𝐴 )
18	17	eqcomd	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐵 ) = 𝐵 ) → 𝐴 = 𝐵 )
19	6	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐺 ∈ TarskiG )
20	7	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 ∈ 𝑃 )
21	9	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐵 ∈ 𝑃 )
22		eqidd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 − 𝐵 ) )
23		simpr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
24	1 2 3 19 21 21	tgbtwntriv1	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐵 ∈ ( 𝐵 𝐼 𝐵 ) )
25	23 24	eqeltrd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 ∈ ( 𝐵 𝐼 𝐵 ) )
26	1 2 3 4 5 19 20 8 21 21 22 25	ismir	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐵 = ( 𝑀 ‘ 𝐵 ) )
27	26	eqcomd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝑀 ‘ 𝐵 ) = 𝐵 )
28	18 27	impbida	⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐵 ) = 𝐵 ↔ 𝐴 = 𝐵 ) )

Metamath Proof Explorer

Theorem mirinv

Proof