Metamath Proof Explorer

Theorem prlngd

Description: Deduce parallelism between two lines A and B . (Contributed by Thierry Arnoux, 18-Jun-2026)

Ref Expression
Hypotheses brprlng.l ⊢ L = Line 𝒢 ⁡ G
brprlng.e No typesetting found for |- E = ( PlnG ` G ) with typecode |-
brprlng.p No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
brprlng.g ⊢ φ → G ∈ V
prlngd.a ⊢ φ → A ∈ ran ⁡ L
prlngd.b ⊢ φ → B ∈ ran ⁡ L
prlngd.h ⊢ φ → H ∈ ran ⁡ E
prlngd.1 ⊢ φ → A ⊆ H
prlngd.2 ⊢ φ → B ⊆ H
prlngd.3 ⊢ φ → A ∩ B = ∅
Assertion prlngd ⊢ φ → A ∥ ˙ B

Proof

Step Hyp Ref Expression
1 brprlng.l ⊢ L = Line 𝒢 ⁡ G
2 brprlng.e Could not format E = ( PlnG ` G ) : No typesetting found for |- E = ( PlnG ` G ) with typecode |-
3 brprlng.p Could not format .|| = ( parlnG ` G ) : No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
4 brprlng.g ⊢ φ → G ∈ V
5 prlngd.a ⊢ φ → A ∈ ran ⁡ L
6 prlngd.b ⊢ φ → B ∈ ran ⁡ L
7 prlngd.h ⊢ φ → H ∈ ran ⁡ E
8 prlngd.1 ⊢ φ → A ⊆ H
9 prlngd.2 ⊢ φ → B ⊆ H
10 prlngd.3 ⊢ φ → A ∩ B = ∅
11 5 6 jca ⊢ φ → A ∈ ran ⁡ L ∧ B ∈ ran ⁡ L
12 sseq2 ⊢ h = H → A ⊆ h ↔ A ⊆ H
13 sseq2 ⊢ h = H → B ⊆ h ↔ B ⊆ H
14 12 13 anbi12d ⊢ h = H → A ⊆ h ∧ B ⊆ h ↔ A ⊆ H ∧ B ⊆ H
15 8 9 jca ⊢ φ → A ⊆ H ∧ B ⊆ H
16 14 7 15 rspcedvdw ⊢ φ → ∃ h ∈ ran ⁡ E A ⊆ h ∧ B ⊆ h
17 16 10 jca ⊢ φ → ∃ h ∈ ran ⁡ E A ⊆ h ∧ B ⊆ h ∧ A ∩ B = ∅
18 17 olcd ⊢ φ → A = B ∨ ∃ h ∈ ran ⁡ E A ⊆ h ∧ B ⊆ h ∧ A ∩ B = ∅
19 1 2 3 4 brprlng ⊢ φ → A ∥ ˙ B ↔ A ∈ ran ⁡ L ∧ B ∈ ran ⁡ L ∧ A = B ∨ ∃ h ∈ ran ⁡ E A ⊆ h ∧ B ⊆ h ∧ A ∩ B = ∅
20 11 18 19 mpbir2and ⊢ φ → A ∥ ˙ B