Description: Second congruence theorem: ASA. (Angle-Side-Angle): If two pairs of angles of two triangles are equal in measurement, and the included sides are equal in length, then the triangles are congruent. Theorem 11.50 of Schwabhauser p. 108. (Contributed by Thierry Arnoux, 15-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 | ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 ) | ||
| tgasa.l | ⊢ 𝐿 = ( LineG ‘ 𝐺 ) | ||
| tgasa.1 | ⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) | ||
| tgasa.2 | ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) ) | ||
| tgasa.3 | ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) | ||
| tgasa.4 | ⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐹 𝐷 𝐸 ”⟩ ) | ||
| Assertion | tgasa | ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( 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 | tgasa.l | ⊢ 𝐿 = ( LineG ‘ 𝐺 ) | |
| 12 | tgasa.1 | ⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) | |
| 13 | tgasa.2 | ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) ) | |
| 14 | tgasa.3 | ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) | |
| 15 | tgasa.4 | ⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐹 𝐷 𝐸 ”⟩ ) | |
| 16 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 | tgasa1 | ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) ) |
| 17 | 1 2 3 4 5 6 7 8 9 10 13 14 16 | tgsas | ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) |