Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  afsval Structured version   Unicode version

Theorem afsval 26995
Description: Value of the AFS relation for a given geometry structure. (Contributed by Thierry Arnoux, 20-Mar-2019.)
Hypotheses
Ref Expression
brafs.p  |-  P  =  ( Base `  G
)
brafs.d  |-  .-  =  ( dist `  G )
brafs.i  |-  I  =  (Itv `  G )
brafs.g  |-  ( ph  ->  G  e. TarskiG )
Assertion
Ref Expression
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 ) ) ) ) } )
Distinct variable groups:    e, f, G    a, b, c, d, w, x, y, z, I    e, a, f, P, b, c, d, w, x, y, z    .- , a, b, c, d, w, x, y, z    ph, e, f
Allowed substitution hints:    ph( x, y, z, w, a, b, c, d)    G( x, y, z, w, a, b, c, d)    I(
e, f)    .- ( e, f)

Proof of Theorem afsval
Dummy variables  g  h  i  p are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-afs 26994 . . 3  |- AFS  =  ( g  e. TarskiG  |->  { <. e ,  f >.  |  [. ( Base `  g )  /  p ]. [. ( dist `  g )  /  h ]. [. (Itv `  g )  /  i ]. 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 h b )  =  ( x h y )  /\  ( b h c )  =  ( y h z ) )  /\  (
( a h d )  =  ( x h w )  /\  ( b h d )  =  ( y h w ) ) ) ) } )
21a1i 11 . 2  |-  ( ph  -> AFS  =  ( g  e. TarskiG  |->  { <. e ,  f
>.  |  [. ( Base `  g )  /  p ]. [. ( dist `  g
)  /  h ]. [. (Itv `  g )  /  i ]. 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 h b )  =  ( x h y )  /\  ( b h c )  =  ( y h z ) )  /\  (
( a h d )  =  ( x h w )  /\  ( b h d )  =  ( y h w ) ) ) ) } ) )
3 brafs.p . . . . 5  |-  P  =  ( Base `  G
)
4 brafs.d . . . . 5  |-  .-  =  ( dist `  G )
5 brafs.i . . . . 5  |-  I  =  (Itv `  G )
6 simp1 988 . . . . . . 7  |-  ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  ->  p  =  P )
76eqcomd 2448 . . . . . 6  |-  ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  ->  P  =  p )
87adantr 465 . . . . . . 7  |-  ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P
)  ->  P  =  p )
98adantr 465 . . . . . . . 8  |-  ( ( ( ( p  =  P  /\  h  = 
.-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  ->  P  =  p )
109adantr 465 . . . . . . . . 9  |-  ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  ->  P  =  p )
1110adantr 465 . . . . . . . . . 10  |-  ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  ->  P  =  p )
1211adantr 465 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P
)  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  ->  P  =  p )
1312adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( p  =  P  /\  h  = 
.-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  ->  P  =  p )
1413adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  ->  P  =  p )
15 simp3 990 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  ->  i  =  I )
1615ad8antr 739 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  i  =  I )
1716eqcomd 2448 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  I  =  i )
1817oveqd 6108 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  (
a I c )  =  ( a i c ) )
1918eleq2d 2510 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  (
b  e.  ( a I c )  <->  b  e.  ( a i c ) ) )
2017oveqd 6108 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  (
x I z )  =  ( x i z ) )
2120eleq2d 2510 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  (
y  e.  ( x I z )  <->  y  e.  ( x i z ) ) )
2219, 21anbi12d 710 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  (
( b  e.  ( a I c )  /\  y  e.  ( x I z ) )  <->  ( b  e.  ( a i c )  /\  y  e.  ( x i z ) ) ) )
23 simp2 989 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  ->  h  =  .-  )
2423eqcomd 2448 . . . . . . . . . . . . . . . . . . 19  |-  ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  ->  .-  =  h )
2524ad8antr 739 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  .-  =  h )
2625oveqd 6108 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  (
a  .-  b )  =  ( a h b ) )
2725oveqd 6108 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  (
x  .-  y )  =  ( x h y ) )
2826, 27eqeq12d 2457 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  (
( a  .-  b
)  =  ( x 
.-  y )  <->  ( a
h b )  =  ( x h y ) ) )
2925oveqd 6108 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  (
b  .-  c )  =  ( b h c ) )
3025oveqd 6108 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  (
y  .-  z )  =  ( y h z ) )
3129, 30eqeq12d 2457 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  (
( b  .-  c
)  =  ( y 
.-  z )  <->  ( b
h c )  =  ( y h z ) ) )
3228, 31anbi12d 710 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  (
( ( a  .-  b )  =  ( x  .-  y )  /\  ( b  .-  c )  =  ( y  .-  z ) )  <->  ( ( a h b )  =  ( x h y )  /\  ( b h c )  =  ( y h z ) ) ) )
3325oveqd 6108 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  (
a  .-  d )  =  ( a h d ) )
3425oveqd 6108 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  (
x  .-  w )  =  ( x h w ) )
3533, 34eqeq12d 2457 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  (
( a  .-  d
)  =  ( x 
.-  w )  <->  ( a
h d )  =  ( x h w ) ) )
3625oveqd 6108 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  (
b  .-  d )  =  ( b h d ) )
3725oveqd 6108 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  (
y  .-  w )  =  ( y h w ) )
3836, 37eqeq12d 2457 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  (
( b  .-  d
)  =  ( y 
.-  w )  <->  ( b
h d )  =  ( y h w ) ) )
3935, 38anbi12d 710 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  (
( ( a  .-  d )  =  ( x  .-  w )  /\  ( b  .-  d )  =  ( y  .-  w ) )  <->  ( ( a h d )  =  ( x h w )  /\  ( b h d )  =  ( y h w ) ) ) )
4022, 32, 393anbi123d 1289 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  (
( ( 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 h b )  =  ( x h y )  /\  ( b h c )  =  ( y h z ) )  /\  (
( a h d )  =  ( x h w )  /\  ( b h d )  =  ( y h w ) ) ) ) )
41403anbi3d 1295 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  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 ) ) ) )  <->  ( e  = 
<. <. a ,  b
>. ,  <. c ,  d >. >.  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >.  /\  ( (
b  e.  ( a i c )  /\  y  e.  ( x
i z ) )  /\  ( ( a h b )  =  ( x h y )  /\  ( b h c )  =  ( y h z ) )  /\  (
( a h d )  =  ( x h w )  /\  ( b h d )  =  ( y h w ) ) ) ) ) )
4214, 41rexeqbidva 2934 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  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 ) ) ) )  <->  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 h b )  =  ( x h y )  /\  ( b h c )  =  ( y h z ) )  /\  (
( a h d )  =  ( x h w )  /\  ( b h d )  =  ( y h w ) ) ) ) ) )
4313, 42rexeqbidva 2934 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( p  =  P  /\  h  = 
.-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  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 ) ) ) )  <->  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 h b )  =  ( x h y )  /\  ( b h c )  =  ( y h z ) )  /\  (
( a h d )  =  ( x h w )  /\  ( b h d )  =  ( y h w ) ) ) ) ) )
4412, 43rexeqbidva 2934 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P
)  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  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 ) ) ) )  <->  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 h b )  =  ( x h y )  /\  ( b h c )  =  ( y h z ) )  /\  (
( a h d )  =  ( x h w )  /\  ( b h d )  =  ( y h w ) ) ) ) ) )
4511, 44rexeqbidva 2934 . . . . . . . . 9  |-  ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  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 ) ) ) )  <->  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 h b )  =  ( x h y )  /\  ( b h c )  =  ( y h z ) )  /\  (
( a h d )  =  ( x h w )  /\  ( b h d )  =  ( y h w ) ) ) ) ) )
4610, 45rexeqbidva 2934 . . . . . . . 8  |-  ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  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 ) ) ) )  <->  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 h b )  =  ( x h y )  /\  ( b h c )  =  ( y h z ) )  /\  (
( a h d )  =  ( x h w )  /\  ( b h d )  =  ( y h w ) ) ) ) ) )
479, 46rexeqbidva 2934 . . . . . . 7  |-  ( ( ( ( p  =  P  /\  h  = 
.-  /\  i  =  I )  /\  a  e.  P )  /\  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 ) ) ) )  <->  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 h b )  =  ( x h y )  /\  ( b h c )  =  ( y h z ) )  /\  (
( a h d )  =  ( x h w )  /\  ( b h d )  =  ( y h w ) ) ) ) ) )
488, 47rexeqbidva 2934 . . . . . 6  |-  ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  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 ) ) ) )  <->  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 h b )  =  ( x h y )  /\  ( b h c )  =  ( y h z ) )  /\  (
( a h d )  =  ( x h w )  /\  ( b h d )  =  ( y h w ) ) ) ) ) )
497, 48rexeqbidva 2934 . . . . 5  |-  ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  ->  ( 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 ) ) ) )  <->  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 h b )  =  ( x h y )  /\  ( b h c )  =  ( y h z ) )  /\  (
( a h d )  =  ( x h w )  /\  ( b h d )  =  ( y h w ) ) ) ) ) )
503, 4, 5, 49sbcie3s 14218 . . . 4  |-  ( g  =  G  ->  ( [. ( Base `  g
)  /  p ]. [. ( dist `  g
)  /  h ]. [. (Itv `  g )  /  i ]. 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 h b )  =  ( x h y )  /\  ( b h c )  =  ( y h z ) )  /\  (
( a h d )  =  ( x h w )  /\  ( b h d )  =  ( y h w ) ) ) )  <->  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 ) ) ) ) ) )
5150adantl 466 . . 3  |-  ( (
ph  /\  g  =  G )  ->  ( [. ( Base `  g
)  /  p ]. [. ( dist `  g
)  /  h ]. [. (Itv `  g )  /  i ]. 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 h b )  =  ( x h y )  /\  ( b h c )  =  ( y h z ) )  /\  (
( a h d )  =  ( x h w )  /\  ( b h d )  =  ( y h w ) ) ) )  <->  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 ) ) ) ) ) )
5251opabbidv 4355 . 2  |-  ( (
ph  /\  g  =  G )  ->  { <. e ,  f >.  |  [. ( Base `  g )  /  p ]. [. ( dist `  g )  /  h ]. [. (Itv `  g )  /  i ]. 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 h b )  =  ( x h y )  /\  ( b h c )  =  ( y h z ) )  /\  (
( a h d )  =  ( x h w )  /\  ( b h d )  =  ( y h w ) ) ) ) }  =  { <. 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 ) ) ) ) } )
53 brafs.g . 2  |-  ( ph  ->  G  e. TarskiG )
54 df-xp 4846 . . . . 5  |-  ( ( ( P  X.  P
)  X.  ( P  X.  P ) )  X.  ( ( P  X.  P )  X.  ( P  X.  P
) ) )  =  { <. e ,  f
>.  |  ( e  e.  ( ( P  X.  P )  X.  ( P  X.  P ) )  /\  f  e.  ( ( P  X.  P
)  X.  ( P  X.  P ) ) ) }
55 fvex 5701 . . . . . . . . 9  |-  ( Base `  G )  e.  _V
563, 55eqeltri 2513 . . . . . . . 8  |-  P  e. 
_V
5756, 56xpex 6508 . . . . . . 7  |-  ( P  X.  P )  e. 
_V
5857, 57xpex 6508 . . . . . 6  |-  ( ( P  X.  P )  X.  ( P  X.  P ) )  e. 
_V
5958, 58xpex 6508 . . . . 5  |-  ( ( ( P  X.  P
)  X.  ( P  X.  P ) )  X.  ( ( P  X.  P )  X.  ( P  X.  P
) ) )  e. 
_V
6054, 59eqeltrri 2514 . . . 4  |-  { <. e ,  f >.  |  ( e  e.  ( ( P  X.  P )  X.  ( P  X.  P ) )  /\  f  e.  ( ( P  X.  P )  X.  ( P  X.  P
) ) ) }  e.  _V
61 3simpa 985 . . . . . . . . . . . . . 14  |-  ( ( 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 ) ) ) )  ->  ( e  =  <. <. a ,  b
>. ,  <. c ,  d >. >.  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. ) )
6261reximi 2823 . . . . . . . . . . . . 13  |-  ( 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 ) ) ) )  ->  E. w  e.  P  ( e  =  <. <. a ,  b
>. ,  <. c ,  d >. >.  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. ) )
6362reximi 2823 . . . . . . . . . . . 12  |-  ( 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 ) ) ) )  ->  E. z  e.  P  E. w  e.  P  ( e  =  <. <. a ,  b
>. ,  <. c ,  d >. >.  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. ) )
6463reximi 2823 . . . . . . . . . . 11  |-  ( 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 ) ) ) )  ->  E. y  e.  P  E. z  e.  P  E. w  e.  P  ( e  =  <. <. a ,  b
>. ,  <. c ,  d >. >.  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. ) )
6564reximi 2823 . . . . . . . . . 10  |-  ( 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 ) ) ) )  ->  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 >. >. ) )
6665reximi 2823 . . . . . . . . 9  |-  ( 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 ) ) ) )  ->  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 >. >. ) )
6766reximi 2823 . . . . . . . 8  |-  ( 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 ) ) ) )  ->  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 >. >. ) )
6867reximi 2823 . . . . . . 7  |-  ( 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 ) ) ) )  ->  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 >. >. ) )
6968reximi 2823 . . . . . 6  |-  ( 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 ) ) ) )  ->  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 >. >. ) )
70 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  /\  e  =  <. <. a ,  b
>. ,  <. c ,  d >. >. )  ->  e  =  <. <. a ,  b
>. ,  <. c ,  d >. >. )
71 simp-8l 773 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  /\  e  =  <. <. a ,  b
>. ,  <. c ,  d >. >. )  ->  a  e.  P )
72 simp-8r 774 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  /\  e  =  <. <. a ,  b
>. ,  <. c ,  d >. >. )  ->  b  e.  P )
73 opelxpi 4871 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  P  /\  b  e.  P )  -> 
<. a ,  b >.  e.  ( P  X.  P
) )
7471, 72, 73syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  /\  e  =  <. <. a ,  b
>. ,  <. c ,  d >. >. )  ->  <. a ,  b >.  e.  ( P  X.  P ) )
75 simp-7r 772 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  /\  e  =  <. <. a ,  b
>. ,  <. c ,  d >. >. )  ->  c  e.  P )
76 simp-6r 770 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  /\  e  =  <. <. a ,  b
>. ,  <. c ,  d >. >. )  ->  d  e.  P )
77 opelxpi 4871 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( c  e.  P  /\  d  e.  P )  -> 
<. c ,  d >.  e.  ( P  X.  P
) )
7875, 76, 77syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  /\  e  =  <. <. a ,  b
>. ,  <. c ,  d >. >. )  ->  <. c ,  d >.  e.  ( P  X.  P ) )
79 opelxpi 4871 . . . . . . . . . . . . . . . . . . 19  |-  ( (
<. a ,  b >.  e.  ( P  X.  P
)  /\  <. c ,  d >.  e.  ( P  X.  P ) )  ->  <. <. a ,  b
>. ,  <. c ,  d >. >.  e.  ( ( P  X.  P )  X.  ( P  X.  P ) ) )
8074, 78, 79syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  /\  e  =  <. <. a ,  b
>. ,  <. c ,  d >. >. )  ->  <. <. a ,  b >. ,  <. c ,  d >. >.  e.  ( ( P  X.  P
)  X.  ( P  X.  P ) ) )
8170, 80eqeltrd 2517 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  /\  e  =  <. <. a ,  b
>. ,  <. c ,  d >. >. )  ->  e  e.  ( ( P  X.  P )  X.  ( P  X.  P ) ) )
8281adantrr 716 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  /\  (
e  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. ) )  -> 
e  e.  ( ( P  X.  P )  X.  ( P  X.  P ) ) )
83 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. )  ->  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. )
84 simp-5r 768 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. )  ->  x  e.  P )
85 simp-4r 766 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. )  ->  y  e.  P )
86 opelxpi 4871 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  P  /\  y  e.  P )  -> 
<. x ,  y >.  e.  ( P  X.  P
) )
8784, 85, 86syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. )  ->  <. x ,  y >.  e.  ( P  X.  P ) )
88 simpllr 758 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. )  ->  z  e.  P )
89 simplr 754 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. )  ->  w  e.  P )
90 opelxpi 4871 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( z  e.  P  /\  w  e.  P )  -> 
<. z ,  w >.  e.  ( P  X.  P
) )
9188, 89, 90syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. )  ->  <. z ,  w >.  e.  ( P  X.  P ) )
92 opelxpi 4871 . . . . . . . . . . . . . . . . . . 19  |-  ( (
<. x ,  y >.  e.  ( P  X.  P
)  /\  <. z ,  w >.  e.  ( P  X.  P ) )  ->  <. <. x ,  y
>. ,  <. z ,  w >. >.  e.  ( ( P  X.  P )  X.  ( P  X.  P ) ) )
9387, 91, 92syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. )  ->  <. <. x ,  y >. ,  <. z ,  w >. >.  e.  ( ( P  X.  P
)  X.  ( P  X.  P ) ) )
9483, 93eqeltrd 2517 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. )  ->  f  e.  ( ( P  X.  P )  X.  ( P  X.  P ) ) )
9594adantrl 715 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  /\  (
e  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. ) )  -> 
f  e.  ( ( P  X.  P )  X.  ( P  X.  P ) ) )
9682, 95jca 532 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  /\  (
e  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. ) )  -> 
( e  e.  ( ( P  X.  P
)  X.  ( P  X.  P ) )  /\  f  e.  ( ( P  X.  P
)  X.  ( P  X.  P ) ) ) )
9796ex 434 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  /\  w  e.  P )  ->  (
( e  =  <. <.
a ,  b >. ,  <. c ,  d
>. >.  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. )  ->  (
e  e.  ( ( P  X.  P )  X.  ( P  X.  P ) )  /\  f  e.  ( ( P  X.  P )  X.  ( P  X.  P
) ) ) ) )
9897rexlimdva 2841 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( a  e.  P  /\  b  e.  P
)  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  /\  z  e.  P )  ->  ( E. w  e.  P  ( e  =  <. <.
a ,  b >. ,  <. c ,  d
>. >.  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. )  ->  (
e  e.  ( ( P  X.  P )  X.  ( P  X.  P ) )  /\  f  e.  ( ( P  X.  P )  X.  ( P  X.  P
) ) ) ) )
9998rexlimdva 2841 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  x  e.  P )  /\  y  e.  P )  ->  ( E. z  e.  P  E. w  e.  P  ( e  =  <. <.
a ,  b >. ,  <. c ,  d
>. >.  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. )  ->  (
e  e.  ( ( P  X.  P )  X.  ( P  X.  P ) )  /\  f  e.  ( ( P  X.  P )  X.  ( P  X.  P
) ) ) ) )
10099rexlimdva 2841 . . . . . . . . . . 11  |-  ( ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  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 >. >. )  ->  (
e  e.  ( ( P  X.  P )  X.  ( P  X.  P ) )  /\  f  e.  ( ( P  X.  P )  X.  ( P  X.  P
) ) ) ) )
101100rexlimdva 2841 . . . . . . . . . 10  |-  ( ( ( ( a  e.  P  /\  b  e.  P )  /\  c  e.  P )  /\  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 >. >. )  ->  (
e  e.  ( ( P  X.  P )  X.  ( P  X.  P ) )  /\  f  e.  ( ( P  X.  P )  X.  ( P  X.  P
) ) ) ) )
102101rexlimdva 2841 . . . . . . . . 9  |-  ( ( ( a  e.  P  /\  b  e.  P
)  /\  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 >. >. )  ->  (
e  e.  ( ( P  X.  P )  X.  ( P  X.  P ) )  /\  f  e.  ( ( P  X.  P )  X.  ( P  X.  P
) ) ) ) )
103102rexlimdva 2841 . . . . . . . 8  |-  ( ( a  e.  P  /\  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 >. >. )  ->  (
e  e.  ( ( P  X.  P )  X.  ( P  X.  P ) )  /\  f  e.  ( ( P  X.  P )  X.  ( P  X.  P
) ) ) ) )
104103rexlimdva 2841 . . . . . . 7  |-  ( 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 >. >. )  ->  (
e  e.  ( ( P  X.  P )  X.  ( P  X.  P ) )  /\  f  e.  ( ( P  X.  P )  X.  ( P  X.  P
) ) ) ) )
105104rexlimiv 2835 . . . . . 6  |-  ( 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 >. >. )  ->  (
e  e.  ( ( P  X.  P )  X.  ( P  X.  P ) )  /\  f  e.  ( ( P  X.  P )  X.  ( P  X.  P
) ) ) )
10669, 105syl 16 . . . . 5  |-  ( 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 ) ) ) )  ->  ( e  e.  ( ( P  X.  P )  X.  ( P  X.  P ) )  /\  f  e.  ( ( P  X.  P
)  X.  ( P  X.  P ) ) ) )
107106ssopab2i 4616 . . . 4  |-  { <. 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 ) ) ) ) }  C_  { <. e ,  f >.  |  ( e  e.  ( ( P  X.  P )  X.  ( P  X.  P ) )  /\  f  e.  ( ( P  X.  P )  X.  ( P  X.  P
) ) ) }
10860, 107ssexi 4437 . . 3  |-  { <. 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 ) ) ) ) }  e.  _V
109108a1i 11 . 2  |-  ( ph  ->  { <. 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 ) ) ) ) }  e.  _V )
1102, 52, 53, 109fvmptd 5779 1  |-  ( 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 ) ) ) ) } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756   E.wrex 2716   _Vcvv 2972   [.wsbc 3186   <.cop 3883   {copab 4349    e. cmpt 4350    X. cxp 4838   ` cfv 5418  (class class class)co 6091   Basecbs 14174   distcds 14247  TarskiGcstrkg 22889  Itvcitv 22897  AFScafs 26993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-iota 5381  df-fun 5420  df-fv 5426  df-ov 6094  df-afs 26994
This theorem is referenced by:  brafs  26996
  Copyright terms: Public domain W3C validator