Definition df-prlng

Description: Define the parallel relation for lines. Definition 12.2 of Schwabhauser p. 121. Note that the textbook first defines a "strict" parallelism where equal lines are not considered parallel in the strict sense: here we jump directly to the more common definition which allows equality. (Contributed by Thierry Arnoux, 17-Jun-2026)

	Ref	Expression
Assertion	df-prlng	⊢ parlnG = ( 𝑔 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ∧ ( 𝑎 = 𝑏 ∨ ( ∃ ℎ ∈ ran ( hlG ‘ 𝑔 ) ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprlng	⊢ parlnG
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		va	⊢ 𝑎
4		vb	⊢ 𝑏
5	3	cv	⊢ 𝑎
6		clng	⊢ LineG
7	1	cv	⊢ 𝑔
8	7 6	cfv	⊢ ( LineG ‘ 𝑔 )
9	8	crn	⊢ ran ( LineG ‘ 𝑔 )
10	5 9	wcel	⊢ 𝑎 ∈ ran ( LineG ‘ 𝑔 )
11	4	cv	⊢ 𝑏
12	11 9	wcel	⊢ 𝑏 ∈ ran ( LineG ‘ 𝑔 )
13	10 12	wa	⊢ ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) )
14	5 11	wceq	⊢ 𝑎 = 𝑏
15		vh	⊢ ℎ
16		cplng	⊢ hlG
17	7 16	cfv	⊢ ( hlG ‘ 𝑔 )
18	17	crn	⊢ ran ( hlG ‘ 𝑔 )
19	15	cv	⊢ ℎ
20	5 19	wss	⊢ 𝑎 ⊆ ℎ
21	11 19	wss	⊢ 𝑏 ⊆ ℎ
22	20 21	wa	⊢ ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ )
23	22 15 18	wrex	⊢ ∃ ℎ ∈ ran ( hlG ‘ 𝑔 ) ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ )
24	5 11	cin	⊢ ( 𝑎 ∩ 𝑏 )
25		c0	⊢ ∅
26	24 25	wceq	⊢ ( 𝑎 ∩ 𝑏 ) = ∅
27	23 26	wa	⊢ ( ∃ ℎ ∈ ran ( hlG ‘ 𝑔 ) ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ )
28	14 27	wo	⊢ ( 𝑎 = 𝑏 ∨ ( ∃ ℎ ∈ ran ( hlG ‘ 𝑔 ) ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) )
29	13 28	wa	⊢ ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ∧ ( 𝑎 = 𝑏 ∨ ( ∃ ℎ ∈ ran ( hlG ‘ 𝑔 ) ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ) )
30	29 3 4	copab	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ∧ ( 𝑎 = 𝑏 ∨ ( ∃ ℎ ∈ ran ( hlG ‘ 𝑔 ) ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ) ) }
31	1 2 30	cmpt	⊢ ( 𝑔 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ∧ ( 𝑎 = 𝑏 ∨ ( ∃ ℎ ∈ ran ( hlG ‘ 𝑔 ) ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ) ) } )
32	0 31	wceq	⊢ parlnG = ( 𝑔 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ∧ ( 𝑎 = 𝑏 ∨ ( ∃ ℎ ∈ ran ( hlG ‘ 𝑔 ) ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ) ) } )