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⟩ \| \exists n \in ℕ ((x \in (𝔼 (n) \times 𝔼 (n)) \land y \in (𝔼 (n) \times 𝔼 (n))) \land \sum_{i = 1}^{n} {(1^{st} (x) (i) - 2^{nd} (x) (i))}^{2} = \sum_{i = 1}^{n} {(1^{st} (y) (i) - 2^{nd} (y) (i))}^{2})\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccgr	$class Cgr$
1		vx	$setvar x$
2		vy	$setvar y$
3		vn	$setvar n$
4		cn	$class ℕ$
5	1	cv	$setvar x$
6		cee	$class 𝔼$
7	3	cv	$setvar n$
8	7 6	cfv	$class 𝔼 (n)$
9	8 8	cxp	$class (𝔼 (n) \times 𝔼 (n))$
10	5 9	wcel	$wff x \in (𝔼 (n) \times 𝔼 (n))$
11	2	cv	$setvar y$
12	11 9	wcel	$wff y \in (𝔼 (n) \times 𝔼 (n))$
13	10 12	wa	$wff (x \in (𝔼 (n) \times 𝔼 (n)) \land y \in (𝔼 (n) \times 𝔼 (n)))$
14		vi	$setvar i$
15		c1	$class 1$
16		cfz	$class \dots$
17	15 7 16	co	$class (1 \dots n)$
18		c1st	$class 1^{st}$
19	5 18	cfv	$class 1^{st} (x)$
20	14	cv	$setvar i$
21	20 19	cfv	$class 1^{st} (x) (i)$
22		cmin	$class -$
23		c2nd	$class 2^{nd}$
24	5 23	cfv	$class 2^{nd} (x)$
25	20 24	cfv	$class 2^{nd} (x) (i)$
26	21 25 22	co	$class (1^{st} (x) (i) - 2^{nd} (x) (i))$
27		cexp	$class^$
28		c2	$class 2$
29	26 28 27	co	$class {(1^{st} (x) (i) - 2^{nd} (x) (i))}^{2}$
30	17 29 14	csu	$class \sum_{i = 1}^{n} {(1^{st} (x) (i) - 2^{nd} (x) (i))}^{2}$
31	11 18	cfv	$class 1^{st} (y)$
32	20 31	cfv	$class 1^{st} (y) (i)$
33	11 23	cfv	$class 2^{nd} (y)$
34	20 33	cfv	$class 2^{nd} (y) (i)$
35	32 34 22	co	$class (1^{st} (y) (i) - 2^{nd} (y) (i))$
36	35 28 27	co	$class {(1^{st} (y) (i) - 2^{nd} (y) (i))}^{2}$
37	17 36 14	csu	$class \sum_{i = 1}^{n} {(1^{st} (y) (i) - 2^{nd} (y) (i))}^{2}$
38	30 37	wceq	$wff \sum_{i = 1}^{n} {(1^{st} (x) (i) - 2^{nd} (x) (i))}^{2} = \sum_{i = 1}^{n} {(1^{st} (y) (i) - 2^{nd} (y) (i))}^{2}$
39	13 38	wa	$wff ((x \in (𝔼 (n) \times 𝔼 (n)) \land y \in (𝔼 (n) \times 𝔼 (n))) \land \sum_{i = 1}^{n} {(1^{st} (x) (i) - 2^{nd} (x) (i))}^{2} = \sum_{i = 1}^{n} {(1^{st} (y) (i) - 2^{nd} (y) (i))}^{2})$
40	39 3 4	wrex	$wff \exists n \in ℕ ((x \in (𝔼 (n) \times 𝔼 (n)) \land y \in (𝔼 (n) \times 𝔼 (n))) \land \sum_{i = 1}^{n} {(1^{st} (x) (i) - 2^{nd} (x) (i))}^{2} = \sum_{i = 1}^{n} {(1^{st} (y) (i) - 2^{nd} (y) (i))}^{2})$
41	40 1 2	copab	$class \{⟨x, y⟩ \| \exists n \in ℕ ((x \in (𝔼 (n) \times 𝔼 (n)) \land y \in (𝔼 (n) \times 𝔼 (n))) \land \sum_{i = 1}^{n} {(1^{st} (x) (i) - 2^{nd} (x) (i))}^{2} = \sum_{i = 1}^{n} {(1^{st} (y) (i) - 2^{nd} (y) (i))}^{2})\}$
42	0 41	wceq	$wff Cgr = \{⟨x, y⟩ \| \exists n \in ℕ ((x \in (𝔼 (n) \times 𝔼 (n)) \land y \in (𝔼 (n) \times 𝔼 (n))) \land \sum_{i = 1}^{n} {(1^{st} (x) (i) - 2^{nd} (x) (i))}^{2} = \sum_{i = 1}^{n} {(1^{st} (y) (i) - 2^{nd} (y) (i))}^{2})\}$

Metamath Proof Explorer

Definition df-cgr

Detailed syntax breakdown