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 A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N G 𝔼 N H 𝔼 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 𝔼 n = 𝔼 N
51 df-fs FiveSeg = p q | n a 𝔼 n b 𝔼 n c 𝔼 n d 𝔼 n e 𝔼 n f 𝔼 n g 𝔼 n h 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N G 𝔼 N H 𝔼 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