prlngplngtr

Description: Transitivity of parallelism, for lines in the same plane H . This is case 1 of Theorem 12.15 of Schwabhauser p. 124. (Contributed by Thierry Arnoux, 13-Jul-2026)

	Ref	Expression
Hypotheses	prlngpln4.e	No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
	prlngpln4.p	No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
	prlngpln4.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	prlngpln4.h	$⊢ φ \to H \in ran E$
	prlngpln4.a	$⊢ φ \to A \subseteq H$
	prlngpln4.1	$⊢ φ \to A \underset{˙}{∥} B$
	prlngplngtr.g	$⊢ φ \to G \in 𝒢_{Tarski}^{E}$
	prlngplngtr.c	$⊢ φ \to C \subseteq H$
	prlngplngtr.b	$⊢ φ \to B \underset{˙}{∥} C$
Assertion	prlngplngtr	$⊢ φ \to A \underset{˙}{∥} C$

Proof

Step	Hyp	Ref	Expression
1		prlngpln4.e	Could not format E = ( PlnG ` G ) : No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
2		prlngpln4.p	Could not format .\|\| = ( parlnG ` G ) : No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
3		prlngpln4.g	$⊢ φ \to G \in 𝒢_{Tarski}$
4		prlngpln4.h	$⊢ φ \to H \in ran E$
5		prlngpln4.a	$⊢ φ \to A \subseteq H$
6		prlngpln4.1	$⊢ φ \to A \underset{˙}{∥} B$
7		prlngplngtr.g	$⊢ φ \to G \in 𝒢_{Tarski}^{E}$
8		prlngplngtr.c	$⊢ φ \to C \subseteq H$
9		prlngplngtr.b	$⊢ φ \to B \underset{˙}{∥} C$
10		simpr	$⊢ (φ \land A = C) \to A = C$
11		eqid	$⊢ {Line}_{𝒢} (G) = {Line}_{𝒢} (G)$
12	3	adantr	$⊢ (φ \land A = C) \to G \in 𝒢_{Tarski}$
13	11 2 3 9	prlngrcl2	$⊢ φ \to C \in ran {Line}_{𝒢} (G)$
14	13	adantr	$⊢ (φ \land A = C) \to C \in ran {Line}_{𝒢} (G)$
15	11 1 2 12 14	prlngref	$⊢ (φ \land A = C) \to C \underset{˙}{∥} C$
16	10 15	eqbrtrd	$⊢ (φ \land A = C) \to A \underset{˙}{∥} C$
17	3	adantr	$⊢ (φ \land A \cap C = \emptyset) \to G \in 𝒢_{Tarski}$
18	11 2 3 6	prlngrcl1	$⊢ φ \to A \in ran {Line}_{𝒢} (G)$
19	18	adantr	$⊢ (φ \land A \cap C = \emptyset) \to A \in ran {Line}_{𝒢} (G)$
20	13	adantr	$⊢ (φ \land A \cap C = \emptyset) \to C \in ran {Line}_{𝒢} (G)$
21	4	adantr	$⊢ (φ \land A \cap C = \emptyset) \to H \in ran E$
22	5	adantr	$⊢ (φ \land A \cap C = \emptyset) \to A \subseteq H$
23	8	adantr	$⊢ (φ \land A \cap C = \emptyset) \to C \subseteq H$
24		simpr	$⊢ (φ \land A \cap C = \emptyset) \to A \cap C = \emptyset$
25	11 1 2 17 19 20 21 22 23 24	prlngd	$⊢ (φ \land A \cap C = \emptyset) \to A \underset{˙}{∥} C$
26	25	stoic1a	$⊢ (φ \land \neg A \underset{˙}{∥} C) \to \neg A \cap C = \emptyset$
27	26	neqned	$⊢ (φ \land \neg A \underset{˙}{∥} C) \to A \cap C \neq \emptyset$
28	27	adantlr	$⊢ ((φ \land A \neq C) \land \neg A \underset{˙}{∥} C) \to A \cap C \neq \emptyset$
29		eqid	$⊢ {Base}_{G} = {Base}_{G}$
30	3	ad3antrrr	$⊢ (((φ \land A \neq C) \land \neg A \underset{˙}{∥} C) \land x \in (A \cap C)) \to G \in 𝒢_{Tarski}$
31	11 2 3 9	prlngrcl1	$⊢ φ \to B \in ran {Line}_{𝒢} (G)$
32	31	ad3antrrr	$⊢ (((φ \land A \neq C) \land \neg A \underset{˙}{∥} C) \land x \in (A \cap C)) \to B \in ran {Line}_{𝒢} (G)$
33		eqid	$⊢ Itv (G) = Itv (G)$
34	18	ad3antrrr	$⊢ (((φ \land A \neq C) \land \neg A \underset{˙}{∥} C) \land x \in (A \cap C)) \to A \in ran {Line}_{𝒢} (G)$
35		simpr	$⊢ (((φ \land A \neq C) \land \neg A \underset{˙}{∥} C) \land x \in (A \cap C)) \to x \in (A \cap C)$
36	35	elin1d	$⊢ (((φ \land A \neq C) \land \neg A \underset{˙}{∥} C) \land x \in (A \cap C)) \to x \in A$
37	29 11 33 30 34 36	tglnpt	$⊢ (((φ \land A \neq C) \land \neg A \underset{˙}{∥} C) \land x \in (A \cap C)) \to x \in {Base}_{G}$
38	7	ad3antrrr	$⊢ (((φ \land A \neq C) \land \neg A \underset{˙}{∥} C) \land x \in (A \cap C)) \to G \in 𝒢_{Tarski}^{E}$
39	29 11 2 30 32 37 38	prlngmo2	$⊢ (((φ \land A \neq C) \land \neg A \underset{˙}{∥} C) \land x \in (A \cap C)) \to \exists^{*} a \in ran {Line}_{𝒢} (G) (B \underset{˙}{∥} a \land x \in a)$
40		breq2	$⊢ a = A \to (B \underset{˙}{∥} a \leftrightarrow B \underset{˙}{∥} A)$
41		eleq2w2	$⊢ a = A \to (x \in a \leftrightarrow x \in A)$
42	40 41	anbi12d	$⊢ a = A \to ((B \underset{˙}{∥} a \land x \in a) \leftrightarrow (B \underset{˙}{∥} A \land x \in A))$
43		breq2	$⊢ a = C \to (B \underset{˙}{∥} a \leftrightarrow B \underset{˙}{∥} C)$
44		eleq2w2	$⊢ a = C \to (x \in a \leftrightarrow x \in C)$
45	43 44	anbi12d	$⊢ a = C \to ((B \underset{˙}{∥} a \land x \in a) \leftrightarrow (B \underset{˙}{∥} C \land x \in C))$
46	13	ad3antrrr	$⊢ (((φ \land A \neq C) \land \neg A \underset{˙}{∥} C) \land x \in (A \cap C)) \to C \in ran {Line}_{𝒢} (G)$
47	11 1 2 3 6	prlngsym	$⊢ φ \to B \underset{˙}{∥} A$
48	47	ad3antrrr	$⊢ (((φ \land A \neq C) \land \neg A \underset{˙}{∥} C) \land x \in (A \cap C)) \to B \underset{˙}{∥} A$
49	48 36	jca	$⊢ (((φ \land A \neq C) \land \neg A \underset{˙}{∥} C) \land x \in (A \cap C)) \to (B \underset{˙}{∥} A \land x \in A)$
50	9	ad3antrrr	$⊢ (((φ \land A \neq C) \land \neg A \underset{˙}{∥} C) \land x \in (A \cap C)) \to B \underset{˙}{∥} C$
51	35	elin2d	$⊢ (((φ \land A \neq C) \land \neg A \underset{˙}{∥} C) \land x \in (A \cap C)) \to x \in C$
52	50 51	jca	$⊢ (((φ \land A \neq C) \land \neg A \underset{˙}{∥} C) \land x \in (A \cap C)) \to (B \underset{˙}{∥} C \land x \in C)$
53		simpllr	$⊢ (((φ \land A \neq C) \land \neg A \underset{˙}{∥} C) \land x \in (A \cap C)) \to A \neq C$
54	42 45 34 46 49 52 53	nrmod	$⊢ (((φ \land A \neq C) \land \neg A \underset{˙}{∥} C) \land x \in (A \cap C)) \to \neg \exists^{*} a \in ran {Line}_{𝒢} (G) (B \underset{˙}{∥} a \land x \in a)$
55	39 54	pm2.21fal	$⊢ (((φ \land A \neq C) \land \neg A \underset{˙}{∥} C) \land x \in (A \cap C)) \to ⊥$
56	28 55	n0limd	$⊢ ((φ \land A \neq C) \land \neg A \underset{˙}{∥} C) \to ⊥$
57	56	efald	$⊢ (φ \land A \neq C) \to A \underset{˙}{∥} C$
58	16 57	pm2.61dane	$⊢ φ \to A \underset{˙}{∥} C$

Metamath Proof Explorer

Theorem prlngplngtr

Proof