Metamath Proof Explorer

Theorem brfs

Description: Binary relation form of the general five segment predicate. (Contributed by Scott Fenton, 5-Oct-2013)

Ref Expression
Assertion brfs 
|- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. A , B >. , <. C , D >. >. FiveSeg <. <. E , F >. , <. G , H >. >. <-> ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) ) )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( a = A -> ( a Colinear <. b , c >. <-> A Colinear <. b , c >. ) )
2 opeq1 
 |-  ( a = A -> <. a , <. b , c >. >. = <. A , <. b , c >. >. )
3 2 breq1d 
 |-  ( a = A -> ( <. a , <. b , c >. >. Cgr3 <. e , <. f , g >. >. <-> <. A , <. b , c >. >. Cgr3 <. e , <. f , g >. >. ) )
4 opeq1 
 |-  ( a = A -> <. a , d >. = <. A , d >. )
5 4 breq1d 
 |-  ( a = A -> ( <. a , d >. Cgr <. e , h >. <-> <. A , d >. Cgr <. e , h >. ) )
6 5 anbi1d 
 |-  ( a = A -> ( ( <. a , d >. Cgr <. e , h >. /\ <. b , d >. Cgr <. f , h >. ) <-> ( <. A , d >. Cgr <. e , h >. /\ <. b , d >. Cgr <. f , h >. ) ) )
7 1 3 6 3anbi123d 
 |-  ( a = A -> ( ( a Colinear <. b , c >. /\ <. a , <. b , c >. >. Cgr3 <. e , <. f , g >. >. /\ ( <. a , d >. Cgr <. e , h >. /\ <. b , d >. Cgr <. f , h >. ) ) <-> ( A Colinear <. b , c >. /\ <. A , <. b , c >. >. Cgr3 <. e , <. f , g >. >. /\ ( <. A , d >. Cgr <. e , h >. /\ <. b , d >. Cgr <. f , h >. ) ) ) )
8 opeq1 
 |-  ( b = B -> <. b , c >. = <. B , c >. )
9 8 breq2d 
 |-  ( b = B -> ( A Colinear <. b , c >. <-> A Colinear <. B , c >. ) )
10 8 opeq2d 
 |-  ( b = B -> <. A , <. b , c >. >. = <. A , <. B , c >. >. )
11 10 breq1d 
 |-  ( b = B -> ( <. A , <. b , c >. >. Cgr3 <. e , <. f , g >. >. <-> <. A , <. B , c >. >. Cgr3 <. e , <. f , g >. >. ) )
12 opeq1 
 |-  ( b = B -> <. b , d >. = <. B , d >. )
13 12 breq1d 
 |-  ( b = B -> ( <. b , d >. Cgr <. f , h >. <-> <. B , d >. Cgr <. f , h >. ) )
14 13 anbi2d 
 |-  ( b = B -> ( ( <. A , d >. Cgr <. e , h >. /\ <. b , d >. Cgr <. f , h >. ) <-> ( <. A , d >. Cgr <. e , h >. /\ <. B , d >. Cgr <. f , h >. ) ) )
15 9 11 14 3anbi123d 
 |-  ( b = B -> ( ( A Colinear <. b , c >. /\ <. A , <. b , c >. >. Cgr3 <. e , <. f , g >. >. /\ ( <. A , d >. Cgr <. e , h >. /\ <. b , d >. Cgr <. f , h >. ) ) <-> ( A Colinear <. B , c >. /\ <. A , <. B , c >. >. Cgr3 <. e , <. f , g >. >. /\ ( <. A , d >. Cgr <. e , h >. /\ <. B , d >. Cgr <. f , h >. ) ) ) )
16 opeq2 
 |-  ( c = C -> <. B , c >. = <. B , C >. )
17 16 breq2d 
 |-  ( c = C -> ( A Colinear <. B , c >. <-> A Colinear <. B , C >. ) )
18 16 opeq2d 
 |-  ( c = C -> <. A , <. B , c >. >. = <. A , <. B , C >. >. )
19 18 breq1d 
 |-  ( c = C -> ( <. A , <. B , c >. >. Cgr3 <. e , <. f , g >. >. <-> <. A , <. B , C >. >. Cgr3 <. e , <. f , g >. >. ) )
20 17 19 3anbi12d 
 |-  ( c = C -> ( ( A Colinear <. B , c >. /\ <. A , <. B , c >. >. Cgr3 <. e , <. f , g >. >. /\ ( <. A , d >. Cgr <. e , h >. /\ <. B , d >. Cgr <. f , h >. ) ) <-> ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. e , <. f , g >. >. /\ ( <. A , d >. Cgr <. e , h >. /\ <. B , d >. Cgr <. f , h >. ) ) ) )
21 opeq2 
 |-  ( d = D -> <. A , d >. = <. A , D >. )
22 21 breq1d 
 |-  ( d = D -> ( <. A , d >. Cgr <. e , h >. <-> <. A , D >. Cgr <. e , h >. ) )
23 opeq2 
 |-  ( d = D -> <. B , d >. = <. B , D >. )
24 23 breq1d 
 |-  ( d = D -> ( <. B , d >. Cgr <. f , h >. <-> <. B , D >. Cgr <. f , h >. ) )
25 22 24 anbi12d 
 |-  ( d = D -> ( ( <. A , d >. Cgr <. e , h >. /\ <. B , d >. Cgr <. f , h >. ) <-> ( <. A , D >. Cgr <. e , h >. /\ <. B , D >. Cgr <. f , h >. ) ) )
