Metamath Proof Explorer

Theorem prlngsym

Description: Parallelism is symmetric. Theorem 12.5 of Schwabhauser p. 122. (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
prlngsym.1 ⊢ φ → A ∥ ˙ B
Assertion prlngsym ⊢ φ → B ∥ ˙ A

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 prlngsym.1 ⊢ φ → A ∥ ˙ B
6 1 2 3 4 brprlng ⊢ φ → A ∥ ˙ B ↔ A ∈ ran ⁡ L ∧ B ∈ ran ⁡ L ∧ A = B ∨ ∃ h ∈ ran ⁡ E A ⊆ h ∧ B ⊆ h ∧ A ∩ B = ∅
7 5 6 mpbid ⊢ φ → A ∈ ran ⁡ L ∧ B ∈ ran ⁡ L ∧ A = B ∨ ∃ h ∈ ran ⁡ E A ⊆ h ∧ B ⊆ h ∧ A ∩ B = ∅
8 7 simpld ⊢ φ → A ∈ ran ⁡ L ∧ B ∈ ran ⁡ L
9 8 simprd ⊢ φ → B ∈ ran ⁡ L
10 8 simpld ⊢ φ → A ∈ ran ⁡ L
11 eqcom ⊢ A = B ↔ B = A
12 11 bilani ⊢ φ ∧ A = B → B = A
13 ancom ⊢ A ⊆ h ∧ B ⊆ h ↔ B ⊆ h ∧ A ⊆ h
14 13 a1i ⊢ φ → A ⊆ h ∧ B ⊆ h ↔ B ⊆ h ∧ A ⊆ h
15 14 rexbidv ⊢ φ → ∃ h ∈ ran ⁡ E A ⊆ h ∧ B ⊆ h ↔ ∃ h ∈ ran ⁡ E B ⊆ h ∧ A ⊆ h
16 incom ⊢ A ∩ B = B ∩ A
17 16 a1i ⊢ φ → A ∩ B = B ∩ A
18 17 eqeq1d ⊢ φ → A ∩ B = ∅ ↔ B ∩ A = ∅
19 15 18 anbi12d ⊢ φ → ∃ h ∈ ran ⁡ E A ⊆ h ∧ B ⊆ h ∧ A ∩ B = ∅ ↔ ∃ h ∈ ran ⁡ E B ⊆ h ∧ A ⊆ h ∧ B ∩ A = ∅
20 19 biimpa ⊢ φ ∧ ∃ h ∈ ran ⁡ E A ⊆ h ∧ B ⊆ h ∧ A ∩ B = ∅ → ∃ h ∈ ran ⁡ E B ⊆ h ∧ A ⊆ h ∧ B ∩ A = ∅
21 7 simprd ⊢ φ → A = B ∨ ∃ h ∈ ran ⁡ E A ⊆ h ∧ B ⊆ h ∧ A ∩ B = ∅
22 12 20 21 orim12da ⊢ φ → B = A ∨ ∃ h ∈ ran ⁡ E B ⊆ h ∧ A ⊆ h ∧ B ∩ A = ∅
23 9 10 22 jca31 ⊢ φ → B ∈ ran ⁡ L ∧ A ∈ ran ⁡ L ∧ B = A ∨ ∃ h ∈ ran ⁡ E B ⊆ h ∧ A ⊆ h ∧ B ∩ A = ∅
24 1 2 3 4 brprlng ⊢ φ → B ∥ ˙ A ↔ B ∈ ran ⁡ L ∧ A ∈ ran ⁡ L ∧ B = A ∨ ∃ h ∈ ran ⁡ E B ⊆ h ∧ A ⊆ h ∧ B ∩ A = ∅
25 23 24 mpbird ⊢ φ → B ∥ ˙ A