nhpmirhp

Description: If a point Z is on the plane defined by a line A and a point Y , but not on the same half-plane as Y , then its mirror point ( MZ ) by a point X on A is on the same half-plane as Y . (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	nhpmirhp.p	$⊢ P = {Base}_{G}$
	nhpmirhp.l	$⊢ L = {Line}_{𝒢} (G)$
	nhpmirhp.s	$⊢ S = {pInv}_{𝒢} (G)$
	nhpmirhp.e	No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
	nhpmirhp.m	$⊢ M = S (X)$
	nhpmirhp.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	nhpmirhp.a	$⊢ φ \to A \in ran L$
	nhpmirhp.x	$⊢ φ \to X \in A$
	nhpmirhp.y	$⊢ φ \to Y \in (P ∖ A)$
	nhpmirhp.z	$⊢ φ \to Z \in ((A E Y) ∖ A)$
	nhpmirhp.1	$⊢ φ \to \neg Y {hp}_{𝒢} (G) (A) Z$
Assertion	nhpmirhp	$⊢ φ \to Y {hp}_{𝒢} (G) (A) M (Z)$

Proof

Step	Hyp	Ref	Expression
1		nhpmirhp.p	$⊢ P = {Base}_{G}$
2		nhpmirhp.l	$⊢ L = {Line}_{𝒢} (G)$
3		nhpmirhp.s	$⊢ S = {pInv}_{𝒢} (G)$
4		nhpmirhp.e	Could not format E = ( PlnG ` G ) : No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
5		nhpmirhp.m	$⊢ M = S (X)$
6		nhpmirhp.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		nhpmirhp.a	$⊢ φ \to A \in ran L$
8		nhpmirhp.x	$⊢ φ \to X \in A$
9		nhpmirhp.y	$⊢ φ \to Y \in (P ∖ A)$
10		nhpmirhp.z	$⊢ φ \to Z \in ((A E Y) ∖ A)$
11		nhpmirhp.1	$⊢ φ \to \neg Y {hp}_{𝒢} (G) (A) Z$
12		eqid	$⊢ dist (G) = dist (G)$
13		eqid	$⊢ Itv (G) = Itv (G)$
14		eleq1w	$⊢ x = z \to (x \in (P ∖ A) \leftrightarrow z \in (P ∖ A))$
15		eleq1w	$⊢ y = w \to (y \in (P ∖ A) \leftrightarrow w \in (P ∖ A))$
16	14 15	bi2anan9	$⊢ (x = z \land y = w) \to ((x \in (P ∖ A) \land y \in (P ∖ A)) \leftrightarrow (z \in (P ∖ A) \land w \in (P ∖ A)))$
17		oveq12	$⊢ (x = z \land y = w) \to x Itv (G) y = z Itv (G) w$
18	17	eleq2d	$⊢ (x = z \land y = w) \to (s \in (x Itv (G) y) \leftrightarrow s \in (z Itv (G) w))$
19	18	rexbidv	$⊢ (x = z \land y = w) \to (\exists s \in A s \in (x Itv (G) y) \leftrightarrow \exists s \in A s \in (z Itv (G) w))$
20		eleq1w	$⊢ s = t \to (s \in (z Itv (G) w) \leftrightarrow t \in (z Itv (G) w))$
21	20	cbvrexvw	$⊢ \exists s \in A s \in (z Itv (G) w) \leftrightarrow \exists t \in A t \in (z Itv (G) w)$
22	19 21	bitrdi	$⊢ (x = z \land y = w) \to (\exists s \in A s \in (x Itv (G) y) \leftrightarrow \exists t \in A t \in (z Itv (G) w))$
23	16 22	anbi12d	$⊢ (x = z \land y = w) \to (((x \in (P ∖ A) \land y \in (P ∖ A)) \land \exists s \in A s \in (x Itv (G) y)) \leftrightarrow ((z \in (P ∖ A) \land w \in (P ∖ A)) \land \exists t \in A t \in (z Itv (G) w)))$
24	23	cbvopabv	$⊢ \{⟨x, y⟩ \| ((x \in (P ∖ A) \land y \in (P ∖ A)) \land \exists s \in A s \in (x Itv (G) y))\} = \{⟨z, w⟩ \| ((z \in (P ∖ A) \land w \in (P ∖ A)) \land \exists t \in A t \in (z Itv (G) w))\}$
25	10	eldifad	$⊢ φ \to Z \in (A E Y)$
26	1 13 2 4 6 7 9 25	plngssp	$⊢ φ \to Z \in P$
27	1 2 13 6 7 8	tglnpt	$⊢ φ \to X \in P$
28	1 12 13 2 3 6 27 5 26	mircl	$⊢ φ \to M (Z) \in P$
29	10	eldifbd	$⊢ φ \to \neg Z \in A$
30	26 29	eldifd	$⊢ φ \to Z \in (P ∖ A)$
31	1 13 3 5 24 6 7 8 30 2	oppmir	$⊢ φ \to Z \{⟨x, y⟩ \| ((x \in (P ∖ A) \land y \in (P ∖ A)) \land \exists s \in A s \in (x Itv (G) y))\} M (Z)$
32	1 12 13 24 2 7 6 26 28 31	oppcom	$⊢ φ \to M (Z) \{⟨x, y⟩ \| ((x \in (P ∖ A) \land y \in (P ∖ A)) \land \exists s \in A s \in (x Itv (G) y))\} Z$
33	9	eldifad	$⊢ φ \to Y \in P$
34	6	adantr	$⊢ (φ \land Z {hp}_{𝒢} (G) (A) Y) \to G \in 𝒢_{Tarski}$
35	7	adantr	$⊢ (φ \land Z {hp}_{𝒢} (G) (A) Y) \to A \in ran L$
36	26	adantr	$⊢ (φ \land Z {hp}_{𝒢} (G) (A) Y) \to Z \in P$
37	33	adantr	$⊢ (φ \land Z {hp}_{𝒢} (G) (A) Y) \to Y \in P$
38		simpr	$⊢ (φ \land Z {hp}_{𝒢} (G) (A) Y) \to Z {hp}_{𝒢} (G) (A) Y$
39	1 13 2 34 35 36 24 37 38	hpgcom	$⊢ (φ \land Z {hp}_{𝒢} (G) (A) Y) \to Y {hp}_{𝒢} (G) (A) Z$
40	11 39	mtand	$⊢ φ \to \neg Z {hp}_{𝒢} (G) (A) Y$
41	1 13 2 4 6 7 9 24 26	elplng	$⊢ φ \to (Z \in (A E Y) \leftrightarrow (Z \in A \lor Z {hp}_{𝒢} (G) (A) Y \lor Z \{⟨x, y⟩ \| ((x \in (P ∖ A) \land y \in (P ∖ A)) \land \exists s \in A s \in (x Itv (G) y))\} Y))$
42	25 41	mpbid	$⊢ φ \to (Z \in A \lor Z {hp}_{𝒢} (G) (A) Y \lor Z \{⟨x, y⟩ \| ((x \in (P ∖ A) \land y \in (P ∖ A)) \land \exists s \in A s \in (x Itv (G) y))\} Y)$
43	29 40 42	ecase33d	$⊢ φ \to Z \{⟨x, y⟩ \| ((x \in (P ∖ A) \land y \in (P ∖ A)) \land \exists s \in A s \in (x Itv (G) y))\} Y$
44	1 12 13 24 2 7 6 26 33 43	oppcom	$⊢ φ \to Y \{⟨x, y⟩ \| ((x \in (P ∖ A) \land y \in (P ∖ A)) \land \exists s \in A s \in (x Itv (G) y))\} Z$
45	1 13 2 24 6 7 33 28 26 44	lnopp2hpgb	$⊢ φ \to (M (Z) \{⟨x, y⟩ \| ((x \in (P ∖ A) \land y \in (P ∖ A)) \land \exists s \in A s \in (x Itv (G) y))\} Z \leftrightarrow Y {hp}_{𝒢} (G) (A) M (Z))$
46	32 45	mpbid	$⊢ φ \to Y {hp}_{𝒢} (G) (A) M (Z)$

Metamath Proof Explorer

Theorem nhpmirhp

Proof