plngmiropp

Description: Given a line A and a point X not on A , then a point Y on the plane defined by A and X is either opposite to X , or opposite to the mirror point of X by any point Z of A . (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	plngmiropp.p	$⊢ P = {Base}_{G}$
	plngmiropp.i	$⊢ I = Itv (G)$
	plngmiropp.l	$⊢ L = {Line}_{𝒢} (G)$
	plngmiropp.e	No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
	plngmiropp.s	$⊢ S = {pInv}_{𝒢} (G)$
	plngmiropp.m	$⊢ M = S (Z)$
	plngmiropp.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b))\}$
	plngmiropp.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	plngmiropp.a	$⊢ φ \to A \in ran L$
	plngmiropp.x	$⊢ φ \to X \in (P ∖ A)$
	plngmiropp.y	$⊢ φ \to Y \in ((A E X) ∖ A)$
	plngmiropp.z	$⊢ φ \to Z \in A$
Assertion	plngmiropp	$⊢ φ \to (X O Y \lor M (X) O Y)$

Proof

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

Metamath Proof Explorer

Theorem plngmiropp

Proof