oppmir

Description: The mirror point with regard to a point X on a line A lies on the other side of A . (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	oppmir.p	$⊢ P = {Base}_{G}$
	oppmir.i	$⊢ I = Itv (G)$
	oppmir.s	$⊢ S = {pInv}_{𝒢} (G)$
	oppmir.m	$⊢ M = S (X)$
	oppmir.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b))\}$
	oppmir.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	oppmir.a	$⊢ φ \to A \in ran L$
	oppmir.x	$⊢ φ \to X \in A$
	oppmir.y	$⊢ φ \to Y \in (P ∖ A)$
	oppmir.1	$⊢ L = {Line}_{𝒢} (G)$
Assertion	oppmir	$⊢ φ \to Y O M (Y)$

Step	Hyp	Ref	Expression
1		oppmir.p	$⊢ P = {Base}_{G}$
2		oppmir.i	$⊢ I = Itv (G)$
3		oppmir.s	$⊢ S = {pInv}_{𝒢} (G)$
4		oppmir.m	$⊢ M = S (X)$
5		oppmir.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b))\}$
6		oppmir.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		oppmir.a	$⊢ φ \to A \in ran L$
8		oppmir.x	$⊢ φ \to X \in A$
9		oppmir.y	$⊢ φ \to Y \in (P ∖ A)$
10		oppmir.1	$⊢ L = {Line}_{𝒢} (G)$
11		eqid	$⊢ dist (G) = dist (G)$
12	9	eldifad	$⊢ φ \to Y \in P$
13	1 10 2 6 7 8	tglnpt	$⊢ φ \to X \in P$
14	1 11 2 10 3 6 13 4 12	mircl	$⊢ φ \to M (Y) \in P$
15	9	eldifbd	$⊢ φ \to \neg Y \in A$
16	1 11 2 10 3 6 13 4 12	mirmir	$⊢ φ \to M (M (Y)) = Y$
17	16	adantr	$⊢ (φ \land M (Y) \in A) \to M (M (Y)) = Y$
18	6	adantr	$⊢ (φ \land M (Y) \in A) \to G \in 𝒢_{Tarski}$
19	7	adantr	$⊢ (φ \land M (Y) \in A) \to A \in ran L$
20	8	adantr	$⊢ (φ \land M (Y) \in A) \to X \in A$
21		simpr	$⊢ (φ \land M (Y) \in A) \to M (Y) \in A$
22	1 11 2 10 3 18 4 19 20 21	mirln	$⊢ (φ \land M (Y) \in A) \to M (M (Y)) \in A$
23	17 22	eqeltrrd	$⊢ (φ \land M (Y) \in A) \to Y \in A$
24	15 23	mtand	$⊢ φ \to \neg M (Y) \in A$
25	1 11 2 10 3 6 13 4 12	mirbtwn	$⊢ φ \to X \in (M (Y) I Y)$
26	1 11 2 6 14 13 12 25	tgbtwncom	$⊢ φ \to X \in (Y I M (Y))$
27	1 11 2 5 12 14 8 15 24 26	islnoppd	$⊢ φ \to Y O M (Y)$

Metamath Proof Explorer