MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cgr Structured version   Visualization version   GIF version

Definition df-cgr 26984
Description: Define the Euclidean congruence predicate. For details, see brcgr 26991. (Contributed by Scott Fenton, 3-Jun-2013.)
Assertion
Ref Expression
df-cgr Cgr = {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑦 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))) ∧ Σ𝑖 ∈ (1...𝑛)((((1st𝑥)‘𝑖) − ((2nd𝑥)‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑛)((((1st𝑦)‘𝑖) − ((2nd𝑦)‘𝑖))↑2))}
Distinct variable group:   𝑥,𝑛,𝑦,𝑖

Detailed syntax breakdown of Definition df-cgr
StepHypRef Expression
1 ccgr 26981 . 2 class Cgr
2 vx . . . . . . . 8 setvar 𝑥
32cv 1542 . . . . . . 7 class 𝑥
4 vn . . . . . . . . . 10 setvar 𝑛
54cv 1542 . . . . . . . . 9 class 𝑛
6 cee 26979 . . . . . . . . 9 class 𝔼
75, 6cfv 6380 . . . . . . . 8 class (𝔼‘𝑛)
87, 7cxp 5549 . . . . . . 7 class ((𝔼‘𝑛) × (𝔼‘𝑛))
93, 8wcel 2110 . . . . . 6 wff 𝑥 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))
10 vy . . . . . . . 8 setvar 𝑦
1110cv 1542 . . . . . . 7 class 𝑦
1211, 8wcel 2110 . . . . . 6 wff 𝑦 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))
139, 12wa 399 . . . . 5 wff (𝑥 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑦 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)))
14 c1 10730 . . . . . . . 8 class 1
15 cfz 13095 . . . . . . . 8 class ...
1614, 5, 15co 7213 . . . . . . 7 class (1...𝑛)
17 vi . . . . . . . . . . 11 setvar 𝑖
1817cv 1542 . . . . . . . . . 10 class 𝑖
19 c1st 7759 . . . . . . . . . . 11 class 1st
203, 19cfv 6380 . . . . . . . . . 10 class (1st𝑥)
2118, 20cfv 6380 . . . . . . . . 9 class ((1st𝑥)‘𝑖)
22 c2nd 7760 . . . . . . . . . . 11 class 2nd
233, 22cfv 6380 . . . . . . . . . 10 class (2nd𝑥)
2418, 23cfv 6380 . . . . . . . . 9 class ((2nd𝑥)‘𝑖)
25 cmin 11062 . . . . . . . . 9 class
2621, 24, 25co 7213 . . . . . . . 8 class (((1st𝑥)‘𝑖) − ((2nd𝑥)‘𝑖))
27 c2 11885 . . . . . . . 8 class 2
28 cexp 13635 . . . . . . . 8 class
2926, 27, 28co 7213 . . . . . . 7 class ((((1st𝑥)‘𝑖) − ((2nd𝑥)‘𝑖))↑2)
3016, 29, 17csu 15249 . . . . . 6 class Σ𝑖 ∈ (1...𝑛)((((1st𝑥)‘𝑖) − ((2nd𝑥)‘𝑖))↑2)
3111, 19cfv 6380 . . . . . . . . . 10 class (1st𝑦)
3218, 31cfv 6380 . . . . . . . . 9 class ((1st𝑦)‘𝑖)
3311, 22cfv 6380 . . . . . . . . . 10 class (2nd𝑦)
3418, 33cfv 6380 . . . . . . . . 9 class ((2nd𝑦)‘𝑖)
3532, 34, 25co 7213 . . . . . . . 8 class (((1st𝑦)‘𝑖) − ((2nd𝑦)‘𝑖))
3635, 27, 28co 7213 . . . . . . 7 class ((((1st𝑦)‘𝑖) − ((2nd𝑦)‘𝑖))↑2)
3716, 36, 17csu 15249 . . . . . 6 class Σ𝑖 ∈ (1...𝑛)((((1st𝑦)‘𝑖) − ((2nd𝑦)‘𝑖))↑2)
3830, 37wceq 1543 . . . . 5 wff Σ𝑖 ∈ (1...𝑛)((((1st𝑥)‘𝑖) − ((2nd𝑥)‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑛)((((1st𝑦)‘𝑖) − ((2nd𝑦)‘𝑖))↑2)
3913, 38wa 399 . . . 4 wff ((𝑥 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑦 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))) ∧ Σ𝑖 ∈ (1...𝑛)((((1st𝑥)‘𝑖) − ((2nd𝑥)‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑛)((((1st𝑦)‘𝑖) − ((2nd𝑦)‘𝑖))↑2))
40 cn 11830 . . . 4 class
4139, 4, 40wrex 3062 . . 3 wff 𝑛 ∈ ℕ ((𝑥 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑦 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))) ∧ Σ𝑖 ∈ (1...𝑛)((((1st𝑥)‘𝑖) − ((2nd𝑥)‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑛)((((1st𝑦)‘𝑖) − ((2nd𝑦)‘𝑖))↑2))
4241, 2, 10copab 5115 . 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑦 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))) ∧ Σ𝑖 ∈ (1...𝑛)((((1st𝑥)‘𝑖) − ((2nd𝑥)‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑛)((((1st𝑦)‘𝑖) − ((2nd𝑦)‘𝑖))↑2))}
431, 42wceq 1543 1 wff Cgr = {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑦 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))) ∧ Σ𝑖 ∈ (1...𝑛)((((1st𝑥)‘𝑖) − ((2nd𝑥)‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑛)((((1st𝑦)‘𝑖) − ((2nd𝑦)‘𝑖))↑2))}
Colors of variables: wff setvar class
This definition is referenced by:  brcgr  26991
  Copyright terms: Public domain W3C validator