Theorem prlngref

Description: Parallelism is reflexive. Theorem 12.4 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	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
	prlngref.1	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
Assertion	prlngref	⊢ ( 𝜑 → 𝐴 ∥ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		brprlng.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
2		brprlng.e	⊢ 𝐸 = ( hlG ‘ 𝐺 )
3		brprlng.p	⊢ ∥ = ( parlnG ‘ 𝐺 )
4		brprlng.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
5		prlngref.1	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
6	5 5	jca	⊢ ( 𝜑 → ( 𝐴 ∈ ran 𝐿 ∧ 𝐴 ∈ ran 𝐿 ) )
7		eqidd	⊢ ( 𝜑 → 𝐴 = 𝐴 )
8	7	orcd	⊢ ( 𝜑 → ( 𝐴 = 𝐴 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐴 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐴 ) = ∅ ) ) )
9	1 2 3 4	brprlng	⊢ ( 𝜑 → ( 𝐴 ∥ 𝐴 ↔ ( ( 𝐴 ∈ ran 𝐿 ∧ 𝐴 ∈ ran 𝐿 ) ∧ ( 𝐴 = 𝐴 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐴 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐴 ) = ∅ ) ) ) ) )
10	6 8 9	mpbir2and	⊢ ( 𝜑 → 𝐴 ∥ 𝐴 )