Definition df-cgrg 28579

Description: Define the relation of congruence between shapes. Definition 4.4 of [Schwabhauser] p. 35. A "shape" is a finite sequence of points, and a triangle can be represented as a shape with three points. Two shapes are congruent if all corresponding segments between all corresponding points are congruent.

Many systems of geometry define triangle congruence as requiring both segment congruence and angle congruence. Such systems, such as Hilbert's axiomatic system, typically have a primitive notion of angle congruence in addition to segment congruence. Here, angle congruence is instead a derived notion, defined later in df-cgra 28876 and expanded in iscgra 28877. This does not mean our system is weaker; dfcgrg2 28931 proves that these two definitions are equivalent, and using the Tarski definition instead (given in [Schwabhauser] p. 35) is simpler. Once two triangles are proven congruent as defined here, you can use various theorems to prove that corresponding parts of congruent triangles are congruent (CPCTC). For example, see cgr3simp1 28588, cgr3simp2 28589, cgr3simp3 28590, cgrcgra 28889, and permutation laws such as cgr3swap12 28591 and dfcgrg2 28931.

Ideally, we would define this for functions of any set, but we will use words (see df-word 14476) in most cases.

(Contributed by Thierry Arnoux, 3-Apr-2019.)

Assertion

Ref	Expression
df-cgrg	⊢ cgrG = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))})

Distinct variable group:   𝑎,𝑏,𝑔,𝑖,𝑗

Detailed syntax breakdown of Definition df-cgrg

Step	Hyp	Ref	Expression
1		ccgrg 28578	. 2 class cgrG
2		vg	. . 3 setvar 𝑔
3		cvv 3429	. . 3 class V
4		va	. . . . . . . 8 setvar 𝑎
5	4	cv 1541	. . . . . . 7 class 𝑎
6	2	cv 1541	. . . . . . . . 9 class 𝑔
7		cbs 17179	. . . . . . . . 9 class Base
8	6, 7	cfv 6498	. . . . . . . 8 class (Base‘𝑔)
9		cr 11037	. . . . . . . 8 class ℝ
10		cpm 8774	. . . . . . . 8 class ↑pm
11	8, 9, 10	co 7367	. . . . . . 7 class ((Base‘𝑔) ↑pm ℝ)
12	5, 11	wcel 2114	. . . . . 6 wff 𝑎 ∈ ((Base‘𝑔) ↑pm ℝ)
13		vb	. . . . . . . 8 setvar 𝑏
14	13	cv 1541	. . . . . . 7 class 𝑏
15	14, 11	wcel 2114	. . . . . 6 wff 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)
16	12, 15	wa 395	. . . . 5 wff (𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ))
17	5	cdm 5631	. . . . . . 7 class dom 𝑎
18	14	cdm 5631	. . . . . . 7 class dom 𝑏
19	17, 18	wceq 1542	. . . . . 6 wff dom 𝑎 = dom 𝑏
20		vi	. . . . . . . . . . . 12 setvar 𝑖
21	20	cv 1541	. . . . . . . . . . 11 class 𝑖
22	21, 5	cfv 6498	. . . . . . . . . 10 class (𝑎‘𝑖)
23		vj	. . . . . . . . . . . 12 setvar 𝑗
24	23	cv 1541	. . . . . . . . . . 11 class 𝑗
25	24, 5	cfv 6498	. . . . . . . . . 10 class (𝑎‘𝑗)
26		cds 17229	. . . . . . . . . . 11 class dist
27	6, 26	cfv 6498	. . . . . . . . . 10 class (dist‘𝑔)
28	22, 25, 27	co 7367	. . . . . . . . 9 class ((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗))
29	21, 14	cfv 6498	. . . . . . . . . 10 class (𝑏‘𝑖)
30	24, 14	cfv 6498	. . . . . . . . . 10 class (𝑏‘𝑗)
31	29, 30, 27	co 7367	. . . . . . . . 9 class ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))
32	28, 31	wceq 1542	. . . . . . . 8 wff ((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))
33	32, 23, 17	wral 3051	. . . . . . 7 wff ∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))
34	33, 20, 17	wral 3051	. . . . . 6 wff ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))
35	19, 34	wa 395	. . . . 5 wff (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)))
36	16, 35	wa 395	. . . 4 wff ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))
37	36, 4, 13	copab 5147	. . 3 class {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))}
38	2, 3, 37	cmpt 5166	. 2 class (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))})
39	1, 38	wceq 1542	1 wff cgrG = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))})

This definition is referenced by:  iscgrg  28580  ercgrg  28585