Definition df-cgr 29475

Description: Define the Euclidean congruence predicate. For details, see brcgr 29483. (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

Step	Hyp	Ref	Expression
1		ccgr 29472	. 2 class Cgr
2		vx	. . . . . . . 8 setvar 𝑥
3	2	cv 1568	. . . . . . 7 class 𝑥
4		vn	. . . . . . . . . 10 setvar 𝑛
5	4	cv 1568	. . . . . . . . 9 class 𝑛
6		cee 29470	. . . . . . . . 9 class 𝔼
7	5, 6	cfv 6538	. . . . . . . 8 class (𝔼‘𝑛)
8	7, 7	cxp 5648	. . . . . . 7 class ((𝔼‘𝑛) × (𝔼‘𝑛))
9	3, 8	wcel 2144	. . . . . 6 wff 𝑥 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))
10		vy	. . . . . . . 8 setvar 𝑦
11	10	cv 1568	. . . . . . 7 class 𝑦
12	11, 8	wcel 2144	. . . . . 6 wff 𝑦 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))
13	9, 12	wa 401	. . . . 5 wff (𝑥 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑦 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)))
14		c1 11204	. . . . . . . 8 class 1
15		cfz 13642	. . . . . . . 8 class ...
16	14, 5, 15	co 7420	. . . . . . 7 class (1...𝑛)
17		vi	. . . . . . . . . . 11 setvar 𝑖
18	17	cv 1568	. . . . . . . . . 10 class 𝑖
19		c1st 7999	. . . . . . . . . . 11 class 1st
20	3, 19	cfv 6538	. . . . . . . . . 10 class (1st ‘𝑥)
21	18, 20	cfv 6538	. . . . . . . . 9 class ((1st ‘𝑥)‘𝑖)
22		c2nd 8000	. . . . . . . . . . 11 class 2nd
23	3, 22	cfv 6538	. . . . . . . . . 10 class (2nd ‘𝑥)
24	18, 23	cfv 6538	. . . . . . . . 9 class ((2nd ‘𝑥)‘𝑖)
25		cmin 11544	. . . . . . . . 9 class −
26	21, 24, 25	co 7420	. . . . . . . 8 class (((1st ‘𝑥)‘𝑖) − ((2nd ‘𝑥)‘𝑖))
27		c2 12400	. . . . . . . 8 class 2
28		cexp 14207	. . . . . . . 8 class ↑
29	26, 27, 28	co 7420	. . . . . . 7 class ((((1st ‘𝑥)‘𝑖) − ((2nd ‘𝑥)‘𝑖))↑2)
30	16, 29, 17	csu 15858	. . . . . 6 class Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑥)‘𝑖) − ((2nd ‘𝑥)‘𝑖))↑2)
31	11, 19	cfv 6538	. . . . . . . . . 10 class (1st ‘𝑦)
32	18, 31	cfv 6538	. . . . . . . . 9 class ((1st ‘𝑦)‘𝑖)
33	11, 22	cfv 6538	. . . . . . . . . 10 class (2nd ‘𝑦)
34	18, 33	cfv 6538	. . . . . . . . 9 class ((2nd ‘𝑦)‘𝑖)
35	32, 34, 25	co 7420	. . . . . . . 8 class (((1st ‘𝑦)‘𝑖) − ((2nd ‘𝑦)‘𝑖))
36	35, 27, 28	co 7420	. . . . . . 7 class ((((1st ‘𝑦)‘𝑖) − ((2nd ‘𝑦)‘𝑖))↑2)
37	16, 36, 17	csu 15858	. . . . . 6 class Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑦)‘𝑖) − ((2nd ‘𝑦)‘𝑖))↑2)
38	30, 37	wceq 1569	. . . . 5 wff Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑥)‘𝑖) − ((2nd ‘𝑥)‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑦)‘𝑖) − ((2nd ‘𝑦)‘𝑖))↑2)
39	13, 38	wa 401	. . . 4 wff ((𝑥 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑦 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))) ∧ Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑥)‘𝑖) − ((2nd ‘𝑥)‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑦)‘𝑖) − ((2nd ‘𝑦)‘𝑖))↑2))
40		cn 12338	. . . 4 class ℕ
41	39, 4, 40	wrex 3086	. . 3 wff ∃𝑛 ∈ ℕ ((𝑥 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑦 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))) ∧ Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑥)‘𝑖) − ((2nd ‘𝑥)‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑦)‘𝑖) − ((2nd ‘𝑦)‘𝑖))↑2))
42	41, 2, 10	copab 5166	. 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑦 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))) ∧ Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑥)‘𝑖) − ((2nd ‘𝑥)‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑦)‘𝑖) − ((2nd ‘𝑦)‘𝑖))↑2))}
43	1, 42	wceq 1569	1 wff Cgr = {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑦 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))) ∧ Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑥)‘𝑖) − ((2nd ‘𝑥)‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑦)‘𝑖) − ((2nd ‘𝑦)‘𝑖))↑2))}

This definition is used by:  brcgr  29483