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	Could not format assertion : No typesetting found for |- parlnG = ( g e. _V |-> { <. a , b >. | ( ( a e. ran ( LineG ` g ) /\ b e. ran ( LineG ` g ) ) /\ ( a = b \/ ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) ) ) } ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprlng	Could not format parlnG : No typesetting found for class parlnG with typecode class
1		vg	$$setvarg$$
2		cvv	$$class\mathrm{V}$$
3		va	$$setvara$$
4		vb	$$setvarb$$
5	3	cv	$$setvara$$
6		clng	$$class{Line}_{𝒢}$$
7	1	cv	$$setvarg$$
8	7 6	cfv	$$class{Line}_{𝒢}\left(g\right)$$
9	8	crn	$$class\mathrm{ran}{Line}_{𝒢}\left(g\right)$$
10	5 9	wcel	$$wffa\in \mathrm{ran}{Line}_{𝒢}\left(g\right)$$
11	4	cv	$$setvarb$$
12	11 9	wcel	$$wffb\in \mathrm{ran}{Line}_{𝒢}\left(g\right)$$
13	10 12	wa	$$wff\left(a\in \mathrm{ran}{Line}_{𝒢}\left(g\right)\wedge b\in \mathrm{ran}{Line}_{𝒢}\left(g\right)\right)$$
14	5 11	wceq	$$wffa=b$$
15		vh	$$setvarh$$
16		cplng	Could not format PlnG : No typesetting found for class PlnG with typecode class
17	7 16	cfv	Could not format ( PlnG ` g ) : No typesetting found for class ( PlnG ` g ) with typecode class
18	17	crn	Could not format ran ( PlnG ` g ) : No typesetting found for class ran ( PlnG ` g ) with typecode class
19	15	cv	$$setvarh$$
20	5 19	wss	$$wffa\subseteq h$$
21	11 19	wss	$$wffb\subseteq h$$
22	20 21	wa	$$wff\left(a\subseteq h\wedge b\subseteq h\right)$$
23	22 15 18	wrex	Could not format E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) : No typesetting found for wff E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) with typecode wff
24	5 11	cin	$$class\left(a\cap b\right)$$
25		c0	$$class\varnothing$$
26	24 25	wceq	$$wffa\cap b=\varnothing$$
27	23 26	wa	Could not format ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) : No typesetting found for wff ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) with typecode wff
28	14 27	wo	Could not format ( a = b \/ ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) ) : No typesetting found for wff ( a = b \/ ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) ) with typecode wff
29	13 28	wa	Could not format ( ( a e. ran ( LineG ` g ) /\ b e. ran ( LineG ` g ) ) /\ ( a = b \/ ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) ) ) : No typesetting found for wff ( ( a e. ran ( LineG ` g ) /\ b e. ran ( LineG ` g ) ) /\ ( a = b \/ ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) ) ) with typecode wff
30	29 3 4	copab	Could not format { <. a , b >. | ( ( a e. ran ( LineG ` g ) /\ b e. ran ( LineG ` g ) ) /\ ( a = b \/ ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) ) ) } : No typesetting found for class { <. a , b >. | ( ( a e. ran ( LineG ` g ) /\ b e. ran ( LineG ` g ) ) /\ ( a = b \/ ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) ) ) } with typecode class
31	1 2 30	cmpt	Could not format ( g e. _V |-> { <. a , b >. | ( ( a e. ran ( LineG ` g ) /\ b e. ran ( LineG ` g ) ) /\ ( a = b \/ ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) ) ) } ) : No typesetting found for class ( g e. _V |-> { <. a , b >. | ( ( a e. ran ( LineG ` g ) /\ b e. ran ( LineG ` g ) ) /\ ( a = b \/ ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) ) ) } ) with typecode class
32	0 31	wceq	Could not format parlnG = ( g e. _V |-> { <. a , b >. | ( ( a e. ran ( LineG ` g ) /\ b e. ran ( LineG ` g ) ) /\ ( a = b \/ ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) ) ) } ) : No typesetting found for wff parlnG = ( g e. _V |-> { <. a , b >. | ( ( a e. ran ( LineG ` g ) /\ b e. ran ( LineG ` g ) ) /\ ( a = b \/ ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) ) ) } ) with typecode wff