dfprlng3

Description: Alternate definition of (strict) parallelism. Theorem 12.7 of Schwabhauser p. 122. (Contributed by Thierry Arnoux, 13-Jul-2026)

	Ref	Expression
Hypotheses	dfprlng2.b	$⊢ P = {Base}_{G}$
	dfprlng2.l	$⊢ L = {Line}_{𝒢} (G)$
	dfprlng2.p	No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
	dfprlng2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	dfprlng2.x	$⊢ φ \to X \in P$
	dfprlng2.y	$⊢ φ \to Y \in (P ∖ \{X\})$
	dfprlng3.a	$⊢ φ \to A \in ran L$
	dfprlng3.1	$⊢ φ \to A \neq X L Y$
Assertion	dfprlng3	$⊢ φ \to (A \underset{˙}{∥} (X L Y) \leftrightarrow (X {hp}_{𝒢} (G) (A) Y \land A \cap (X L Y) = \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		dfprlng2.b	$⊢ P = {Base}_{G}$
2		dfprlng2.l	$⊢ L = {Line}_{𝒢} (G)$
3		dfprlng2.p	Could not format .\|\| = ( parlnG ` G ) : No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
4		dfprlng2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		dfprlng2.x	$⊢ φ \to X \in P$
6		dfprlng2.y	$⊢ φ \to Y \in (P ∖ \{X\})$
7		dfprlng3.a	$⊢ φ \to A \in ran L$
8		dfprlng3.1	$⊢ φ \to A \neq X L Y$
9	4	ad4antr	$⊢ ((((φ \land z \in P) \land w \in P) \land A = z L w) \land z \neq w) \to G \in 𝒢_{Tarski}$
10		simp-4r	$⊢ ((((φ \land z \in P) \land w \in P) \land A = z L w) \land z \neq w) \to z \in P$
11		simpllr	$⊢ ((((φ \land z \in P) \land w \in P) \land A = z L w) \land z \neq w) \to w \in P$
12		simpr	$⊢ ((((φ \land z \in P) \land w \in P) \land A = z L w) \land z \neq w) \to z \neq w$
13	12	necomd	$⊢ ((((φ \land z \in P) \land w \in P) \land A = z L w) \land z \neq w) \to w \neq z$
14	11 13	eldifsnd	$⊢ ((((φ \land z \in P) \land w \in P) \land A = z L w) \land z \neq w) \to w \in (P ∖ \{z\})$
15	5	ad4antr	$⊢ ((((φ \land z \in P) \land w \in P) \land A = z L w) \land z \neq w) \to X \in P$
16	6	ad4antr	$⊢ ((((φ \land z \in P) \land w \in P) \land A = z L w) \land z \neq w) \to Y \in (P ∖ \{X\})$
17		simplr	$⊢ ((((φ \land z \in P) \land w \in P) \land A = z L w) \land z \neq w) \to A = z L w$
18	8	ad4antr	$⊢ ((((φ \land z \in P) \land w \in P) \land A = z L w) \land z \neq w) \to A \neq X L Y$
19	17 18	eqnetrrd	$⊢ ((((φ \land z \in P) \land w \in P) \land A = z L w) \land z \neq w) \to z L w \neq X L Y$
20	1 2 3 9 10 14 15 16 19	dfprlng2	$⊢ ((((φ \land z \in P) \land w \in P) \land A = z L w) \land z \neq w) \to ((z L w) \underset{˙}{∥} (X L Y) \leftrightarrow (X {hp}_{𝒢} (G) (z L w) Y \land (z L w) \cap (X L Y) = \emptyset))$
21	17	breq1d	$⊢ ((((φ \land z \in P) \land w \in P) \land A = z L w) \land z \neq w) \to (A \underset{˙}{∥} (X L Y) \leftrightarrow (z L w) \underset{˙}{∥} (X L Y))$
22	17	fveq2d	$⊢ ((((φ \land z \in P) \land w \in P) \land A = z L w) \land z \neq w) \to {hp}_{𝒢} (G) (A) = {hp}_{𝒢} (G) (z L w)$
23	22	breqd	$⊢ ((((φ \land z \in P) \land w \in P) \land A = z L w) \land z \neq w) \to (X {hp}_{𝒢} (G) (A) Y \leftrightarrow X {hp}_{𝒢} (G) (z L w) Y)$
24	17	ineq1d	$⊢ ((((φ \land z \in P) \land w \in P) \land A = z L w) \land z \neq w) \to A \cap (X L Y) = (z L w) \cap (X L Y)$
25	24	eqeq1d	$⊢ ((((φ \land z \in P) \land w \in P) \land A = z L w) \land z \neq w) \to (A \cap (X L Y) = \emptyset \leftrightarrow (z L w) \cap (X L Y) = \emptyset)$
26	23 25	anbi12d	$⊢ ((((φ \land z \in P) \land w \in P) \land A = z L w) \land z \neq w) \to ((X {hp}_{𝒢} (G) (A) Y \land A \cap (X L Y) = \emptyset) \leftrightarrow (X {hp}_{𝒢} (G) (z L w) Y \land (z L w) \cap (X L Y) = \emptyset))$
27	20 21 26	3bitr4d	$⊢ ((((φ \land z \in P) \land w \in P) \land A = z L w) \land z \neq w) \to (A \underset{˙}{∥} (X L Y) \leftrightarrow (X {hp}_{𝒢} (G) (A) Y \land A \cap (X L Y) = \emptyset))$
28	27	anasss	$⊢ (((φ \land z \in P) \land w \in P) \land (A = z L w \land z \neq w)) \to (A \underset{˙}{∥} (X L Y) \leftrightarrow (X {hp}_{𝒢} (G) (A) Y \land A \cap (X L Y) = \emptyset))$
29		eqid	$⊢ Itv (G) = Itv (G)$
30	1 29 2 4 7	tgisline	$⊢ φ \to \exists z \in P \exists w \in P (A = z L w \land z \neq w)$
31	28 30	r19.29vva	$⊢ φ \to (A \underset{˙}{∥} (X L Y) \leftrightarrow (X {hp}_{𝒢} (G) (A) Y \land A \cap (X L Y) = \emptyset))$

Metamath Proof Explorer

Theorem dfprlng3

Proof