Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-fs Unicode version

Definition df-fs 24005
Description: The general five segment configuration is a generalization of the outer and inner five segment configurations. See brfs 24042 and fscgr 24043 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
StepHypRef Expression
1 cfs 24001 . 2  class  FiveSeg
2 vp . . . . . . . . . . . . . . 15  set  p
32cv 1618 . . . . . . . . . . . . . 14  class  p
4 va . . . . . . . . . . . . . . . . 17  set  a
54cv 1618 . . . . . . . . . . . . . . . 16  class  a
6 vb . . . . . . . . . . . . . . . . 17  set  b
76cv 1618 . . . . . . . . . . . . . . . 16  class  b
85, 7cop 3584 . . . . . . . . . . . . . . 15  class  <. a ,  b >.
9 vc . . . . . . . . . . . . . . . . 17  set  c
109cv 1618 . . . . . . . . . . . . . . . 16  class  c
11 vd . . . . . . . . . . . . . . . . 17  set  d
1211cv 1618 . . . . . . . . . . . . . . . 16  class  d
1310, 12cop 3584 . . . . . . . . . . . . . . 15  class  <. c ,  d >.
148, 13cop 3584 . . . . . . . . . . . . . 14  class  <. <. a ,  b >. ,  <. c ,  d >. >.
153, 14wceq 1619 . . . . . . . . . . . . 13  wff  p  = 
<. <. a ,  b
>. ,  <. c ,  d >. >.
16 vq . . . . . . . . . . . . . . 15  set  q
1716cv 1618 . . . . . . . . . . . . . 14  class  q
18 vx . . . . . . . . . . . . . . . . 17  set  x
1918cv 1618 . . . . . . . . . . . . . . . 16  class  x
20 vy . . . . . . . . . . . . . . . . 17  set  y
2120cv 1618 . . . . . . . . . . . . . . . 16  class  y
2219, 21cop 3584 . . . . . . . . . . . . . . 15  class  <. x ,  y >.
23 vz . . . . . . . . . . . . . . . . 17  set  z
2423cv 1618 . . . . . . . . . . . . . . . 16  class  z
25 vw . . . . . . . . . . . . . . . . 17  set  w
2625cv 1618 . . . . . . . . . . . . . . . 16  class  w
2724, 26cop 3584 . . . . . . . . . . . . . . 15  class  <. z ,  w >.
2822, 27cop 3584 . . . . . . . . . . . . . 14  class  <. <. x ,  y >. ,  <. z ,  w >. >.
2917, 28wceq 1619 . . . . . . . . . . . . 13  wff  q  = 
<. <. x ,  y
>. ,  <. z ,  w >. >.
307, 10cop 3584 . . . . . . . . . . . . . . 15  class  <. b ,  c >.
31 ccolin 24000 . . . . . . . . . . . . . . 15  class  Colinear
325, 30, 31wbr 3963 . . . . . . . . . . . . . 14  wff  a  Colinear  <. b ,  c >.
335, 30cop 3584 . . . . . . . . . . . . . . 15  class  <. a ,  <. b ,  c
>. >.
3421, 24cop 3584 . . . . . . . . . . . . . . . 16  class  <. y ,  z >.
3519, 34cop 3584 . . . . . . . . . . . . . . 15  class  <. x ,  <. y ,  z
>. >.
36 ccgr3 23999 . . . . . . . . . . . . . . 15  class Cgr3
3733, 35, 36wbr 3963 . . . . . . . . . . . . . 14  wff  <. a ,  <. b ,  c
>. >.Cgr3 <. x ,  <. y ,  z >. >.
385, 12cop 3584 . . . . . . . . . . . . . . . 16  class  <. a ,  d >.
3919, 26cop 3584 . . . . . . . . . . . . . . . 16  class  <. x ,  w >.
40 ccgr 23858 . . . . . . . . . . . . . . . 16  class Cgr
4138, 39, 40wbr 3963 . . . . . . . . . . . . . . 15  wff  <. a ,  d >.Cgr <. x ,  w >.
427, 12cop 3584 . . . . . . . . . . . . . . . 16  class  <. b ,  d >.
4321, 26cop 3584 . . . . . . . . . . . . . . . 16  class  <. y ,  w >.
4442, 43, 40wbr 3963 . . . . . . . . . . . . . . 15  wff  <. b ,  d >.Cgr <. y ,  w >.
4541, 44wa 360 . . . . . . . . . . . . . 14  wff  ( <.
a ,  d >.Cgr <. x ,  w >.  /\ 
<. b ,  d >.Cgr <. y ,  w >. )
4632, 37, 45w3a 939 . . . . . . . . . . . . 13  wff  ( a 
Colinear 
<. b ,  c >.  /\  <. a ,  <. b ,  c >. >.Cgr3 <. x ,  <. y ,  z
>. >.  /\  ( <. a ,  d >.Cgr <. x ,  w >.  /\  <. b ,  d >.Cgr <. y ,  w >. ) )
4715, 29, 46w3a 939 . . . . . . . . . . . 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  set  n
4948cv 1618 . . . . . . . . . . . . 13  class  n
50 cee 23856 . . . . . . . . . . . . 13  class  EE
5149, 50cfv 4638 . . . . . . . . . . . 12  class  ( EE
`  n )
5247, 25, 51wrex 2517 . . . . . . . . . . 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 >. ) ) )
5352, 23, 51wrex 2517 . . . . . . . . . 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 >. ) ) )
5453, 20, 51wrex 2517 . . . . . . . . 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 >. ) ) )
5554, 18, 51wrex 2517 . . . . . . . 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 >. ) ) )
5655, 11, 51wrex 2517 . . . . . . 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 >. ) ) )
5756, 9, 51wrex 2517 . . . . . 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 >. ) ) )
5857, 6, 51wrex 2517 . . . . 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 >. ) ) )
5958, 4, 51wrex 2517 . . . 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 9679 . . . 4  class  NN
6159, 48, 60wrex 2517 . . 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 >. ) ) )
6261, 2, 16copab 4016 . 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 >. ) ) ) }
631, 62wceq 1619 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 >. ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  brfs  24042
  Copyright terms: Public domain W3C validator