Metamath Proof Explorer

Definition df-line2

Description: Define the Line function. This function generates the line passing through the distinct points a and b . Adapted from definition 6.14 of Schwabhauser p. 45. (Contributed by Scott Fenton, 25-Oct-2013)

Ref Expression
Assertion df-line2 
|- Line = { <. <. a , b >. , l >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cline2 
 |-  Line
1 va 
 |-  a
2 vb 
 |-  b
3 vl 
 |-  l
4 vn 
 |-  n
5 cn 
 |-  NN
6 1 cv 
 |-  a
7 cee 
 |-  EE
8 4 cv 
 |-  n
9 8 7 cfv 
 |-  ( EE ` n )
10 6 9 wcel 
 |-  a e. ( EE ` n )
11 2 cv 
 |-  b
12 11 9 wcel 
 |-  b e. ( EE ` n )
13 6 11 wne 
 |-  a =/= b
14 10 12 13 w3a 
 |-  ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b )
15 3 cv 
 |-  l
16 6 11 cop 
 |-  <. a , b >.
17 ccolin 
 |-  Colinear
18 17 ccnv 
 |-  `' Colinear
19 16 18 cec 
 |-  [ <. a , b >. ] `' Colinear
20 15 19 wceq 
 |-  l = [ <. a , b >. ] `' Colinear
21 14 20 wa 
 |-  ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear )
22 21 4 5 wrex 
 |-  E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear )
23 22 1 2 3 coprab 
 |-  { <. <. a , b >. , l >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) }
24 0 23 wceq 
 |-  Line = { <. <. a , b >. , l >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) }