Metamath Proof Explorer

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 = ( 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 ) = (/) ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cprlng 
 |-  parlnG
1 vg 
 |-  g
2 cvv 
 |-  _V
3 va 
 |-  a
4 vb 
 |-  b
5 3 cv 
 |-  a
6 clng 
 |-  LineG
7 1 cv 
 |-  g
8 7 6 cfv 
 |-  ( LineG ` g )
9 8 crn 
 |-  ran ( LineG ` g )
10 5 9 wcel 
 |-  a e. ran ( LineG ` g )
11 4 cv 
 |-  b
12 11 9 wcel 
 |-  b e. ran ( LineG ` g )
13 10 12 wa 
 |-  ( a e. ran ( LineG ` g ) /\ b e. ran ( LineG ` g ) )
14 5 11 wceq 
 |-  a = b
15 vh 
 |-  h
16 cplng 
 |-  PlnG
17 7 16 cfv 
 |-  ( PlnG ` g )
18 17 crn 
 |-  ran ( PlnG ` g )
19 15 cv 
 |-  h
20 5 19 wss 
 |-  a C_ h
21 11 19 wss 
 |-  b C_ h
22 20 21 wa 
 |-  ( a C_ h /\ b C_ h )
23 22 15 18 wrex 
 |-  E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h )
24 5 11 cin 
 |-  ( a i^i b )
25 c0 
 |-  (/)
26 24 25 wceq 
 |-  ( a i^i b ) = (/)
27 23 26 wa 
 |-  ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) )
28 14 27 wo 
 |-  ( a = b \/ ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) )
29 13 28 wa 
 |-  ( ( 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 ) = (/) ) ) )
30 29 3 4 copab 
 |-  { <. 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 ) = (/) ) ) ) }
31 1 2 30 cmpt 
 |-  ( 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 ) = (/) ) ) ) } )
32 0 31 wceq 
 |-  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 ) = (/) ) ) ) } )