Metamath Proof Explorer

Definition df-cgrg

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 and expanded in iscgra . This does not mean our system is weaker; dfcgrg2 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 , cgr3simp2 , cgr3simp3 , cgrcgra , and permutation laws such as cgr3swap12 and dfcgrg2 .

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

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

Ref Expression
Assertion df-cgrg ⊢ ∼ 𝒢 = g ∈ V ⟼ a b | a ∈ Base g ↑ 𝑝𝑚 ℝ ∧ b ∈ Base g ↑ 𝑝𝑚 ℝ ∧ dom ⁡ a = dom ⁡ b ∧ ∀ i ∈ dom ⁡ a ∀ j ∈ dom ⁡ a a ⁡ i dist ⁡ g a ⁡ j = b ⁡ i dist ⁡ g b ⁡ j

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccgrg class ∼ 𝒢
1 vg setvar g
2 cvv class V
3 va setvar a
4 vb setvar b
5 3 cv setvar a
6 cbs class Base
7 1 cv setvar g
8 7 6 cfv class Base g
9 cpm class ↑ 𝑝𝑚
10 cr class ℝ
11 8 10 9 co class Base g ↑ 𝑝𝑚 ℝ
12 5 11 wcel wff a ∈ Base g ↑ 𝑝𝑚 ℝ
13 4 cv setvar b
14 13 11 wcel wff b ∈ Base g ↑ 𝑝𝑚 ℝ
15 12 14 wa wff a ∈ Base g ↑ 𝑝𝑚 ℝ ∧ b ∈ Base g ↑ 𝑝𝑚 ℝ
16 5 cdm class dom ⁡ a
17 13 cdm class dom ⁡ b
18 16 17 wceq wff dom ⁡ a = dom ⁡ b
19 vi setvar i
20 vj setvar j
21 19 cv setvar i
22 21 5 cfv class a ⁡ i
23 cds class dist
24 7 23 cfv class dist ⁡ g
25 20 cv setvar j
26 25 5 cfv class a ⁡ j
27 22 26 24 co class a ⁡ i dist ⁡ g a ⁡ j
28 21 13 cfv class b ⁡ i
29 25 13 cfv class b ⁡ j
30 28 29 24 co class b ⁡ i dist ⁡ g b ⁡ j
31 27 30 wceq wff a ⁡ i dist ⁡ g a ⁡ j = b ⁡ i dist ⁡ g b ⁡ j
32 31 20 16 wral wff ∀ j ∈ dom ⁡ a a ⁡ i dist ⁡ g a ⁡ j = b ⁡ i dist ⁡ g b ⁡ j
33 32 19 16 wral wff ∀ i ∈ dom ⁡ a ∀ j ∈ dom ⁡ a a ⁡ i dist ⁡ g a ⁡ j = b ⁡ i dist ⁡ g b ⁡ j
34 18 33 wa wff dom ⁡ a = dom ⁡ b ∧ ∀ i ∈ dom ⁡ a ∀ j ∈ dom ⁡ a a ⁡ i dist ⁡ g a ⁡ j = b ⁡ i dist ⁡ g b ⁡ j
35 15 34 wa wff a ∈ Base g ↑ 𝑝𝑚 ℝ ∧ b ∈ Base g ↑ 𝑝𝑚 ℝ ∧ dom ⁡ a = dom ⁡ b ∧ ∀ i ∈ dom ⁡ a ∀ j ∈ dom ⁡ a a ⁡ i dist ⁡ g a ⁡ j = b ⁡ i dist ⁡ g b ⁡ j
36 35 3 4 copab class a b | a ∈ Base g ↑ 𝑝𝑚 ℝ ∧ b ∈ Base g ↑ 𝑝𝑚 ℝ ∧ dom ⁡ a = dom ⁡ b ∧ ∀ i ∈ dom ⁡ a ∀ j ∈ dom ⁡ a a ⁡ i dist ⁡ g a ⁡ j = b ⁡ i dist ⁡ g b ⁡ j
37 1 2 36 cmpt class g ∈ V ⟼ a b | a ∈ Base g ↑ 𝑝𝑚 ℝ ∧ b ∈ Base g ↑ 𝑝𝑚 ℝ ∧ dom ⁡ a = dom ⁡ b ∧ ∀ i ∈ dom ⁡ a ∀ j ∈ dom ⁡ a a ⁡ i dist ⁡ g a ⁡ j = b ⁡ i dist ⁡ g b ⁡ j
38 0 37 wceq wff ∼ 𝒢 = g ∈ V ⟼ a b | a ∈ Base g ↑ 𝑝𝑚 ℝ ∧ b ∈ Base g ↑ 𝑝𝑚 ℝ ∧ dom ⁡ a = dom ⁡ b ∧ ∀ i ∈ dom ⁡ a ∀ j ∈ dom ⁡ a a ⁡ i dist ⁡ g a ⁡ j = b ⁡ i dist ⁡ g b ⁡ j