Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cgr Unicode version

Definition df-cgr 24521
Description: Define the Euclidean congruence predicate. For details, see brcgr 24528. (Contributed by Scott Fenton, 3-Jun-2013.)
Assertion
Ref Expression
df-cgr  |- Cgr  =  { <. x ,  y >.  |  E. n  e.  NN  ( ( x  e.  ( ( EE `  n )  X.  ( EE `  n ) )  /\  y  e.  ( ( EE `  n
)  X.  ( EE
`  n ) ) )  /\  sum_ i  e.  ( 1 ... n
) ( ( ( ( 1st `  x
) `  i )  -  ( ( 2nd `  x ) `  i
) ) ^ 2 )  =  sum_ i  e.  ( 1 ... n
) ( ( ( ( 1st `  y
) `  i )  -  ( ( 2nd `  y ) `  i
) ) ^ 2 ) ) }
Distinct variable group:    x, n, y, i

Detailed syntax breakdown of Definition df-cgr
StepHypRef Expression
1 ccgr 24518 . 2  class Cgr
2 vx . . . . . . . 8  set  x
32cv 1622 . . . . . . 7  class  x
4 vn . . . . . . . . . 10  set  n
54cv 1622 . . . . . . . . 9  class  n
6 cee 24516 . . . . . . . . 9  class  EE
75, 6cfv 5255 . . . . . . . 8  class  ( EE
`  n )
87, 7cxp 4687 . . . . . . 7  class  ( ( EE `  n )  X.  ( EE `  n ) )
93, 8wcel 1684 . . . . . 6  wff  x  e.  ( ( EE `  n )  X.  ( EE `  n ) )
10 vy . . . . . . . 8  set  y
1110cv 1622 . . . . . . 7  class  y
1211, 8wcel 1684 . . . . . 6  wff  y  e.  ( ( EE `  n )  X.  ( EE `  n ) )
139, 12wa 358 . . . . 5  wff  ( x  e.  ( ( EE
`  n )  X.  ( EE `  n
) )  /\  y  e.  ( ( EE `  n )  X.  ( EE `  n ) ) )
14 c1 8738 . . . . . . . 8  class  1
15 cfz 10782 . . . . . . . 8  class  ...
1614, 5, 15co 5858 . . . . . . 7  class  ( 1 ... n )
17 vi . . . . . . . . . . 11  set  i
1817cv 1622 . . . . . . . . . 10  class  i
19 c1st 6120 . . . . . . . . . . 11  class  1st
203, 19cfv 5255 . . . . . . . . . 10  class  ( 1st `  x )
2118, 20cfv 5255 . . . . . . . . 9  class  ( ( 1st `  x ) `
 i )
22 c2nd 6121 . . . . . . . . . . 11  class  2nd
233, 22cfv 5255 . . . . . . . . . 10  class  ( 2nd `  x )
2418, 23cfv 5255 . . . . . . . . 9  class  ( ( 2nd `  x ) `
 i )
25 cmin 9037 . . . . . . . . 9  class  -
2621, 24, 25co 5858 . . . . . . . 8  class  ( ( ( 1st `  x
) `  i )  -  ( ( 2nd `  x ) `  i
) )
27 c2 9795 . . . . . . . 8  class  2
28 cexp 11104 . . . . . . . 8  class  ^
2926, 27, 28co 5858 . . . . . . 7  class  ( ( ( ( 1st `  x
) `  i )  -  ( ( 2nd `  x ) `  i
) ) ^ 2 )
3016, 29, 17csu 12158 . . . . . 6  class  sum_ i  e.  ( 1 ... n
) ( ( ( ( 1st `  x
) `  i )  -  ( ( 2nd `  x ) `  i
) ) ^ 2 )
3111, 19cfv 5255 . . . . . . . . . 10  class  ( 1st `  y )
3218, 31cfv 5255 . . . . . . . . 9  class  ( ( 1st `  y ) `
 i )
3311, 22cfv 5255 . . . . . . . . . 10  class  ( 2nd `  y )
3418, 33cfv 5255 . . . . . . . . 9  class  ( ( 2nd `  y ) `
 i )
3532, 34, 25co 5858 . . . . . . . 8  class  ( ( ( 1st `  y
) `  i )  -  ( ( 2nd `  y ) `  i
) )
3635, 27, 28co 5858 . . . . . . 7  class  ( ( ( ( 1st `  y
) `  i )  -  ( ( 2nd `  y ) `  i
) ) ^ 2 )
3716, 36, 17csu 12158 . . . . . 6  class  sum_ i  e.  ( 1 ... n
) ( ( ( ( 1st `  y
) `  i )  -  ( ( 2nd `  y ) `  i
) ) ^ 2 )
3830, 37wceq 1623 . . . . 5  wff  sum_ i  e.  ( 1 ... n
) ( ( ( ( 1st `  x
) `  i )  -  ( ( 2nd `  x ) `  i
) ) ^ 2 )  =  sum_ i  e.  ( 1 ... n
) ( ( ( ( 1st `  y
) `  i )  -  ( ( 2nd `  y ) `  i
) ) ^ 2 )
3913, 38wa 358 . . . 4  wff  ( ( x  e.  ( ( EE `  n )  X.  ( EE `  n ) )  /\  y  e.  ( ( EE `  n )  X.  ( EE `  n
) ) )  /\  sum_ i  e.  ( 1 ... n ) ( ( ( ( 1st `  x ) `  i
)  -  ( ( 2nd `  x ) `
 i ) ) ^ 2 )  = 
sum_ i  e.  ( 1 ... n ) ( ( ( ( 1st `  y ) `
 i )  -  ( ( 2nd `  y
) `  i )
) ^ 2 ) )
40 cn 9746 . . . 4  class  NN
4139, 4, 40wrex 2544 . . 3  wff  E. n  e.  NN  ( ( x  e.  ( ( EE
`  n )  X.  ( EE `  n
) )  /\  y  e.  ( ( EE `  n )  X.  ( EE `  n ) ) )  /\  sum_ i  e.  ( 1 ... n
) ( ( ( ( 1st `  x
) `  i )  -  ( ( 2nd `  x ) `  i
) ) ^ 2 )  =  sum_ i  e.  ( 1 ... n
) ( ( ( ( 1st `  y
) `  i )  -  ( ( 2nd `  y ) `  i
) ) ^ 2 ) )
4241, 2, 10copab 4076 . 2  class  { <. x ,  y >.  |  E. n  e.  NN  (
( x  e.  ( ( EE `  n
)  X.  ( EE
`  n ) )  /\  y  e.  ( ( EE `  n
)  X.  ( EE
`  n ) ) )  /\  sum_ i  e.  ( 1 ... n
) ( ( ( ( 1st `  x
) `  i )  -  ( ( 2nd `  x ) `  i
) ) ^ 2 )  =  sum_ i  e.  ( 1 ... n
) ( ( ( ( 1st `  y
) `  i )  -  ( ( 2nd `  y ) `  i
) ) ^ 2 ) ) }
431, 42wceq 1623 1  wff Cgr  =  { <. x ,  y >.  |  E. n  e.  NN  ( ( x  e.  ( ( EE `  n )  X.  ( EE `  n ) )  /\  y  e.  ( ( EE `  n
)  X.  ( EE
`  n ) ) )  /\  sum_ i  e.  ( 1 ... n
) ( ( ( ( 1st `  x
) `  i )  -  ( ( 2nd `  x ) `  i
) ) ^ 2 )  =  sum_ i  e.  ( 1 ... n
) ( ( ( ( 1st `  y
) `  i )  -  ( ( 2nd `  y ) `  i
) ) ^ 2 ) ) }
Colors of variables: wff set class
This definition is referenced by:  brcgr  24528
  Copyright terms: Public domain W3C validator