Metamath Proof Explorer

Definition df-cgr

Description: Define the Euclidean congruence predicate. For details, see brcgr . (Contributed by Scott Fenton, 3-Jun-2013)

Ref Expression
Assertion 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 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccgr 
 |-  Cgr
1 vx 
 |-  x
2 vy 
 |-  y
3 vn 
 |-  n
4 cn 
 |-  NN
5 1 cv 
 |-  x
6 cee 
 |-  EE
7 3 cv 
 |-  n
8 7 6 cfv 
 |-  ( EE ` n )
9 8 8 cxp 
 |-  ( ( EE ` n ) X. ( EE ` n ) )
10 5 9 wcel 
 |-  x e. ( ( EE ` n ) X. ( EE ` n ) )
11 2 cv 
 |-  y
12 11 9 wcel 
 |-  y e. ( ( EE ` n ) X. ( EE ` n ) )
13 10 12 wa 
 |-  ( x e. ( ( EE ` n ) X. ( EE ` n ) ) /\ y e. ( ( EE ` n ) X. ( EE ` n ) ) )
14 vi 
 |-  i
15 c1 
 |-  1
16 cfz 
 |-  ...
17 15 7 16 co 
 |-  ( 1 ... n )
18 c1st 
 |-  1st
19 5 18 cfv 
 |-  ( 1st ` x )
20 14 cv 
 |-  i
21 20 19 cfv 
 |-  ( ( 1st ` x ) ` i )
22 cmin 
 |-  -
23 c2nd 
 |-  2nd
24 5 23 cfv 
 |-  ( 2nd ` x )
25 20 24 cfv 
 |-  ( ( 2nd ` x ) ` i )
26 21 25 22 co 
 |-  ( ( ( 1st ` x ) ` i ) - ( ( 2nd ` x ) ` i ) )
27 cexp 
 |-  ^
28 c2 
 |-  2
29 26 28 27 co 
 |-  ( ( ( ( 1st ` x ) ` i ) - ( ( 2nd ` x ) ` i ) ) ^ 2 )
30 17 29 14 csu 
 |-  sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` x ) ` i ) - ( ( 2nd ` x ) ` i ) ) ^ 2 )
31 11 18 cfv 
 |-  ( 1st ` y )
32 20 31 cfv 
 |-  ( ( 1st ` y ) ` i )
33 11 23 cfv 
 |-  ( 2nd ` y )
34 20 33 cfv 
 |-  ( ( 2nd ` y ) ` i )
35 32 34 22 co 
 |-  ( ( ( 1st ` y ) ` i ) - ( ( 2nd ` y ) ` i ) )
36 35 28 27 co 
 |-  ( ( ( ( 1st ` y ) ` i ) - ( ( 2nd ` y ) ` i ) ) ^ 2 )
37 17 36 14 csu 
 |-  sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` y ) ` i ) - ( ( 2nd ` y ) ` i ) ) ^ 2 )
38 30 37 wceq 
 |-  sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` x ) ` i ) - ( ( 2nd ` x ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` y ) ` i ) - ( ( 2nd ` y ) ` i ) ) ^ 2 )
39 13 38 wa 
 |-  ( ( 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 39 3 4 wrex 
 |-  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 ) )
41 40 1 2 copab 
 |-  { <. 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 ) ) }
42 0 41 wceq 
 |-  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 ) ) }