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 ⊢ 𝐿 = ( LineG ‘ 𝐺 )
brprlng.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
brprlng.p ⊢ ∥ = ( parlnG ‘ 𝐺 )
brprlng.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
prlngsym.1 ⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
Assertion prlngsym ( 𝜑 → 𝐵 ∥ 𝐴 )

Proof

Step Hyp Ref Expression
1 brprlng.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
2 brprlng.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
3 brprlng.p ⊢ ∥ = ( parlnG ‘ 𝐺 )
4 brprlng.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
5 prlngsym.1 ⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
6 1 2 3 4 brprlng ⊢ ( 𝜑 → ( 𝐴 ∥ 𝐵 ↔ ( ( 𝐴 ∈ ran 𝐿 ∧ 𝐵 ∈ ran 𝐿 ) ∧ ( 𝐴 = 𝐵 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) ) ) )
7 5 6 mpbid ⊢ ( 𝜑 → ( ( 𝐴 ∈ ran 𝐿 ∧ 𝐵 ∈ ran 𝐿 ) ∧ ( 𝐴 = 𝐵 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) ) )
8 7 simpld ⊢ ( 𝜑 → ( 𝐴 ∈ ran 𝐿 ∧ 𝐵 ∈ ran 𝐿 ) )
9 8 simprd ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
10 8 simpld ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
11 eqcom ⊢ ( 𝐴 = 𝐵 ↔ 𝐵 = 𝐴 )
12 11 bilani ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐵 = 𝐴 )
13 ancom ⊢ ( ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ↔ ( 𝐵 ⊆ ℎ ∧ 𝐴 ⊆ ℎ ) )
14 13 a1i ⊢ ( 𝜑 → ( ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ↔ ( 𝐵 ⊆ ℎ ∧ 𝐴 ⊆ ℎ ) ) )
15 14 rexbidv ⊢ ( 𝜑 → ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ↔ ∃ ℎ ∈ ran 𝐸 ( 𝐵 ⊆ ℎ ∧ 𝐴 ⊆ ℎ ) ) )
16 incom ⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
17 16 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 ) )
18 17 eqeq1d ⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ( 𝐵 ∩ 𝐴 ) = ∅ ) )
19 15 18 anbi12d ⊢ ( 𝜑 → ( ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ↔ ( ∃ ℎ ∈ ran 𝐸 ( 𝐵 ⊆ ℎ ∧ 𝐴 ⊆ ℎ ) ∧ ( 𝐵 ∩ 𝐴 ) = ∅ ) ) )
20 19 biimpa ⊢ ( ( 𝜑 ∧ ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) → ( ∃ ℎ ∈ ran 𝐸 ( 𝐵 ⊆ ℎ ∧ 𝐴 ⊆ ℎ ) ∧ ( 𝐵 ∩ 𝐴 ) = ∅ ) )
21 7 simprd ⊢ ( 𝜑 → ( 𝐴 = 𝐵 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) )
22 12 20 21 orim12da ⊢ ( 𝜑 → ( 𝐵 = 𝐴 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝐵 ⊆ ℎ ∧ 𝐴 ⊆ ℎ ) ∧ ( 𝐵 ∩ 𝐴 ) = ∅ ) ) )
23 9 10 22 jca31 ⊢ ( 𝜑 → ( ( 𝐵 ∈ ran 𝐿 ∧ 𝐴 ∈ ran 𝐿 ) ∧ ( 𝐵 = 𝐴 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝐵 ⊆ ℎ ∧ 𝐴 ⊆ ℎ ) ∧ ( 𝐵 ∩ 𝐴 ) = ∅ ) ) ) )
24 1 2 3 4 brprlng ⊢ ( 𝜑 → ( 𝐵 ∥ 𝐴 ↔ ( ( 𝐵 ∈ ran 𝐿 ∧ 𝐴 ∈ ran 𝐿 ) ∧ ( 𝐵 = 𝐴 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝐵 ⊆ ℎ ∧ 𝐴 ⊆ ℎ ) ∧ ( 𝐵 ∩ 𝐴 ) = ∅ ) ) ) ) )
25 23 24 mpbird ⊢ ( 𝜑 → 𝐵 ∥ 𝐴 )