Metamath Proof Explorer

Definition df-fs

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

Ref Expression
Assertion 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 >. ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfs 
 |-  FiveSeg
1 vp 
 |-  p
2 vq 
 |-  q
3 vn 
 |-  n
4 cn 
 |-  NN
5 va 
 |-  a
6 cee 
 |-  EE
7 3 cv 
 |-  n
8 7 6 cfv 
 |-  ( EE ` n )
9 vb 
 |-  b
10 vc 
 |-  c
11 vd 
 |-  d
12 vx 
 |-  x
13 vy 
 |-  y
14 vz 
 |-  z
15 vw 
 |-  w
16 1 cv 
 |-  p
17 5 cv 
 |-  a
18 9 cv 
 |-  b
19 17 18 cop 
 |-  <. a , b >.
20 10 cv 
 |-  c
21 11 cv 
 |-  d
22 20 21 cop 
 |-  <. c , d >.
23 19 22 cop 
 |-  <. <. a , b >. , <. c , d >. >.
24 16 23 wceq 
 |-  p = <. <. a , b >. , <. c , d >. >.
25 2 cv 
 |-  q
26 12 cv 
 |-  x
27 13 cv 
 |-  y
28 26 27 cop 
 |-  <. x , y >.
29 14 cv 
 |-  z
30 15 cv 
 |-  w
31 29 30 cop 
 |-  <. z , w >.
32 28 31 cop 
 |-  <. <. x , y >. , <. z , w >. >.
33 25 32 wceq 
 |-  q = <. <. x , y >. , <. z , w >. >.
34 ccolin 
 |-  Colinear
35 18 20 cop 
 |-  <. b , c >.
36 17 35 34 wbr 
 |-  a Colinear <. b , c >.
37 17 35 cop 
 |-  <. a , <. b , c >. >.
38 ccgr3 
 |-  Cgr3
39 27 29 cop 
 |-  <. y , z >.
40 26 39 cop 
 |-  <. x , <. y , z >. >.
41 37 40 38 wbr 
 |-  <. a , <. b , c >. >. Cgr3 <. x , <. y , z >. >.
42 17 21 cop 
 |-  <. a , d >.
43 ccgr 
 |-  Cgr
44 26 30 cop 
 |-  <. x , w >.
45 42 44 43 wbr 
 |-  <. a , d >. Cgr <. x , w >.
46 18 21 cop 
 |-  <. b , d >.
47 27 30 cop 
 |-  <. y , w >.
48 46 47 43 wbr 
 |-  <. b , d >. Cgr <. y , w >.
49 45 48 wa 
 |-  ( <. a , d >. Cgr <. x , w >. /\ <. b , d >. Cgr <. y , w >. )
50 36 41 49 w3a 
 |-  ( a Colinear <. b , c >. /\ <. a , <. b , c >. >. Cgr3 <. x , <. y , z >. >. /\ ( <. a , d >. Cgr <. x , w >. /\ <. b , d >. Cgr <. y , w >. ) )
51 24 33 50 w3a 
 |-  ( 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 >. ) ) )
52 51 15 8 wrex 
 |-  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 14 8 wrex 
 |-  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 13 8 wrex 
 |-  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 12 8 wrex 
 |-  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 8 wrex 
 |-  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 10 8 wrex 
 |-  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 9 8 wrex 
 |-  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 5 8 wrex 
 |-  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 59 3 4 wrex 
 |-  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 >. ) ) )
61 60 1 2 copab 
 |-  { <. 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 >. ) ) ) }
62 0 61 wceq 
 |-  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 >. ) ) ) }