Metamath Proof Explorer

Theorem brafs

Description: Binary relation form of the outer five segment predicate. (Contributed by Scott Fenton, 21-Sep-2013)

Ref Expression
Hypotheses brafs.p 
|- P = ( Base ` G )
brafs.d 
|- .- = ( dist ` G )
brafs.i 
|- I = ( Itv ` G )
brafs.g 
|- ( ph -> G e. TarskiG )
brafs.o 
|- O = ( AFS ` G )
brafs.1 
|- ( ph -> A e. P )
brafs.2 
|- ( ph -> B e. P )
brafs.3 
|- ( ph -> C e. P )
brafs.4 
|- ( ph -> D e. P )
brafs.5 
|- ( ph -> X e. P )
brafs.6 
|- ( ph -> Y e. P )
brafs.7 
|- ( ph -> Z e. P )
brafs.8 
|- ( ph -> W e. P )
Assertion brafs 
|- ( ph -> ( <. <. A , B >. , <. C , D >. >. O <. <. X , Y >. , <. Z , W >. >. <-> ( ( B e. ( A I C ) /\ Y e. ( X I Z ) ) /\ ( ( A .- B ) = ( X .- Y ) /\ ( B .- C ) = ( Y .- Z ) ) /\ ( ( A .- D ) = ( X .- W ) /\ ( B .- D ) = ( Y .- W ) ) ) ) )

Proof

Step Hyp Ref Expression
1 brafs.p 
 |-  P = ( Base ` G )
2 brafs.d 
 |-  .- = ( dist ` G )
3 brafs.i 
 |-  I = ( Itv ` G )
4 brafs.g 
 |-  ( ph -> G e. TarskiG )
5 brafs.o 
 |-  O = ( AFS ` G )
6 brafs.1 
 |-  ( ph -> A e. P )
7 brafs.2 
 |-  ( ph -> B e. P )
8 brafs.3 
 |-  ( ph -> C e. P )
9 brafs.4 
 |-  ( ph -> D e. P )
10 brafs.5 
 |-  ( ph -> X e. P )
11 brafs.6 
 |-  ( ph -> Y e. P )
12 brafs.7 
 |-  ( ph -> Z e. P )
13 brafs.8 
 |-  ( ph -> W e. P )
14 oveq1 
 |-  ( a = A -> ( a I c ) = ( A I c ) )
15 14 eleq2d 
 |-  ( a = A -> ( b e. ( a I c ) <-> b e. ( A I c ) ) )
16 15 anbi1d 
 |-  ( a = A -> ( ( b e. ( a I c ) /\ y e. ( x I z ) ) <-> ( b e. ( A I c ) /\ y e. ( x I z ) ) ) )
17 oveq1 
 |-  ( a = A -> ( a .- b ) = ( A .- b ) )
18 17 eqeq1d 
 |-  ( a = A -> ( ( a .- b ) = ( x .- y ) <-> ( A .- b ) = ( x .- y ) ) )
19 18 anbi1d 
 |-  ( a = A -> ( ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) <-> ( ( A .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) ) )
20 oveq1 
 |-  ( a = A -> ( a .- d ) = ( A .- d ) )
21 20 eqeq1d 
 |-  ( a = A -> ( ( a .- d ) = ( x .- w ) <-> ( A .- d ) = ( x .- w ) ) )
