Metamath Proof Explorer


Theorem tgsss1

Description: Third congruence theorem: SSS (Side-Side-Side): If the three pairs of sides of two triangles are equal in length, then the triangles are congruent. Theorem 11.51 of Schwabhauser p. 109. (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 ( 𝜑𝐹𝑃 )
tgsss.1 ( 𝜑 → ( 𝐴 𝐵 ) = ( 𝐷 𝐸 ) )
tgsss.2 ( 𝜑 → ( 𝐵 𝐶 ) = ( 𝐸 𝐹 ) )
tgsss.3 ( 𝜑 → ( 𝐶 𝐴 ) = ( 𝐹 𝐷 ) )
tgsss.4 ( 𝜑𝐴𝐵 )
tgsss.5 ( 𝜑𝐵𝐶 )
tgsss.6 ( 𝜑𝐶𝐴 )
Assertion tgsss1 ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )

Proof

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 tgsss.1 ( 𝜑 → ( 𝐴 𝐵 ) = ( 𝐷 𝐸 ) )
12 tgsss.2 ( 𝜑 → ( 𝐵 𝐶 ) = ( 𝐸 𝐹 ) )
13 tgsss.3 ( 𝜑 → ( 𝐶 𝐴 ) = ( 𝐹 𝐷 ) )
14 tgsss.4 ( 𝜑𝐴𝐵 )
15 tgsss.5 ( 𝜑𝐵𝐶 )
16 tgsss.6 ( 𝜑𝐶𝐴 )
17 eqid ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
18 eqid ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
19 1 2 18 4 5 6 7 8 9 10 11 12 13 trgcgr ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
20 1 3 4 17 5 6 7 8 9 10 14 15 19 cgrcgra ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )