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

Definition df-cgrg 28265
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 28562 and expanded in iscgra 28563. This does not mean our system is weaker; dfcgrg2 28617 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 28274, cgr3simp2 28275, cgr3simp3 28276, cgrcgra 28575, and permutation laws such as cgr3swap12 28277 and dfcgrg2 28617.

Ideally, we would define this for functions of any set, but we will use words (see df-word 14468) 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
StepHypRef Expression
1 ccgrg 28264 . 2 class cgrG
2 vg . . 3 setvar 𝑔
3 cvv 3468 . . 3 class V
4 va . . . . . . . 8 setvar π‘Ž
54cv 1532 . . . . . . 7 class π‘Ž
62cv 1532 . . . . . . . . 9 class 𝑔
7 cbs 17150 . . . . . . . . 9 class Base
86, 7cfv 6536 . . . . . . . 8 class (Baseβ€˜π‘”)
9 cr 11108 . . . . . . . 8 class ℝ
10 cpm 8820 . . . . . . . 8 class ↑pm
118, 9, 10co 7404 . . . . . . 7 class ((Baseβ€˜π‘”) ↑pm ℝ)
125, 11wcel 2098 . . . . . 6 wff π‘Ž ∈ ((Baseβ€˜π‘”) ↑pm ℝ)
13 vb . . . . . . . 8 setvar 𝑏
1413cv 1532 . . . . . . 7 class 𝑏
1514, 11wcel 2098 . . . . . 6 wff 𝑏 ∈ ((Baseβ€˜π‘”) ↑pm ℝ)
1612, 15wa 395 . . . . 5 wff (π‘Ž ∈ ((Baseβ€˜π‘”) ↑pm ℝ) ∧ 𝑏 ∈ ((Baseβ€˜π‘”) ↑pm ℝ))
175cdm 5669 . . . . . . 7 class dom π‘Ž
1814cdm 5669 . . . . . . 7 class dom 𝑏
1917, 18wceq 1533 . . . . . 6 wff dom π‘Ž = dom 𝑏
20 vi . . . . . . . . . . . 12 setvar 𝑖
2120cv 1532 . . . . . . . . . . 11 class 𝑖
2221, 5cfv 6536 . . . . . . . . . 10 class (π‘Žβ€˜π‘–)
23 vj . . . . . . . . . . . 12 setvar 𝑗
2423cv 1532 . . . . . . . . . . 11 class 𝑗
2524, 5cfv 6536 . . . . . . . . . 10 class (π‘Žβ€˜π‘—)
26 cds 17212 . . . . . . . . . . 11 class dist
276, 26cfv 6536 . . . . . . . . . 10 class (distβ€˜π‘”)
2822, 25, 27co 7404 . . . . . . . . 9 class ((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—))
2921, 14cfv 6536 . . . . . . . . . 10 class (π‘β€˜π‘–)
3024, 14cfv 6536 . . . . . . . . . 10 class (π‘β€˜π‘—)
3129, 30, 27co 7404 . . . . . . . . 9 class ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—))
3228, 31wceq 1533 . . . . . . . 8 wff ((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—))
3332, 23, 17wral 3055 . . . . . . 7 wff βˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—))
3433, 20, 17wral 3055 . . . . . 6 wff βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—))
3519, 34wa 395 . . . . 5 wff (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—)))
3616, 35wa 395 . . . 4 wff ((π‘Ž ∈ ((Baseβ€˜π‘”) ↑pm ℝ) ∧ 𝑏 ∈ ((Baseβ€˜π‘”) ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—))))
3736, 4, 13copab 5203 . . 3 class {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ ((Baseβ€˜π‘”) ↑pm ℝ) ∧ 𝑏 ∈ ((Baseβ€˜π‘”) ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—))))}
382, 3, 37cmpt 5224 . 2 class (𝑔 ∈ V ↦ {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ ((Baseβ€˜π‘”) ↑pm ℝ) ∧ 𝑏 ∈ ((Baseβ€˜π‘”) ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—))))})
391, 38wceq 1533 1 wff cgrG = (𝑔 ∈ V ↦ {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ ((Baseβ€˜π‘”) ↑pm ℝ) ∧ 𝑏 ∈ ((Baseβ€˜π‘”) ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—))))})
Colors of variables: wff setvar class
This definition is referenced by:  iscgrg  28266  ercgrg  28271
  Copyright terms: Public domain W3C validator