22 21 anbi1d 
 |-  ( a = A -> ( ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) <-> ( ( A .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) )
23 16 19 22 3anbi123d 
 |-  ( a = A -> ( ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) <-> ( ( b e. ( A I c ) /\ y e. ( x I z ) ) /\ ( ( A .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( A .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) )
24 eleq1 
 |-  ( b = B -> ( b e. ( A I c ) <-> B e. ( A I c ) ) )
25 24 anbi1d 
 |-  ( b = B -> ( ( b e. ( A I c ) /\ y e. ( x I z ) ) <-> ( B e. ( A I c ) /\ y e. ( x I z ) ) ) )
26 oveq2 
 |-  ( b = B -> ( A .- b ) = ( A .- B ) )
27 26 eqeq1d 
 |-  ( b = B -> ( ( A .- b ) = ( x .- y ) <-> ( A .- B ) = ( x .- y ) ) )
28 oveq1 
 |-  ( b = B -> ( b .- c ) = ( B .- c ) )
29 28 eqeq1d 
 |-  ( b = B -> ( ( b .- c ) = ( y .- z ) <-> ( B .- c ) = ( y .- z ) ) )
30 27 29 anbi12d 
 |-  ( b = B -> ( ( ( A .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) <-> ( ( A .- B ) = ( x .- y ) /\ ( B .- c ) = ( y .- z ) ) ) )
31 oveq1 
 |-  ( b = B -> ( b .- d ) = ( B .- d ) )
32 31 eqeq1d 
 |-  ( b = B -> ( ( b .- d ) = ( y .- w ) <-> ( B .- d ) = ( y .- w ) ) )
33 32 anbi2d 
 |-  ( b = B -> ( ( ( A .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) <-> ( ( A .- d ) = ( x .- w ) /\ ( B .- d ) = ( y .- w ) ) ) )
34 25 30 33 3anbi123d 
 |-  ( b = B -> ( ( ( b e. ( A I c ) /\ y e. ( x I z ) ) /\ ( ( A .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( A .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) <-> ( ( B e. ( A I c ) /\ y e. ( x I z ) ) /\ ( ( A .- B ) = ( x .- y ) /\ ( B .- c ) = ( y .- z ) ) /\ ( ( A .- d ) = ( x .- w ) /\ ( B .- d ) = ( y .- w ) ) ) ) )
35 oveq2 
 |-  ( c = C -> ( A I c ) = ( A I C ) )
36 35 eleq2d 
 |-  ( c = C -> ( B e. ( A I c ) <-> B e. ( A I C ) ) )
37 36 anbi1d 
 |-  ( c = C -> ( ( B e. ( A I c ) /\ y e. ( x I z ) ) <-> ( B e. ( A I C ) /\ y e. ( x I z ) ) ) )
38 oveq2 
 |-  ( c = C -> ( B .- c ) = ( B .- C ) )
39 38 eqeq1d 
 |-  ( c = C -> ( ( B .- c ) = ( y .- z ) <-> ( B .- C ) = ( y .- z ) ) )
40 39 anbi2d 
 |-  ( c = C -> ( ( ( A .- B ) = ( x .- y ) /\ ( B .- c ) = ( y .- z ) ) <-> ( ( A .- B ) = ( x .- y ) /\ ( B .- C ) = ( y .- z ) ) ) )
41 37 40 3anbi12d 
 |-  ( c = C -> ( ( ( B e. ( A I c ) /\ y e. ( x I z ) ) /\ ( ( A .- B ) = ( x .- y ) /\ ( B .- c ) = ( y .- z ) ) /\ ( ( A .- d ) = ( x .- w ) /\ ( B .- d ) = ( y .- w ) ) ) <-> ( ( B e. ( A I C ) /\ y e. ( x I z ) ) /\ ( ( A .- B ) = ( x .- y ) /\ ( B .- C ) = ( y .- z ) ) /\ ( ( A .- d ) = ( x .- w ) /\ ( B .- d ) = ( y .- w ) ) ) ) )
42 oveq2 
 |-  ( d = D -> ( A .- d ) = ( A .- D ) )
43 42 eqeq1d 
 |-  ( d = D -> ( ( A .- d ) = ( x .- w ) <-> ( A .- D ) = ( x .- w ) ) )
44 oveq2 
 |-  ( d = D -> ( B .- d ) = ( B .- D ) )
45 44 eqeq1d 
 |-  ( d = D -> ( ( B .- d ) = ( y .- w ) <-> ( B .- D ) = ( y .- w ) ) )
46 43 45 anbi12d 
 |-  ( d = D -> ( ( ( A .- d ) = ( x .- w ) /\ ( B .- d ) = ( y .- w ) ) <-> ( ( A .- D ) = ( x .- w ) /\ ( B .- D ) = ( y .- w ) ) ) )
47 46 3anbi3d 
 |-  ( d = D -> ( ( ( B e. ( A I C ) /\ y e. ( x I z ) ) /\ ( ( A .- B ) = ( x .- y ) /\ ( B .- C ) = ( y .- z ) ) /\ ( ( A .- d ) = ( x .- w ) /\ ( B .- d ) = ( y .- w ) ) ) <-> ( ( B e. ( A I C ) /\ y e. ( x I z ) ) /\ ( ( A .- B ) = ( x .- y ) /\ ( B .- C ) = ( y .- z ) ) /\ ( ( A .- D ) = ( x .- w ) /\ ( B .- D ) = ( y .- w ) ) ) ) )
48 oveq1 
 |-  ( x = X -> ( x I z ) = ( X I z ) )
49 48 eleq2d 
 |-  ( x = X -> ( y e. ( x I z ) <-> y e. ( X I z ) ) )
50 49 anbi2d 
 |-  ( x = X -> ( ( B e. ( A I C ) /\ y e. ( x I z ) ) <-> ( B e. ( A I C ) /\ y e. ( X I z ) ) ) )
51 oveq1 
 |-  ( x = X -> ( x .- y ) = ( X .- y ) )
52 51 eqeq2d 
 |-  ( x = X -> ( ( A .- B ) = ( x .- y ) <-> ( A .- B ) = ( X .- y ) ) )
53 52 anbi1d 
 |-  ( x = X -> ( ( ( A .- B ) = ( x .- y ) /\ ( B .- C ) = ( y .- z ) ) <-> ( ( A .- B ) = ( X .- y ) /\ ( B .- C ) = ( y .- z ) ) ) )
54 oveq1 
 |-  ( x = X -> ( x .- w ) = ( X .- w ) )
55 54 eqeq2d 
 |-  ( x = X -> ( ( A .- D ) = ( x .- w ) <-> ( A .- D ) = ( X .- w ) ) )
56 55 anbi1d 
 |-  ( x = X -> ( ( ( A .- D ) = ( x .- w ) /\ ( B .- D ) = ( y .- w ) ) <-> ( ( A .- D ) = ( X .- w ) /\ ( B .- D ) = ( y .- w ) ) ) )
57 50 53 56 3anbi123d 
 |-  ( x = X -> ( ( ( B e. ( A I C ) /\ y e. ( x I z ) ) /\ ( ( A .- B ) = ( x .- y ) /\ ( B .- C ) = ( y .- z ) ) /\ ( ( A .- D ) = ( x .- w ) /\ ( B .- D ) = ( y .- w ) ) ) <-> ( ( B e. ( A I C ) /\ y e. ( X I z ) ) /\ ( ( A .- B ) = ( X .- y ) /\ ( B .- C ) = ( y .- z ) ) /\ ( ( A .- D ) = ( X .- w ) /\ ( B .- D ) = ( y .- w ) ) ) ) )
58 eleq1 
 |-  ( y = Y -> ( y e. ( X I z ) <-> Y e. ( X I z ) ) )
59 58 anbi2d 
 |-  ( y = Y -> ( ( B e. ( A I C ) /\ y e. ( X I z ) ) <-> ( B e. ( A I C ) /\ Y e. ( X I z ) ) ) )
60 oveq2 
 |-  ( y = Y -> ( X .- y ) = ( X .- Y ) )
61 60 eqeq2d 
 |-  ( y = Y -> ( ( A .- B ) = ( X .- y ) <-> ( A .- B ) = ( X .- Y ) ) )
62 oveq1 
 |-  ( y = Y -> ( y .- z ) = ( Y .- z ) )
63 62 eqeq2d 
 |-  ( y = Y -> ( ( B .- C ) = ( y .- z ) <-> ( B .- C ) = ( Y .- z ) ) )
64 61 63 anbi12d 
 |-  ( y = Y -> ( ( ( A .- B ) = ( X .- y ) /\ ( B .- C ) = ( y .- z ) ) <-> ( ( A .- B ) = ( X .- Y ) /\ ( B .- C ) = ( Y .- z ) ) ) )
65 oveq1 
 |-  ( y = Y -> ( y .- w ) = ( Y .- w ) )
66 65 eqeq2d 
 |-  ( y = Y -> ( ( B .- D ) = ( y .- w ) <-> ( B .- D ) = ( Y .- w ) ) )
67 66 anbi2d 
 |-  ( y = Y -> ( ( ( A .- D ) = ( X .- w ) /\ ( B .- D ) = ( y .- w ) ) <-> ( ( A .- D ) = ( X .- w ) /\ ( B .- D ) = ( Y .- w ) ) ) )
68 59 64 67 3anbi123d 
 |-  ( y = Y -> ( ( ( B e. ( A I C ) /\ y e. ( X I z ) ) /\ ( ( A .- B ) = ( X .- y ) /\ ( B .- C ) = ( y .- z ) ) /\ ( ( A .- D ) = ( X .- w ) /\ ( B .- D ) = ( y .- w ) ) ) <-> ( ( B e. ( A I C ) /\ Y e. ( X I z ) ) /\ ( ( A .- B ) = ( X .- Y ) /\ ( B .- C ) = ( Y .- z ) ) /\ ( ( A .- D ) = ( X .- w ) /\ ( B .- D ) = ( Y .- w ) ) ) ) )
69 oveq2 
 |-  ( z = Z -> ( X I z ) = ( X I Z ) )
70 69 eleq2d 
 |-  ( z = Z -> ( Y e. ( X I z ) <-> Y e. ( X I Z ) ) )
71 70 anbi2d 
 |-  ( z = Z -> ( ( B e. ( A I C ) /\ Y e. ( X I z ) ) <-> ( B e. ( A I C ) /\ Y e. ( X I Z ) ) ) )
72 oveq2 
 |-  ( z = Z -> ( Y .- z ) = ( Y .- Z ) )
73 72 eqeq2d 
 |-  ( z = Z -> ( ( B .- C ) = ( Y .- z ) <-> ( B .- C ) = ( Y .- Z ) ) )
74 73 anbi2d 
 |-  ( z = Z -> ( ( ( A .- B ) = ( X .- Y ) /\ ( B .- C ) = ( Y .- z ) ) <-> ( ( A .- B ) = ( X .- Y ) /\ ( B .- C ) = ( Y .- Z ) ) ) )
75 71 74 3anbi12d 
 |-  ( z = Z -> ( ( ( B e. ( A I C ) /\ Y e. ( X I z ) ) /\ ( ( A .- B ) = ( X .- Y ) /\ ( B .- C ) = ( Y .- z ) ) /\ ( ( A .- D ) = ( X .- w ) /\ ( B .- D ) = ( Y .- w ) ) ) <-> ( ( B e. ( A I C ) /\ Y e. ( X I Z ) ) /\ ( ( A .- B ) = ( X .- Y ) /\ ( B .- C ) = ( Y .- Z ) ) /\ ( ( A .- D ) = ( X .- w ) /\ ( B .- D ) = ( Y .- w ) ) ) ) )
76 oveq2 
 |-  ( w = W -> ( X .- w ) = ( X .- W ) )
77 76 eqeq2d 
 |-  ( w = W -> ( ( A .- D ) = ( X .- w ) <-> ( A .- D ) = ( X .- W ) ) )
78 oveq2 
 |-  ( w = W -> ( Y .- w ) = ( Y .- W ) )
79 78 eqeq2d 
 |-  ( w = W -> ( ( B .- D ) = ( Y .- w ) <-> ( B .- D ) = ( Y .- W ) ) )
80 77 79 anbi12d 
 |-  ( w = W -> ( ( ( A .- D ) = ( X .- w ) /\ ( B .- D ) = ( Y .- w ) ) <-> ( ( A .- D ) = ( X .- W ) /\ ( B .- D ) = ( Y .- W ) ) ) )
81 80 3anbi3d 
 |-  ( w = W -> ( ( ( B e. ( A I C ) /\ Y e. ( X I Z ) ) /\ ( ( A .- B ) = ( X .- Y ) /\ ( B .- C ) = ( Y .- Z ) ) /\ ( ( A .- D ) = ( X .- w ) /\ ( B .- D ) = ( Y .- w ) ) ) <-> ( ( B e. ( A I C ) /\ Y e. ( X I Z ) ) /\ ( ( A .- B ) = ( X .- Y ) /\ ( B .- C ) = ( Y .- Z ) ) /\ ( ( A .- D ) = ( X .- W ) /\ ( B .- D ) = ( Y .- W ) ) ) ) )
82 1 2 3 4 afsval 
 |-  ( ph -> ( AFS ` G ) = { <. e , f >. | E. a e. P E. b e. P E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) } )
83 5 82 eqtrid 
 |-  ( ph -> O = { <. e , f >. | E. a e. P E. b e. P E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) } )
84 23 34 41 47 57 68 75 81 83 6 7 8 9 10 11 12 13 br8d 
 |-  ( ph -> ( <. <. A , B >. , <. C , D >. >. O <. <. X , Y >. , <. Z , W >. >. <-> ( ( B e. ( A I C ) /\ Y e. ( X I Z ) ) /\ ( ( A .- B ) = ( X .- Y ) /\ ( B .- C ) = ( Y .- Z ) ) /\ ( ( A .- D ) = ( X .- W ) /\ ( B .- D ) = ( Y .- W ) ) ) ) )