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 | ⊢ cgrG = ( 𝑔 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) ) ) } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | ccgrg | ⊢ cgrG | |
| 1 | vg | ⊢ 𝑔 | |
| 2 | cvv | ⊢ V | |
| 3 | va | ⊢ 𝑎 | |
| 4 | vb | ⊢ 𝑏 | |
| 5 | 3 | cv | ⊢ 𝑎 |
| 6 | cbs | ⊢ Base | |
| 7 | 1 | cv | ⊢ 𝑔 |
| 8 | 7 6 | cfv | ⊢ ( Base ‘ 𝑔 ) |
| 9 | cpm | ⊢ ↑pm | |
| 10 | cr | ⊢ ℝ | |
| 11 | 8 10 9 | co | ⊢ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) |
| 12 | 5 11 | wcel | ⊢ 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) |
| 13 | 4 | cv | ⊢ 𝑏 |
| 14 | 13 11 | wcel | ⊢ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) |
| 15 | 12 14 | wa | ⊢ ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ) |
| 16 | 5 | cdm | ⊢ dom 𝑎 |
| 17 | 13 | cdm | ⊢ dom 𝑏 |
| 18 | 16 17 | wceq | ⊢ dom 𝑎 = dom 𝑏 |
| 19 | vi | ⊢ 𝑖 | |
| 20 | vj | ⊢ 𝑗 | |
| 21 | 19 | cv | ⊢ 𝑖 |
| 22 | 21 5 | cfv | ⊢ ( 𝑎 ‘ 𝑖 ) |
| 23 | cds | ⊢ dist | |
| 24 | 7 23 | cfv | ⊢ ( dist ‘ 𝑔 ) |
| 25 | 20 | cv | ⊢ 𝑗 |
| 26 | 25 5 | cfv | ⊢ ( 𝑎 ‘ 𝑗 ) |
| 27 | 22 26 24 | co | ⊢ ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) |
| 28 | 21 13 | cfv | ⊢ ( 𝑏 ‘ 𝑖 ) |
| 29 | 25 13 | cfv | ⊢ ( 𝑏 ‘ 𝑗 ) |
| 30 | 28 29 24 | co | ⊢ ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) |
| 31 | 27 30 | wceq | ⊢ ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) |
| 32 | 31 20 16 | wral | ⊢ ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) |
| 33 | 32 19 16 | wral | ⊢ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) |
| 34 | 18 33 | wa | ⊢ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) ) |
| 35 | 15 34 | wa | ⊢ ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) ) ) |
| 36 | 35 3 4 | copab | ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) ) ) } |
| 37 | 1 2 36 | cmpt | ⊢ ( 𝑔 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) ) ) } ) |
| 38 | 0 37 | wceq | ⊢ cgrG = ( 𝑔 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) ) ) } ) |