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 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑥 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ↑ 2 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccgr	⊢ Cgr
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3		vn	⊢ 𝑛
4		cn	⊢ ℕ
5	1	cv	⊢ 𝑥
6		cee	⊢ 𝔼
7	3	cv	⊢ 𝑛
8	7 6	cfv	⊢ ( 𝔼 ‘ 𝑛 )
9	8 8	cxp	⊢ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) )
10	5 9	wcel	⊢ 𝑥 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) )
11	2	cv	⊢ 𝑦
12	11 9	wcel	⊢ 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) )
13	10 12	wa	⊢ ( 𝑥 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) )
14		vi	⊢ 𝑖
15		c1	⊢ 1
16		cfz	⊢ ...
17	15 7 16	co	⊢ ( 1 ... 𝑛 )
18		c1st	⊢ 1^st
19	5 18	cfv	⊢ ( 1^st ‘ 𝑥 )
20	14	cv	⊢ 𝑖
21	20 19	cfv	⊢ ( ( 1^st ‘ 𝑥 ) ‘ 𝑖 )
22		cmin	⊢ −
23		c2nd	⊢ 2^nd
24	5 23	cfv	⊢ ( 2^nd ‘ 𝑥 )
25	20 24	cfv	⊢ ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 )
26	21 25 22	co	⊢ ( ( ( 1^st ‘ 𝑥 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) )
27		cexp	⊢ ↑
28		c2	⊢ 2
29	26 28 27	co	⊢ ( ( ( ( 1^st ‘ 𝑥 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) ) ↑ 2 )
30	17 29 14	csu	⊢ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑥 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) ) ↑ 2 )
31	11 18	cfv	⊢ ( 1^st ‘ 𝑦 )
32	20 31	cfv	⊢ ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 )
33	11 23	cfv	⊢ ( 2^nd ‘ 𝑦 )
34	20 33	cfv	⊢ ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 )
35	32 34 22	co	⊢ ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) )
36	35 28 27	co	⊢ ( ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ↑ 2 )
37	17 36 14	csu	⊢ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ↑ 2 )
38	30 37	wceq	⊢ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑥 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ↑ 2 )
39	13 38	wa	⊢ ( ( 𝑥 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑥 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ↑ 2 ) )
40	39 3 4	wrex	⊢ ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑥 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ↑ 2 ) )
41	40 1 2	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑥 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ↑ 2 ) ) }
42	0 41	wceq	⊢ Cgr = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑥 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ↑ 2 ) ) }

Metamath Proof Explorer

Definition df-cgr

Detailed syntax breakdown