Metamath Proof Explorer

Definition df-ifs

Description: The inner five segment configuration is an abbreviation for another congruence condition. See brifs and ifscgr for how it is used. Definition 4.1 of Schwabhauser p. 34. (Contributed by Scott Fenton, 26-Sep-2013)

Ref Expression
Assertion df-ifs 
|- InnerFiveSeg = { <. 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 >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , c >. Cgr <. x , z >. /\ <. b , c >. Cgr <. y , z >. ) /\ ( <. a , d >. Cgr <. x , w >. /\ <. c , d >. Cgr <. z , w >. ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cifs 
 |-  InnerFiveSeg
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 cbtwn 
 |-  Btwn
35 17 20 cop 
 |-  <. a , c >.
36 18 35 34 wbr 
 |-  b Btwn <. a , c >.
37 26 29 cop 
 |-  <. x , z >.
38 27 37 34 wbr 
 |-  y Btwn <. x , z >.
39 36 38 wa 
 |-  ( b Btwn <. a , c >. /\ y Btwn <. x , z >. )
40 ccgr 
 |-  Cgr
41 35 37 40 wbr 
 |-  <. a , c >. Cgr <. x , z >.
42 18 20 cop 
 |-  <. b , c >.
43 27 29 cop 
 |-  <. y , z >.
44 42 43 40 wbr 
 |-  <. b , c >. Cgr <. y , z >.
45 41 44 wa 
 |-  ( <. a , c >. Cgr <. x , z >. /\ <. b , c >. Cgr <. y , z >. )
46 17 21 cop 
 |-  <. a , d >.
47 26 30 cop 
 |-  <. x , w >.
48 46 47 40 wbr 
 |-  <. a , d >. Cgr <. x , w >.
49 22 31 40 wbr 
 |-  <. c , d >. Cgr <. z , w >.
50 48 49 wa 
 |-  ( <. a , d >. Cgr <. x , w >. /\ <. c , d >. Cgr <. z , w >. )
51 39 45 50 w3a 
 |-  ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , c >. Cgr <. x , z >. /\ <. b , c >. Cgr <. y , z >. ) /\ ( <. a , d >. Cgr <. x , w >. /\ <. c , d >. Cgr <. z , w >. ) )
52 24 33 51 w3a 
 |-  ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , c >. Cgr <. x , z >. /\ <. b , c >. Cgr <. y , z >. ) /\ ( <. a , d >. Cgr <. x , w >. /\ <. c , d >. Cgr <. z , w >. ) ) )
53 52 15 8 wrex 
 |-  E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , c >. Cgr <. x , z >. /\ <. b , c >. Cgr <. y , z >. ) /\ ( <. a , d >. Cgr <. x , w >. /\ <. c , d >. Cgr <. z , w >. ) ) )
54 53 14 8 wrex 
 |-  E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , c >. Cgr <. x , z >. /\ <. b , c >. Cgr <. y , z >. ) /\ ( <. a , d >. Cgr <. x , w >. /\ <. c , d >. Cgr <. z , w >. ) ) )
55 54 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 >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , c >. Cgr <. x , z >. /\ <. b , c >. Cgr <. y , z >. ) /\ ( <. a , d >. Cgr <. x , w >. /\ <. c , d >. Cgr <. z , w >. ) ) )
56 55 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 >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , c >. Cgr <. x , z >. /\ <. b , c >. Cgr <. y , z >. ) /\ ( <. a , d >. Cgr <. x , w >. /\ <. c , d >. Cgr <. z , w >. ) ) )
57 56 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 >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , c >. Cgr <. x , z >. /\ <. b , c >. Cgr <. y , z >. ) /\ ( <. a , d >. Cgr <. x , w >. /\ <. c , d >. Cgr <. z , w >. ) ) )
58 57 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 >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , c >. Cgr <. x , z >. /\ <. b , c >. Cgr <. y , z >. ) /\ ( <. a , d >. Cgr <. x , w >. /\ <. c , d >. Cgr <. z , w >. ) ) )
59 58 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 >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , c >. Cgr <. x , z >. /\ <. b , c >. Cgr <. y , z >. ) /\ ( <. a , d >. Cgr <. x , w >. /\ <. c , d >. Cgr <. z , w >. ) ) )
60 59 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 >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , c >. Cgr <. x , z >. /\ <. b , c >. Cgr <. y , z >. ) /\ ( <. a , d >. Cgr <. x , w >. /\ <. c , d >. Cgr <. z , w >. ) ) )
61 60 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 >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , c >. Cgr <. x , z >. /\ <. b , c >. Cgr <. y , z >. ) /\ ( <. a , d >. Cgr <. x , w >. /\ <. c , d >. Cgr <. z , w >. ) ) )
62 61 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 >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , c >. Cgr <. x , z >. /\ <. b , c >. Cgr <. y , z >. ) /\ ( <. a , d >. Cgr <. x , w >. /\ <. c , d >. Cgr <. z , w >. ) ) ) }
63 0 62 wceq 
 |-  InnerFiveSeg = { <. 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 >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , c >. Cgr <. x , z >. /\ <. b , c >. Cgr <. y , z >. ) /\ ( <. a , d >. Cgr <. x , w >. /\ <. c , d >. Cgr <. z , w >. ) ) ) }