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 26308
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 26605 and expanded in iscgra 26606. This does not mean our system is weaker; dfcgrg2 26660 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 26317, cgr3simp2 26318, cgr3simp3 26319, cgrcgra 26618, and permutation laws such as cgr3swap12 26320 and dfcgrg2 26660.

Ideally, we would define this for functions of any set, but we will use words (see df-word 13867) 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 26307 . 2 class cgrG
2 vg . . 3 setvar 𝑔
3 cvv 3480 . . 3 class V
4 va . . . . . . . 8 setvar 𝑎
54cv 1537 . . . . . . 7 class 𝑎
62cv 1537 . . . . . . . . 9 class 𝑔
7 cbs 16483 . . . . . . . . 9 class Base
86, 7cfv 6343 . . . . . . . 8 class (Base‘𝑔)
9 cr 10534 . . . . . . . 8 class
10 cpm 8403 . . . . . . . 8 class pm
118, 9, 10co 7149 . . . . . . 7 class ((Base‘𝑔) ↑pm ℝ)
125, 11wcel 2115 . . . . . 6 wff 𝑎 ∈ ((Base‘𝑔) ↑pm ℝ)
13 vb . . . . . . . 8 setvar 𝑏
1413cv 1537 . . . . . . 7 class 𝑏
1514, 11wcel 2115 . . . . . 6 wff 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)
1612, 15wa 399 . . . . 5 wff (𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ))
175cdm 5542 . . . . . . 7 class dom 𝑎
1814cdm 5542 . . . . . . 7 class dom 𝑏
1917, 18wceq 1538 . . . . . 6 wff dom 𝑎 = dom 𝑏
20 vi . . . . . . . . . . . 12 setvar 𝑖
2120cv 1537 . . . . . . . . . . 11 class 𝑖
2221, 5cfv 6343 . . . . . . . . . 10 class (𝑎𝑖)
23 vj . . . . . . . . . . . 12 setvar 𝑗
2423cv 1537 . . . . . . . . . . 11 class 𝑗
2524, 5cfv 6343 . . . . . . . . . 10 class (𝑎𝑗)
26 cds 16574 . . . . . . . . . . 11 class dist
276, 26cfv 6343 . . . . . . . . . 10 class (dist‘𝑔)
2822, 25, 27co 7149 . . . . . . . . 9 class ((𝑎𝑖)(dist‘𝑔)(𝑎𝑗))
2921, 14cfv 6343 . . . . . . . . . 10 class (𝑏𝑖)
3024, 14cfv 6343 . . . . . . . . . 10 class (𝑏𝑗)
3129, 30, 27co 7149 . . . . . . . . 9 class ((𝑏𝑖)(dist‘𝑔)(𝑏𝑗))
3228, 31wceq 1538 . . . . . . . 8 wff ((𝑎𝑖)(dist‘𝑔)(𝑎𝑗)) = ((𝑏𝑖)(dist‘𝑔)(𝑏𝑗))
3332, 23, 17wral 3133 . . . . . . 7 wff 𝑗 ∈ dom 𝑎((𝑎𝑖)(dist‘𝑔)(𝑎𝑗)) = ((𝑏𝑖)(dist‘𝑔)(𝑏𝑗))
3433, 20, 17wral 3133 . . . . . 6 wff 𝑖 ∈ dom 𝑎𝑗 ∈ dom 𝑎((𝑎𝑖)(dist‘𝑔)(𝑎𝑗)) = ((𝑏𝑖)(dist‘𝑔)(𝑏𝑗))
3519, 34wa 399 . . . . 5 wff (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎𝑗 ∈ dom 𝑎((𝑎𝑖)(dist‘𝑔)(𝑎𝑗)) = ((𝑏𝑖)(dist‘𝑔)(𝑏𝑗)))
3616, 35wa 399 . . . 4 wff ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎𝑗 ∈ dom 𝑎((𝑎𝑖)(dist‘𝑔)(𝑎𝑗)) = ((𝑏𝑖)(dist‘𝑔)(𝑏𝑗))))
3736, 4, 13copab 5114 . . 3 class {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎𝑗 ∈ dom 𝑎((𝑎𝑖)(dist‘𝑔)(𝑎𝑗)) = ((𝑏𝑖)(dist‘𝑔)(𝑏𝑗))))}
382, 3, 37cmpt 5132 . 2 class (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎𝑗 ∈ dom 𝑎((𝑎𝑖)(dist‘𝑔)(𝑎𝑗)) = ((𝑏𝑖)(dist‘𝑔)(𝑏𝑗))))})
391, 38wceq 1538 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  26309  ercgrg  26314
  Copyright terms: Public domain W3C validator