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

Metamath Proof Explorer

Theorem mirln

Proof