Definition df-fs 32149

Description: The general five segment configuration is a generalization of the outer and inner five segment configurations. See brfs 32186 and fscgr 32187 for its use. Definition 4.15 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.)

Assertion

Ref

Expression

df-fs

|- FiveSeg = { <. p , q >. | E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) E. x e. ( EE ` n ) E. y e. ( EE ` n ) E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( a Colinear <. b , c >. /\ <. a , <. b , c >. >.Cgr3 <. x , <. y , z >. >. /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) ) }

Distinct variable group:   a, b, c, d, x, y, z, w, p, q, n

Detailed syntax breakdown of Definition df-fs

Step	Hyp	Ref	Expression
1		cfs 32145	. 2 class FiveSeg
2		vp	. . . . . . . . . . . . . . 15 setvar p
3	2	cv 1482	. . . . . . . . . . . . . 14 class p
4		va	. . . . . . . . . . . . . . . . 17 setvar a
5	4	cv 1482	. . . . . . . . . . . . . . . 16 class a
6		vb	. . . . . . . . . . . . . . . . 17 setvar b
7	6	cv 1482	. . . . . . . . . . . . . . . 16 class b
8	5, 7	cop 4183	. . . . . . . . . . . . . . 15 class <. a , b >.
9		vc	. . . . . . . . . . . . . . . . 17 setvar c
10	9	cv 1482	. . . . . . . . . . . . . . . 16 class c
11		vd	. . . . . . . . . . . . . . . . 17 setvar d
12	11	cv 1482	. . . . . . . . . . . . . . . 16 class d
13	10, 12	cop 4183	. . . . . . . . . . . . . . 15 class <. c , d >.
14	8, 13	cop 4183	. . . . . . . . . . . . . 14 class <. <. a , b >. , <. c , d >. >.
15	3, 14	wceq 1483	. . . . . . . . . . . . 13 wff p = <. <. a , b >. , <. c , d >. >.
16		vq	. . . . . . . . . . . . . . 15 setvar q
17	16	cv 1482	. . . . . . . . . . . . . 14 class q
18		vx	. . . . . . . . . . . . . . . . 17 setvar x
19	18	cv 1482	. . . . . . . . . . . . . . . 16 class x
20		vy	. . . . . . . . . . . . . . . . 17 setvar y
21	20	cv 1482	. . . . . . . . . . . . . . . 16 class y
22	19, 21	cop 4183	. . . . . . . . . . . . . . 15 class <. x , y >.
23		vz	. . . . . . . . . . . . . . . . 17 setvar z
24	23	cv 1482	. . . . . . . . . . . . . . . 16 class z
25		vw	. . . . . . . . . . . . . . . . 17 setvar w
26	25	cv 1482	. . . . . . . . . . . . . . . 16 class w
27	24, 26	cop 4183	. . . . . . . . . . . . . . 15 class <. z , w >.
28	22, 27	cop 4183	. . . . . . . . . . . . . 14 class <. <. x , y >. , <. z , w >. >.
29	17, 28	wceq 1483	. . . . . . . . . . . . 13 wff q = <. <. x , y >. , <. z , w >. >.
30	7, 10	cop 4183	. . . . . . . . . . . . . . 15 class <. b , c >.
31		ccolin 32144	. . . . . . . . . . . . . . 15 class Colinear
32	5, 30, 31	wbr 4653	. . . . . . . . . . . . . 14 wff a Colinear <. b , c >.
33	5, 30	cop 4183	. . . . . . . . . . . . . . 15 class <. a , <. b , c >. >.
34	21, 24	cop 4183	. . . . . . . . . . . . . . . 16 class <. y , z >.
35	19, 34	cop 4183	. . . . . . . . . . . . . . 15 class <. x , <. y , z >. >.
36		ccgr3 32143	. . . . . . . . . . . . . . 15 class Cgr3
37	33, 35, 36	wbr 4653	. . . . . . . . . . . . . 14 wff <. a , <. b , c >. >.Cgr3 <. x , <. y , z >. >.
38	5, 12	cop 4183	. . . . . . . . . . . . . . . 16 class <. a , d >.
39	19, 26	cop 4183	. . . . . . . . . . . . . . . 16 class <. x , w >.
40		ccgr 25770	. . . . . . . . . . . . . . . 16 class Cgr
41	38, 39, 40	wbr 4653	. . . . . . . . . . . . . . 15 wff <. a , d >.Cgr <. x , w >.
42	7, 12	cop 4183	. . . . . . . . . . . . . . . 16 class <. b , d >.
43	21, 26	cop 4183	. . . . . . . . . . . . . . . 16 class <. y , w >.
44	42, 43, 40	wbr 4653	. . . . . . . . . . . . . . 15 wff <. b , d >.Cgr <. y , w >.
45	41, 44	wa 384	. . . . . . . . . . . . . 14 wff ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. )
46	32, 37, 45	w3a 1037	. . . . . . . . . . . . 13 wff ( a Colinear <. b , c >. /\ <. a , <. b , c >. >.Cgr3 <. x , <. y , z >. >. /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) )
47	15, 29, 46	w3a 1037	. . . . . . . . . . . 12 wff ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( a Colinear <. b , c >. /\ <. a , <. b , c >. >.Cgr3 <. x , <. y , z >. >. /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) )
48		vn	. . . . . . . . . . . . . 14 setvar n
49	48	cv 1482	. . . . . . . . . . . . 13 class n
50		cee 25768	. . . . . . . . . . . . 13 class EE
51	49, 50	cfv 5888	. . . . . . . . . . . 12 class ( EE ` n )
52	47, 25, 51	wrex 2913	. . . . . . . . . . 11 wff E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( a Colinear <. b , c >. /\ <. a , <. b , c >. >.Cgr3 <. x , <. y , z >. >. /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) )
53	52, 23, 51	wrex 2913	. . . . . . . . . 10 wff E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( a Colinear <. b , c >. /\ <. a , <. b , c >. >.Cgr3 <. x , <. y , z >. >. /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) )
54	53, 20, 51	wrex 2913	. . . . . . . . 9 wff E. y e. ( EE ` n ) E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( a Colinear <. b , c >. /\ <. a , <. b , c >. >.Cgr3 <. x , <. y , z >. >. /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) )
55	54, 18, 51	wrex 2913	. . . . . . . 8 wff E. x e. ( EE ` n ) E. y e. ( EE ` n ) E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( a Colinear <. b , c >. /\ <. a , <. b , c >. >.Cgr3 <. x , <. y , z >. >. /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) )
56	55, 11, 51	wrex 2913	. . . . . . 7 wff E. d e. ( EE ` n ) E. x e. ( EE ` n ) E. y e. ( EE ` n ) E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( a Colinear <. b , c >. /\ <. a , <. b , c >. >.Cgr3 <. x , <. y , z >. >. /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) )
57	56, 9, 51	wrex 2913	. . . . . 6 wff E. c e. ( EE ` n ) E. d e. ( EE ` n ) E. x e. ( EE ` n ) E. y e. ( EE ` n ) E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( a Colinear <. b , c >. /\ <. a , <. b , c >. >.Cgr3 <. x , <. y , z >. >. /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) )
58	57, 6, 51	wrex 2913	. . . . 5 wff E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) E. x e. ( EE ` n ) E. y e. ( EE ` n ) E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( a Colinear <. b , c >. /\ <. a , <. b , c >. >.Cgr3 <. x , <. y , z >. >. /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) )
59	58, 4, 51	wrex 2913	. . . 4 wff E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) E. x e. ( EE ` n ) E. y e. ( EE ` n ) E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( a Colinear <. b , c >. /\ <. a , <. b , c >. >.Cgr3 <. x , <. y , z >. >. /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) )
60		cn 11020	. . . 4 class NN
61	59, 48, 60	wrex 2913	. . 3 wff E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) E. x e. ( EE ` n ) E. y e. ( EE ` n ) E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( a Colinear <. b , c >. /\ <. a , <. b , c >. >.Cgr3 <. x , <. y , z >. >. /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) )
62	61, 2, 16	copab 4712	. 2 class { <. p , q >. | E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) E. x e. ( EE ` n ) E. y e. ( EE ` n ) E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( a Colinear <. b , c >. /\ <. a , <. b , c >. >.Cgr3 <. x , <. y , z >. >. /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) ) }
63	1, 62	wceq 1483	1 wff FiveSeg = { <. p , q >. | E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) E. x e. ( EE ` n ) E. y e. ( EE ` n ) E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( a Colinear <. b , c >. /\ <. a , <. b , c >. >.Cgr3 <. x , <. y , z >. >. /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) ) }

This definition is referenced by:  brfs  32186