26 25 3anbi3d 
 |-  ( d = D -> ( ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. e , <. f , g >. >. /\ ( <. A , d >. Cgr <. e , h >. /\ <. B , d >. Cgr <. f , h >. ) ) <-> ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. e , <. f , g >. >. /\ ( <. A , D >. Cgr <. e , h >. /\ <. B , D >. Cgr <. f , h >. ) ) ) )
27 opeq1 
 |-  ( e = E -> <. e , <. f , g >. >. = <. E , <. f , g >. >. )
28 27 breq2d 
 |-  ( e = E -> ( <. A , <. B , C >. >. Cgr3 <. e , <. f , g >. >. <-> <. A , <. B , C >. >. Cgr3 <. E , <. f , g >. >. ) )
29 opeq1 
 |-  ( e = E -> <. e , h >. = <. E , h >. )
30 29 breq2d 
 |-  ( e = E -> ( <. A , D >. Cgr <. e , h >. <-> <. A , D >. Cgr <. E , h >. ) )
31 30 anbi1d 
 |-  ( e = E -> ( ( <. A , D >. Cgr <. e , h >. /\ <. B , D >. Cgr <. f , h >. ) <-> ( <. A , D >. Cgr <. E , h >. /\ <. B , D >. Cgr <. f , h >. ) ) )
32 28 31 3anbi23d 
 |-  ( e = E -> ( ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. e , <. f , g >. >. /\ ( <. A , D >. Cgr <. e , h >. /\ <. B , D >. Cgr <. f , h >. ) ) <-> ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. f , g >. >. /\ ( <. A , D >. Cgr <. E , h >. /\ <. B , D >. Cgr <. f , h >. ) ) ) )
33 opeq1 
 |-  ( f = F -> <. f , g >. = <. F , g >. )
34 33 opeq2d 
 |-  ( f = F -> <. E , <. f , g >. >. = <. E , <. F , g >. >. )
35 34 breq2d 
 |-  ( f = F -> ( <. A , <. B , C >. >. Cgr3 <. E , <. f , g >. >. <-> <. A , <. B , C >. >. Cgr3 <. E , <. F , g >. >. ) )
36 opeq1 
 |-  ( f = F -> <. f , h >. = <. F , h >. )
37 36 breq2d 
 |-  ( f = F -> ( <. B , D >. Cgr <. f , h >. <-> <. B , D >. Cgr <. F , h >. ) )
38 37 anbi2d 
 |-  ( f = F -> ( ( <. A , D >. Cgr <. E , h >. /\ <. B , D >. Cgr <. f , h >. ) <-> ( <. A , D >. Cgr <. E , h >. /\ <. B , D >. Cgr <. F , h >. ) ) )
39 35 38 3anbi23d 
 |-  ( f = F -> ( ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. f , g >. >. /\ ( <. A , D >. Cgr <. E , h >. /\ <. B , D >. Cgr <. f , h >. ) ) <-> ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , g >. >. /\ ( <. A , D >. Cgr <. E , h >. /\ <. B , D >. Cgr <. F , h >. ) ) ) )
40 opeq2 
 |-  ( g = G -> <. F , g >. = <. F , G >. )
41 40 opeq2d 
 |-  ( g = G -> <. E , <. F , g >. >. = <. E , <. F , G >. >. )
42 41 breq2d 
 |-  ( g = G -> ( <. A , <. B , C >. >. Cgr3 <. E , <. F , g >. >. <-> <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. ) )
43 42 3anbi2d 
 |-  ( g = G -> ( ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , g >. >. /\ ( <. A , D >. Cgr <. E , h >. /\ <. B , D >. Cgr <. F , h >. ) ) <-> ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , h >. /\ <. B , D >. Cgr <. F , h >. ) ) ) )
44 opeq2 
 |-  ( h = H -> <. E , h >. = <. E , H >. )
45 44 breq2d 
 |-  ( h = H -> ( <. A , D >. Cgr <. E , h >. <-> <. A , D >. Cgr <. E , H >. ) )
46 opeq2 
 |-  ( h = H -> <. F , h >. = <. F , H >. )
47 46 breq2d 
 |-  ( h = H -> ( <. B , D >. Cgr <. F , h >. <-> <. B , D >. Cgr <. F , H >. ) )
48 45 47 anbi12d 
 |-  ( h = H -> ( ( <. A , D >. Cgr <. E , h >. /\ <. B , D >. Cgr <. F , h >. ) <-> ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) )
49 48 3anbi3d 
 |-  ( h = H -> ( ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , h >. /\ <. B , D >. Cgr <. F , h >. ) ) <-> ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) ) )
50 fveq2 
 |-  ( n = N -> ( EE ` n ) = ( EE ` N ) )
51 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. e e. ( EE ` n ) E. f e. ( EE ` n ) E. g e. ( EE ` n ) E. h e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ( a Colinear <. b , c >. /\ <. a , <. b , c >. >. Cgr3 <. e , <. f , g >. >. /\ ( <. a , d >. Cgr <. e , h >. /\ <. b , d >. Cgr <. f , h >. ) ) ) }
52 7 15 20 26 32 39 43 49 50 51 br8 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. A , B >. , <. C , D >. >. FiveSeg <. <. E , F >. , <. G , H >. >. <-> ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) ) )