Definition df-line2 32244

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.)

Assertion

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

Distinct variable group:   a, b, l, n

Detailed syntax breakdown of Definition df-line2

Step	Hyp	Ref	Expression
1		cline2 32241	. 2 class Line
2		va	. . . . . . . 8 setvar a
3	2	cv 1482	. . . . . . 7 class a
4		vn	. . . . . . . . 9 setvar n
5	4	cv 1482	. . . . . . . 8 class n
6		cee 25768	. . . . . . . 8 class EE
7	5, 6	cfv 5888	. . . . . . 7 class ( EE ` n )
8	3, 7	wcel 1990	. . . . . 6 wff a e. ( EE ` n )
9		vb	. . . . . . . 8 setvar b
10	9	cv 1482	. . . . . . 7 class b
11	10, 7	wcel 1990	. . . . . 6 wff b e. ( EE ` n )
12	3, 10	wne 2794	. . . . . 6 wff a =/= b
13	8, 11, 12	w3a 1037	. . . . 5 wff ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b )
14		vl	. . . . . . 7 setvar l
15	14	cv 1482	. . . . . 6 class l
16	3, 10	cop 4183	. . . . . . 7 class <. a , b >.
17		ccolin 32144	. . . . . . . 8 class Colinear
18	17	ccnv 5113	. . . . . . 7 class `' Colinear
19	16, 18	cec 7740	. . . . . 6 class [ <. a , b >. ] `' Colinear
20	15, 19	wceq 1483	. . . . 5 wff l = [ <. a , b >. ] `' Colinear
21	13, 20	wa 384	. . . 4 wff ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear )
22		cn 11020	. . . 4 class NN
23	21, 4, 22	wrex 2913	. . 3 wff E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear )
24	23, 2, 9, 14	coprab 6651	. 2 class { <. <. a , b >. , l >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) }
25	1, 24	wceq 1483	1 wff Line = { <. <. a , b >. , l >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) }

This definition is referenced by:  funline  32249  linedegen  32250  fvline  32251  ellines  32259