Theorem brfs 32186

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

Assertion

Ref

Expression

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 of Theorem brfs

Dummy variables a b c d e f g h p q n are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq1 4656	. . 3 |- ( a = A -> ( a Colinear <. b , c >. <-> A Colinear <. b , c >. ) )
2		opeq1 4402	. . . 4 |- ( a = A -> <. a , <. b , c >. >. = <. A , <. b , c >. >. )
3	2	breq1d 4663	. . 3 |- ( a = A -> ( <. a , <. b , c >. >.Cgr3 <. e , <. f , g >. >. <-> <. A , <. b , c >. >.Cgr3 <. e , <. f , g >. >. ) )
4		opeq1 4402	. . . . 5 |- ( a = A -> <. a , d >. = <. A , d >. )
5	4	breq1d 4663	. . . 4 |- ( a = A -> ( <. a , d >.Cgr <. e , h >. <-> <. A , d >.Cgr <. e , h >. ) )
6	5	anbi1d 741	. . 3 |- ( 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 1399	. 2 |- ( 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 4402	. . . 4 |- ( b = B -> <. b , c >. = <. B , c >. )
9	8	breq2d 4665	. . 3 |- ( b = B -> ( A Colinear <. b , c >. <-> A Colinear <. B , c >. ) )
10	8	opeq2d 4409	. . . 4 |- ( b = B -> <. A , <. b , c >. >. = <. A , <. B , c >. >. )
11	10	breq1d 4663	. . 3 |- ( b = B -> ( <. A , <. b , c >. >.Cgr3 <. e , <. f , g >. >. <-> <. A , <. B , c >. >.Cgr3 <. e , <. f , g >. >. ) )
12		opeq1 4402	. . . . 5 |- ( b = B -> <. b , d >. = <. B , d >. )
13	12	breq1d 4663	. . . 4 |- ( b = B -> ( <. b , d >.Cgr <. f , h >. <-> <. B , d >.Cgr <. f , h >. ) )
14	13	anbi2d 740	. . 3 |- ( 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 1399	. 2 |- ( 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 4403	. . . 4 |- ( c = C -> <. B , c >. = <. B , C >. )
17	16	breq2d 4665	. . 3 |- ( c = C -> ( A Colinear <. B , c >. <-> A Colinear <. B , C >. ) )
18	16	opeq2d 4409	. . . 4 |- ( c = C -> <. A , <. B , c >. >. = <. A , <. B , C >. >. )
19	18	breq1d 4663	. . 3 |- ( c = C -> ( <. A , <. B , c >. >.Cgr3 <. e , <. f , g >. >. <-> <. A , <. B , C >. >.Cgr3 <. e , <. f , g >. >. ) )
20	17, 19	3anbi12d 1400	. 2 |- ( 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 4403	. . . . 5 |- ( d = D -> <. A , d >. = <. A , D >. )
22	21	breq1d 4663	. . . 4 |- ( d = D -> ( <. A , d >.Cgr <. e , h >. <-> <. A , D >.Cgr <. e , h >. ) )
23		opeq2 4403	. . . . 5 |- ( d = D -> <. B , d >. = <. B , D >. )
24	23	breq1d 4663	. . . 4 |- ( d = D -> ( <. B , d >.Cgr <. f , h >. <-> <. B , D >.Cgr <. f , h >. ) )
25	22, 24	anbi12d 747	. . 3 |- ( 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 1405	. 2 |- ( 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 4402	. . . 4 |- ( e = E -> <. e , <. f , g >. >. = <. E , <. f , g >. >. )
28	27	breq2d 4665	. . 3 |- ( e = E -> ( <. A , <. B , C >. >.Cgr3 <. e , <. f , g >. >. <-> <. A , <. B , C >. >.Cgr3 <. E , <. f , g >. >. ) )
29		opeq1 4402	. . . . 5 |- ( e = E -> <. e , h >. = <. E , h >. )
30	29	breq2d 4665	. . . 4 |- ( e = E -> ( <. A , D >.Cgr <. e , h >. <-> <. A , D >.Cgr <. E , h >. ) )
31	30	anbi1d 741	. . 3 |- ( 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 1402	. 2 |- ( 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 4402	. . . . 5 |- ( f = F -> <. f , g >. = <. F , g >. )
34	33	opeq2d 4409	. . . 4 |- ( f = F -> <. E , <. f , g >. >. = <. E , <. F , g >. >. )
35	34	breq2d 4665	. . 3 |- ( f = F -> ( <. A , <. B , C >. >.Cgr3 <. E , <. f , g >. >. <-> <. A , <. B , C >. >.Cgr3 <. E , <. F , g >. >. ) )
36		opeq1 4402	. . . . 5 |- ( f = F -> <. f , h >. = <. F , h >. )
37	36	breq2d 4665	. . . 4 |- ( f = F -> ( <. B , D >.Cgr <. f , h >. <-> <. B , D >.Cgr <. F , h >. ) )
38	37	anbi2d 740	. . 3 |- ( 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 1402	. 2 |- ( 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 4403	. . . . 5 |- ( g = G -> <. F , g >. = <. F , G >. )
41	40	opeq2d 4409	. . . 4 |- ( g = G -> <. E , <. F , g >. >. = <. E , <. F , G >. >. )
42	41	breq2d 4665	. . 3 |- ( g = G -> ( <. A , <. B , C >. >.Cgr3 <. E , <. F , g >. >. <-> <. A , <. B , C >. >.Cgr3 <. E , <. F , G >. >. ) )
43	42	3anbi2d 1404	. 2 |- ( 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 4403	. . . . 5 |- ( h = H -> <. E , h >. = <. E , H >. )
45	44	breq2d 4665	. . . 4 |- ( h = H -> ( <. A , D >.Cgr <. E , h >. <-> <. A , D >.Cgr <. E , H >. ) )
46		opeq2 4403	. . . . 5 |- ( h = H -> <. F , h >. = <. F , H >. )
47	46	breq2d 4665	. . . 4 |- ( h = H -> ( <. B , D >.Cgr <. F , h >. <-> <. B , D >.Cgr <. F , H >. ) )
48	45, 47	anbi12d 747	. . 3 |- ( 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 1405	. 2 |- ( 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 6191	. 2 |- ( n = N -> ( EE ` n ) = ( EE ` N ) )
51		df-fs 32149	. 2 |- 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 31646	1 |- ( ( ( 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 >. ) ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   <.cop 4183   class class class wbr 4653   ` cfv 5888   NNcn 11020   EEcee 25768  Cgrccgr 25770  Cgr3ccgr3 32143   Colinear ccolin 32144   FiveSeg cfs 32145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-iota 5851  df-fv 5896  df-fs 32149

This theorem is referenced by:  fscgr  32187  linecgr  32188