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	$⊢ \underset{˙}{-} = dist (G)$
	mirval.i	$⊢ I = Itv (G)$
	mirval.l	$⊢ L = {Line}_{𝒢} (G)$
	mirval.s	$⊢ S = {pInv}_{𝒢} (G)$
	mirval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	mirval.a	$⊢ φ \to A \in P$
	mirfv.m	$⊢ M = S (A)$
	mirinv.b	$⊢ φ \to B \in P$
Assertion	mirinv	$⊢ φ \to (M (B) = B \leftrightarrow A = B)$

Proof

Step	Hyp	Ref	Expression
1		mirval.p	$⊢ P = {Base}_{G}$
2		mirval.d	$⊢ \underset{˙}{-} = dist (G)$
3		mirval.i	$⊢ I = Itv (G)$
4		mirval.l	$⊢ L = {Line}_{𝒢} (G)$
5		mirval.s	$⊢ S = {pInv}_{𝒢} (G)$
6		mirval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		mirval.a	$⊢ φ \to A \in P$
8		mirfv.m	$⊢ M = S (A)$
9		mirinv.b	$⊢ φ \to B \in P$
10	6	adantr	$⊢ (φ \land M (B) = B) \to G \in 𝒢_{Tarski}$
11	9	adantr	$⊢ (φ \land M (B) = B) \to B \in P$
12	7	adantr	$⊢ (φ \land M (B) = B) \to A \in P$
13	1 2 3 4 5 10 12 8 11	mirbtwn	$⊢ (φ \land M (B) = B) \to A \in (M (B) I B)$
14		simpr	$⊢ (φ \land M (B) = B) \to M (B) = B$
15	14	oveq1d	$⊢ (φ \land M (B) = B) \to M (B) I B = B I B$
16	13 15	eleqtrd	$⊢ (φ \land M (B) = B) \to A \in (B I B)$
17	1 2 3 10 11 12 16	axtgbtwnid	$⊢ (φ \land M (B) = B) \to B = A$
18	17	eqcomd	$⊢ (φ \land M (B) = B) \to A = B$
19	6	adantr	$⊢ (φ \land A = B) \to G \in 𝒢_{Tarski}$
20	7	adantr	$⊢ (φ \land A = B) \to A \in P$
21	9	adantr	$⊢ (φ \land A = B) \to B \in P$
22		eqidd	$⊢ (φ \land A = B) \to A \underset{˙}{-} B = A \underset{˙}{-} B$
23		simpr	$⊢ (φ \land A = B) \to A = B$
24	1 2 3 19 21 21	tgbtwntriv1	$⊢ (φ \land A = B) \to B \in (B I B)$
25	23 24	eqeltrd	$⊢ (φ \land A = B) \to A \in (B I B)$
26	1 2 3 4 5 19 20 8 21 21 22 25	ismir	$⊢ (φ \land A = B) \to B = M (B)$
27	26	eqcomd	$⊢ (φ \land A = B) \to M (B) = B$
28	18 27	impbida	$⊢ φ \to (M (B) = B \leftrightarrow A = B)$

Metamath Proof Explorer

Theorem mirinv

Proof