Definition df-line2 30953

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 30950	. 2 class Line
2		va	. . . . . . . 8 setvar a
3	2	cv 1454	. . . . . . 7 class a
4		vn	. . . . . . . . 9 setvar n
5	4	cv 1454	. . . . . . . 8 class n
6		cee 24967	. . . . . . . 8 class EE
7	5, 6	cfv 5601	. . . . . . 7 class ( EE ` n )
8	3, 7	wcel 1898	. . . . . 6 wff a e. ( EE ` n )
9		vb	. . . . . . . 8 setvar b
10	9	cv 1454	. . . . . . 7 class b
11	10, 7	wcel 1898	. . . . . 6 wff b e. ( EE ` n )
12	3, 10	wne 2633	. . . . . 6 wff a =/= b
13	8, 11, 12	w3a 991	. . . . 5 wff ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b )
14		vl	. . . . . . 7 setvar l
15	14	cv 1454	. . . . . 6 class l
16	3, 10	cop 3986	. . . . . . 7 class <. a , b >.
17		ccolin 30853	. . . . . . . 8 class Colinear
18	17	ccnv 4852	. . . . . . 7 class `' Colinear
19	16, 18	cec 7387	. . . . . 6 class [ <. a , b >. ] `' Colinear
20	15, 19	wceq 1455	. . . . 5 wff l = [ <. a , b >. ] `' Colinear
21	13, 20	wa 375	. . . 4 wff ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear )
22		cn 10637	. . . 4 class NN
23	21, 4, 22	wrex 2750	. . 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 6316	. 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 1455	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  30958  linedegen  30959  fvline  30960  ellines  30968