Description: First congruence theorem: SAS (Side-Angle-Side): If two pairs of sides of two triangles are equal in length, and the included angles are equal in measurement, then the triangles are congruent. Theorem 11.49 of Schwabhauser p. 107. (Contributed by Thierry Arnoux, 1-Aug-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | tgsas.p | ⊢ 𝑃 = ( Base ‘ 𝐺 ) | |
| tgsas.m | ⊢ − = ( dist ‘ 𝐺 ) | ||
| tgsas.i | ⊢ 𝐼 = ( Itv ‘ 𝐺 ) | ||
| tgsas.g | ⊢ ( 𝜑 → 𝐺 ∈ TarskiG ) | ||
| tgsas.a | ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 ) | ||
| tgsas.b | ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 ) | ||
| tgsas.c | ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 ) | ||
| tgsas.d | ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 ) | ||
| tgsas.e | ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 ) | ||
| tgsas.f | ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 ) | ||
| tgsas.1 | ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) ) | ||
| tgsas.2 | ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) | ||
| tgsas.3 | ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) ) | ||
| Assertion | tgsas | ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | tgsas.p | ⊢ 𝑃 = ( Base ‘ 𝐺 ) | |
| 2 | tgsas.m | ⊢ − = ( dist ‘ 𝐺 ) | |
| 3 | tgsas.i | ⊢ 𝐼 = ( Itv ‘ 𝐺 ) | |
| 4 | tgsas.g | ⊢ ( 𝜑 → 𝐺 ∈ TarskiG ) | |
| 5 | tgsas.a | ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 ) | |
| 6 | tgsas.b | ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 ) | |
| 7 | tgsas.c | ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 ) | |
| 8 | tgsas.d | ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 ) | |
| 9 | tgsas.e | ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 ) | |
| 10 | tgsas.f | ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 ) | |
| 11 | tgsas.1 | ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) ) | |
| 12 | tgsas.2 | ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) | |
| 13 | tgsas.3 | ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) ) | |
| 14 | eqid | ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 ) | |
| 15 | 1 2 3 4 5 6 7 8 9 10 11 12 13 | tgsas1 | ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐹 − 𝐷 ) ) |
| 16 | 1 2 14 4 5 6 7 8 9 10 11 13 15 | trgcgr | ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) |