Metamath Proof Explorer


Theorem tgsas1

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 third sides are equal in length. Theorem 11.49 of Schwabhauser p. 107. (Contributed by Thierry Arnoux, 1-Aug-2020)

Ref Expression
Hypotheses tgsas.p P = Base G
tgsas.m - ˙ = dist G
tgsas.i I = Itv G
tgsas.g φ G 𝒢 Tarski
tgsas.a φ A P
tgsas.b φ B P
tgsas.c φ C P
tgsas.d φ D P
tgsas.e φ E P
tgsas.f φ F P
tgsas.1 φ A - ˙ B = D - ˙ E
tgsas.2 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩
tgsas.3 φ B - ˙ C = E - ˙ F
Assertion tgsas1 φ C - ˙ A = F - ˙ D

Proof

Step Hyp Ref Expression
1 tgsas.p P = Base G
2 tgsas.m - ˙ = dist G
3 tgsas.i I = Itv G
4 tgsas.g φ G 𝒢 Tarski
5 tgsas.a φ A P
6 tgsas.b φ B P
7 tgsas.c φ C P
8 tgsas.d φ D P
9 tgsas.e φ E P
10 tgsas.f φ F P
11 tgsas.1 φ A - ˙ B = D - ˙ E
12 tgsas.2 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩
13 tgsas.3 φ B - ˙ C = E - ˙ F
14 eqid hl 𝒢 G = hl 𝒢 G
15 1 3 14 4 5 6 7 8 9 10 12 cgrane1 φ A B
16 1 3 14 5 5 6 4 15 hlid φ A hl 𝒢 G B A
17 1 3 14 4 5 6 7 8 9 10 12 cgrane2 φ B C
18 17 necomd φ C B
19 1 3 14 7 5 6 4 18 hlid φ C hl 𝒢 G B C
20 1 2 3 4 5 6 8 9 11 tgcgrcomlr φ B - ˙ A = E - ˙ D
21 1 3 14 4 5 6 7 8 9 10 12 5 2 7 16 19 20 13 cgracgr φ A - ˙ C = D - ˙ F
22 1 2 3 4 5 7 8 10 21 tgcgrcomlr φ C - ˙ A = F - ˙ D