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

Theorem afsval 29276
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 29275 . . 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 1005 . . . . . . 7  |-  ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  ->  p  =  P )
76eqcomd 2437 . . . . . 6  |-  ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  ->  P  =  p )
87adantr 466 . . . . . . 7  |-  ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P
)  ->  P  =  p )
98adantr 466 . . . . . . . 8  |-  ( ( ( ( p  =  P  /\  h  = 
.-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  ->  P  =  p )
109adantr 466 . . . . . . . . 9  |-  ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  ->  P  =  p )
1110adantr 466 . . . . . . . . . 10  |-  ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P )  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  ->  P  =  p )
1211adantr 466 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  /\  a  e.  P
)  /\  b  e.  P )  /\  c  e.  P )  /\  d  e.  P )  /\  x  e.  P )  ->  P  =  p )
1312adantr 466 . . . . . . . . . . . 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 )
147ad7antr 742 . . . . . . . . . . . . 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 1007 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  ->  i  =  I )
1615ad8antr 744 . . . . . . . . . . . . . . . . . . 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 2437 . . . . . . . . . . . . . . . . . 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 6322 . . . . . . . . . . . . . . . . 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 2499 . . . . . . . . . . . . . . . 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 6322 . . . . . . . . . . . . . . . . 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 2499 . . . . . . . . . . . . . . . 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 715 . . . . . . . . . . . . . . 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 1006 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  ->  h  =  .-  )
2423eqcomd 2437 . . . . . . . . . . . . . . . . . . 19  |-  ( ( p  =  P  /\  h  =  .-  /\  i  =  I )  ->  .-  =  h )
2524ad8antr 744 . . . . . . . . . . . . . . . . . 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 6322 . . . . . . . . . . . . . . . . 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 6322 . . . . . . . . . . . . . . . . 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 2451 . . . . . . . . . . . . . . . 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 6322 . . . . . . . . . . . . . . . . 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 6322 . . . . . . . . . . . . . . . . 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 2451 . . . . . . . . . . . . . . . 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 715 . . . . . . . . . . . . . . 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 6322 . . . . . . . . . . . . . . . . 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 6322 . . . . . . . . . . . . . . . . 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 2451 . . . . . . . . . . . . . . . 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 6322 . . . . . . . . . . . . . . . . 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 6322 . . . . . . . . . . . . . . . . 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 2451 . . . . . . . . . . . . . . . 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 715 . . . . . . . . . . . . . . 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 1335 . . . . . . . . . . . . . 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 1341 . . . . . . . . . . . . 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 3049 . . . . . . . . . . . 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 3049 . . . . . . . . . . 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 3049 . . . . . . . . . 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 3049 . . . . . . . . 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 3049 . . . . . . . 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 3049 . . . . . . 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 3049 . . . . . 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 3049 . . . . 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 15130 . . . 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 467 . . 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 4489 . 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 4860 . . . . 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 5891 . . . . . . . . 9  |-  ( Base `  G )  e.  _V
563, 55eqeltri 2513 . . . . . . . 8  |-  P  e. 
_V
5756, 56xpex 6609 . . . . . . 7  |-  ( P  X.  P )  e. 
_V
5857, 57xpex 6609 . . . . . 6  |-  ( ( P  X.  P )  X.  ( P  X.  P ) )  e. 
_V
5958, 58xpex 6609 . . . . 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 1002 . . . . . . . . . . . . . 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 2900 . . . . . . . . . . . . 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 2900 . . . . . . . . . . . 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 2900 . . . . . . . . . . 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 2900 . . . . . . . . . 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 2900 . . . . . . . . 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 2900 . . . . . . . 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 2900 . . . . . . 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 2900 . . . . . 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 462 . . . . . . . . . . . . . . . 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 >. >. )  ->  e  =  <. <. a ,  b
>. ,  <. c ,  d >. >. )
71 opelxpi 4886 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  e.  P  /\  b  e.  P )  -> 
<. a ,  b >.  e.  ( P  X.  P
) )
7271ad7antr 742 . . . . . . . . . . . . . . . . 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 >. >. )  ->  <. a ,  b >.  e.  ( P  X.  P ) )
73 simp-7r 781 . . . . . . . . . . . . . . . . . 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 >. >. )  ->  c  e.  P )
74 simp-6r 779 . . . . . . . . . . . . . . . . . 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 >. >. )  ->  d  e.  P )
75 opelxpi 4886 . . . . . . . . . . . . . . . . . 18  |-  ( ( c  e.  P  /\  d  e.  P )  -> 
<. c ,  d >.  e.  ( P  X.  P
) )
7673, 74, 75syl2anc 665 . . . . . . . . . . . . . . . . 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 >. >. )  ->  <. c ,  d >.  e.  ( P  X.  P ) )
77 opelxpi 4886 . . . . . . . . . . . . . . . . 17  |-  ( (
<. a ,  b >.  e.  ( P  X.  P
)  /\  <. c ,  d >.  e.  ( P  X.  P ) )  ->  <. <. a ,  b
>. ,  <. c ,  d >. >.  e.  ( ( P  X.  P )  X.  ( P  X.  P ) ) )
7872, 76, 77syl2anc 665 . . . . . . . . . . . . . . . 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 >. >. )  ->  <. <. a ,  b >. ,  <. c ,  d >. >.  e.  ( ( P  X.  P
)  X.  ( P  X.  P ) ) )
7970, 78eqeltrd 2517 . . . . . . . . . . . . . . 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 >. >. )  ->  e  e.  ( ( P  X.  P )  X.  ( P  X.  P ) ) )
80 simpr 462 . . . . . . . . . . . . . . . 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 )  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. )  ->  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. )
81 simp-5r 777 . . . . . . . . . . . . . . . . . 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  e.  P )
82 simp-4r 775 . . . . . . . . . . . . . . . . . 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 >. >. )  ->  y  e.  P )
83 opelxpi 4886 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  P  /\  y  e.  P )  -> 
<. x ,  y >.  e.  ( P  X.  P
) )
8481, 82, 83syl2anc 665 . . . . . . . . . . . . . . . . 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 >. >. )  ->  <. x ,  y >.  e.  ( P  X.  P ) )
85 simpllr 767 . . . . . . . . . . . . . . . . . 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 >. >. )  ->  z  e.  P )
86 simplr 760 . . . . . . . . . . . . . . . . . 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 >. >. )  ->  w  e.  P )
87 opelxpi 4886 . . . . . . . . . . . . . . . . . 18  |-  ( ( z  e.  P  /\  w  e.  P )  -> 
<. z ,  w >.  e.  ( P  X.  P
) )
8885, 86, 87syl2anc 665 . . . . . . . . . . . . . . . . 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 >. >. )  ->  <. z ,  w >.  e.  ( P  X.  P ) )
89 opelxpi 4886 . . . . . . . . . . . . . . . . 17  |-  ( (
<. x ,  y >.  e.  ( P  X.  P
)  /\  <. z ,  w >.  e.  ( P  X.  P ) )  ->  <. <. x ,  y
>. ,  <. z ,  w >. >.  e.  ( ( P  X.  P )  X.  ( P  X.  P ) ) )
9084, 88, 89syl2anc 665 . . . . . . . . . . . . . . . 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 )  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. )  ->  <. <. x ,  y >. ,  <. z ,  w >. >.  e.  ( ( P  X.  P
)  X.  ( P  X.  P ) ) )
9180, 90eqeltrd 2517 . . . . . . . . . . . . . . 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 )  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >. )  ->  f  e.  ( ( P  X.  P )  X.  ( P  X.  P ) ) )
9279, 91anim12dan 845 . . . . . . . . . . . . . 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 ) ) ) )
9392ex 435 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( 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
) ) ) ) )
9493rexlimdva 2924 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( 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
) ) ) ) )
9594rexlimdva 2924 . . . . . . . . . . 11  |-  ( ( ( ( ( ( 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
) ) ) ) )
9695rexlimdva 2924 . . . . . . . . . 10  |-  ( ( ( ( ( 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
) ) ) ) )
9796rexlimdva 2924 . . . . . . . . 9  |-  ( ( ( ( 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
) ) ) ) )
9897rexlimdva 2924 . . . . . . . 8  |-  ( ( ( 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
) ) ) ) )
9998rexlimdva 2924 . . . . . . 7  |-  ( ( 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
) ) ) ) )
10099rexlimivv 2929 . . . . . 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
) ) ) )
10169, 100syl 17 . . . . 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 ) ) ) )
102101ssopab2i 4749 . . . 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
) ) ) }
10360, 102ssexi 4570 . . 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
104103a1i 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 )
1052, 52, 53, 104fvmptd 5970 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 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1870   E.wrex 2783   _Vcvv 3087   [.wsbc 3305   <.cop 4008   {copab 4483    |-> cmpt 4484    X. cxp 4852   ` cfv 5601  (class class class)co 6305   Basecbs 15084   distcds 15161  TarskiGcstrkg 24341  Itvcitv 24347  AFScafs 29274
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-mpt 4486  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-iota 5565  df-fun 5603  df-fv 5609  df-ov 6308  df-afs 29275
This theorem is referenced by:  brafs  29277
  Copyright terms: Public domain W3C validator