elplng

Description: Elementhood in the plane defined by a line A and a point R . Definition 9.20 of Schwabhauser p. 74. (Contributed by Thierry Arnoux, 17-Jun-2026)

	Ref	Expression
Hypotheses	plngval.p	$⊢ P = {Base}_{G}$
	plngval.i	$⊢ I = Itv (G)$
	plngval.1	$⊢ L = {Line}_{𝒢} (G)$
	plngval.e	No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
	plngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	elplng.a	$⊢ φ \to A \in ran L$
	elplng.r	$⊢ φ \to R \in (P ∖ A)$
	elplng.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b))\}$
	elplng.x	$⊢ φ \to X \in P$
Assertion	elplng	$⊢ φ \to (X \in (A E R) \leftrightarrow (X \in A \lor X {hp}_{𝒢} (G) (A) R \lor X O R))$

Proof

Step	Hyp	Ref	Expression
1		plngval.p	$⊢ P = {Base}_{G}$
2		plngval.i	$⊢ I = Itv (G)$
3		plngval.1	$⊢ L = {Line}_{𝒢} (G)$
4		plngval.e	Could not format E = ( PlnG ` G ) : No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
5		plngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		elplng.a	$⊢ φ \to A \in ran L$
7		elplng.r	$⊢ φ \to R \in (P ∖ A)$
8		elplng.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b))\}$
9		elplng.x	$⊢ φ \to X \in P$
10	1 2 3 4 5 6 7	plngval	$⊢ φ \to A E R = \{x \in P \| (x \in A \lor x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R))\}$
11	10	eleq2d	$⊢ φ \to (X \in (A E R) \leftrightarrow X \in \{x \in P \| (x \in A \lor x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R))\})$
12		eleq1	$⊢ x = X \to (x \in A \leftrightarrow X \in A)$
13		breq1	$⊢ x = X \to (x {hp}_{𝒢} (G) (A) R \leftrightarrow X {hp}_{𝒢} (G) (A) R)$
14		oveq1	$⊢ x = X \to x I R = X I R$
15	14	eleq2d	$⊢ x = X \to (t \in (x I R) \leftrightarrow t \in (X I R))$
16	15	rexbidv	$⊢ x = X \to (\exists t \in A t \in (x I R) \leftrightarrow \exists t \in A t \in (X I R))$
17	12 13 16	3orbi123d	$⊢ x = X \to ((x \in A \lor x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R)) \leftrightarrow (X \in A \lor X {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (X I R)))$
18	17	elrab	$⊢ X \in \{x \in P \| (x \in A \lor x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R))\} \leftrightarrow (X \in P \land (X \in A \lor X {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (X I R)))$
19	11 18	bitrdi	$⊢ φ \to (X \in (A E R) \leftrightarrow (X \in P \land (X \in A \lor X {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (X I R))))$
20	9	biantrurd	$⊢ φ \to ((X \in A \lor X {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (X I R)) \leftrightarrow (X \in P \land (X \in A \lor X {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (X I R))))$
21	7	eldifbd	$⊢ φ \to \neg R \in A$
22	21	anim1ci	$⊢ (φ \land \neg X \in A) \to (\neg X \in A \land \neg R \in A)$
23	22	biantrurd	$⊢ (φ \land \neg X \in A) \to (\exists t \in A t \in (X I R) \leftrightarrow ((\neg X \in A \land \neg R \in A) \land \exists t \in A t \in (X I R)))$
24		eqid	$⊢ dist (G) = dist (G)$
25	9	adantr	$⊢ (φ \land \neg X \in A) \to X \in P$
26	7	eldifad	$⊢ φ \to R \in P$
27	26	adantr	$⊢ (φ \land \neg X \in A) \to R \in P$
28	1 24 2 8 25 27	islnopp	$⊢ (φ \land \neg X \in A) \to (X O R \leftrightarrow ((\neg X \in A \land \neg R \in A) \land \exists t \in A t \in (X I R)))$
29	23 28	bitr4d	$⊢ (φ \land \neg X \in A) \to (\exists t \in A t \in (X I R) \leftrightarrow X O R)$
30	29	orbi2d	$⊢ (φ \land \neg X \in A) \to ((X {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (X I R)) \leftrightarrow (X {hp}_{𝒢} (G) (A) R \lor X O R))$
31	30	pm5.74da	$⊢ φ \to ((\neg X \in A \to (X {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (X I R))) \leftrightarrow (\neg X \in A \to (X {hp}_{𝒢} (G) (A) R \lor X O R)))$
32		df-or	$⊢ (X \in A \lor (X {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (X I R))) \leftrightarrow (\neg X \in A \to (X {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (X I R)))$
33		df-or	$⊢ (X \in A \lor (X {hp}_{𝒢} (G) (A) R \lor X O R)) \leftrightarrow (\neg X \in A \to (X {hp}_{𝒢} (G) (A) R \lor X O R))$
34	31 32 33	3bitr4g	$⊢ φ \to ((X \in A \lor (X {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (X I R))) \leftrightarrow (X \in A \lor (X {hp}_{𝒢} (G) (A) R \lor X O R)))$
35		3orass	$⊢ (X \in A \lor X {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (X I R)) \leftrightarrow (X \in A \lor (X {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (X I R)))$
36		3orass	$⊢ (X \in A \lor X {hp}_{𝒢} (G) (A) R \lor X O R) \leftrightarrow (X \in A \lor (X {hp}_{𝒢} (G) (A) R \lor X O R))$
37	34 35 36	3bitr4g	$⊢ φ \to ((X \in A \lor X {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (X I R)) \leftrightarrow (X \in A \lor X {hp}_{𝒢} (G) (A) R \lor X O R))$
38	19 20 37	3bitr2d	$⊢ φ \to (X \in (A E R) \leftrightarrow (X \in A \lor X {hp}_{𝒢} (G) (A) R \lor X O R))$

Metamath Proof Explorer

Theorem elplng

Proof