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

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		mirln2.m	$⊢ M = S (A)$
8		mirln2.d	$⊢ φ \to D \in ran L$
9		mirln2.a	$⊢ φ \to A \in P$
10		mirln2.1	$⊢ φ \to B \in D$
11		mirln2.2	$⊢ φ \to M (B) \in D$
12	1 4 3 6 8 10	tglnpt	$⊢ φ \to B \in P$
13	1 2 3 4 5 6 9 7 12	mirinv	$⊢ φ \to (M (B) = B \leftrightarrow A = B)$
14	13	biimpa	$⊢ (φ \land M (B) = B) \to A = B$
15	10	adantr	$⊢ (φ \land M (B) = B) \to B \in D$
16	14 15	eqeltrd	$⊢ (φ \land M (B) = B) \to A \in D$
17	6	adantr	$⊢ (φ \land M (B) \neq B) \to G \in 𝒢_{Tarski}$
18	1 4 3 6 8 11	tglnpt	$⊢ φ \to M (B) \in P$
19	18	adantr	$⊢ (φ \land M (B) \neq B) \to M (B) \in P$
20	12	adantr	$⊢ (φ \land M (B) \neq B) \to B \in P$
21	9	adantr	$⊢ (φ \land M (B) \neq B) \to A \in P$
22		simpr	$⊢ (φ \land M (B) \neq B) \to M (B) \neq B$
23	1 2 3 4 5 17 21 7 20	mirbtwn	$⊢ (φ \land M (B) \neq B) \to A \in (M (B) I B)$
24	1 3 4 17 19 20 21 22 23	btwnlng1	$⊢ (φ \land M (B) \neq B) \to A \in (M (B) L B)$
25	8	adantr	$⊢ (φ \land M (B) \neq B) \to D \in ran L$
26	11	adantr	$⊢ (φ \land M (B) \neq B) \to M (B) \in D$
27	10	adantr	$⊢ (φ \land M (B) \neq B) \to B \in D$
28	1 3 4 17 19 20 22 22 25 26 27	tglinethru	$⊢ (φ \land M (B) \neq B) \to D = M (B) L B$
29	24 28	eleqtrrd	$⊢ (φ \land M (B) \neq B) \to A \in D$
30	16 29	pm2.61dane	$⊢ φ \to A \in D$

Metamath Proof Explorer

Theorem mirln2

Proof