Metamath Proof Explorer

Theorem dfcgrg2

Description: Congruence for two triangles can also be defined as congruence of sides and angles (6 parts). This is often the actual textbook definition of triangle congruence, see for example https://en.wikipedia.org/wiki/Congruence_(geometry)#Congruence_of_triangles . With this definition, the "SSS" congruence theorem has an additional part, namely, that triangle congruence implies congruence of the sides (which means equality of the lengths). Because our development of elementary geometry strives to closely follow Schwabhaeuser's, our original definition of shape congruence, df-cgrg , already covers that part: see trgcgr . This theorem is also named "CPCTC", which stands for "Corresponding Parts of Congruent Triangles are Congruent", see https://en.wikipedia.org/wiki/Congruence_(geometry)#CPCTC . (Contributed by Thierry Arnoux, 18-Jan-2023)

Ref Expression
Hypotheses dfcgrg2.p 
|- P = ( Base ` G )
dfcgrg2.m 
|- .- = ( dist ` G )
dfcgrg2.g 
|- ( ph -> G e. TarskiG )
dfcgrg2.a 
|- ( ph -> A e. P )
dfcgrg2.b 
|- ( ph -> B e. P )
dfcgrg2.c 
|- ( ph -> C e. P )
dfcgrg2.d 
|- ( ph -> D e. P )
dfcgrg2.e 
|- ( ph -> E e. P )
dfcgrg2.f 
|- ( ph -> F e. P )
dfcgrg2.1 
|- ( ph -> A =/= B )
dfcgrg2.2 
|- ( ph -> B =/= C )
dfcgrg2.3 
|- ( ph -> C =/= A )
Assertion dfcgrg2 
|- ( ph -> ( <" A B C "> ( cgrG ` G ) <" D E F "> <-> ( ( ( A .- B ) = ( D .- E ) /\ ( B .- C ) = ( E .- F ) /\ ( C .- A ) = ( F .- D ) ) /\ ( <" A B C "> ( cgrA ` G ) <" D E F "> /\ <" C A B "> ( cgrA ` G ) <" F D E "> /\ <" B C A "> ( cgrA ` G ) <" E F D "> ) ) ) )

Proof

Step Hyp Ref Expression
1 dfcgrg2.p 
 |-  P = ( Base ` G )
2 dfcgrg2.m 
 |-  .- = ( dist ` G )
3 dfcgrg2.g 
 |-  ( ph -> G e. TarskiG )
4 dfcgrg2.a 
 |-  ( ph -> A e. P )
5 dfcgrg2.b 
 |-  ( ph -> B e. P )
6 dfcgrg2.c 
 |-  ( ph -> C e. P )
7 dfcgrg2.d 
 |-  ( ph -> D e. P )
8 dfcgrg2.e 
 |-  ( ph -> E e. P )
9 dfcgrg2.f 
 |-  ( ph -> F e. P )
10 dfcgrg2.1 
 |-  ( ph -> A =/= B )
11 dfcgrg2.2 
 |-  ( ph -> B =/= C )
12 dfcgrg2.3 
 |-  ( ph -> C =/= A )
13 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
14 3 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrG ` G ) <" D E F "> ) -> G e. TarskiG )
15 4 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrG ` G ) <" D E F "> ) -> A e. P )
16 5 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrG ` G ) <" D E F "> ) -> B e. P )
17 6 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrG ` G ) <" D E F "> ) -> C e. P )
18 7 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrG ` G ) <" D E F "> ) -> D e. P )
19 8 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrG ` G ) <" D E F "> ) -> E e. P )
20 9 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrG ` G ) <" D E F "> ) -> F e. P )
21 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
22 1 2 21 3 4 5 6 7 8 9 trgcgrg 
 |-  ( ph -> ( <" A B C "> ( cgrG ` G ) <" D E F "> <-> ( ( A .- B ) = ( D .- E ) /\ ( B .- C ) = ( E .- F ) /\ ( C .- A ) = ( F .- D ) ) ) )
23 22 biimpa 
 |-  ( ( ph /\ <" A B C "> ( cgrG ` G ) <" D E F "> ) -> ( ( A .- B ) = ( D .- E ) /\ ( B .- C ) = ( E .- F ) /\ ( C .- A ) = ( F .- D ) ) )
24 23 simp1d 
 |-  ( ( ph /\ <" A B C "> ( cgrG ` G ) <" D E F "> ) -> ( A .- B ) = ( D .- E ) )
25 23 simp2d 
 |-  ( ( ph /\ <" A B C "> ( cgrG ` G ) <" D E F "> ) -> ( B .- C ) = ( E .- F ) )
26 23 simp3d 
 |-  ( ( ph /\ <" A B C "> ( cgrG ` G ) <" D E F "> ) -> ( C .- A ) = ( F .- D ) )
27 10 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrG ` G ) <" D E F "> ) -> A =/= B )
28 11 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrG ` G ) <" D E F "> ) -> B =/= C )
29 12 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrG ` G ) <" D E F "> ) -> C =/= A )
30 1 2 13 14 15 16 17 18 19 20 24 25 26 27 28 29 tgsss1 
 |-  ( ( ph /\ <" A B C "> ( cgrG ` G ) <" D E F "> ) -> <" A B C "> ( cgrA ` G ) <" D E F "> )
31 1 2 13 14 17 15 16 20 18 19 26 24 25 29 27 28 tgsss1 
 |-  ( ( ph /\ <" A B C "> ( cgrG ` G ) <" D E F "> ) -> <" C A B "> ( cgrA ` G ) <" F D E "> )
32 1 2 13 14 16 17 15 19 20 18 25 26 24 28 29 27 tgsss1 
 |-  ( ( ph /\ <" A B C "> ( cgrG ` G ) <" D E F "> ) -> <" B C A "> ( cgrA ` G ) <" E F D "> )
33 30 31 32 3jca 
 |-  ( ( ph /\ <" A B C "> ( cgrG ` G ) <" D E F "> ) -> ( <" A B C "> ( cgrA ` G ) <" D E F "> /\ <" C A B "> ( cgrA ` G ) <" F D E "> /\ <" B C A "> ( cgrA ` G ) <" E F D "> ) )
34 33 ex 
 |-  ( ph -> ( <" A B C "> ( cgrG ` G ) <" D E F "> -> ( <" A B C "> ( cgrA ` G ) <" D E F "> /\ <" C A B "> ( cgrA ` G ) <" F D E "> /\ <" B C A "> ( cgrA ` G ) <" E F D "> ) ) )
35 34 pm4.71d 
 |-  ( ph -> ( <" A B C "> ( cgrG ` G ) <" D E F "> <-> ( <" A B C "> ( cgrG ` G ) <" D E F "> /\ ( <" A B C "> ( cgrA ` G ) <" D E F "> /\ <" C A B "> ( cgrA ` G ) <" F D E "> /\ <" B C A "> ( cgrA ` G ) <" E F D "> ) ) ) )
36 22 anbi1d 
 |-  ( ph -> ( ( <" A B C "> ( cgrG ` G ) <" D E F "> /\ ( <" A B C "> ( cgrA ` G ) <" D E F "> /\ <" C A B "> ( cgrA ` G ) <" F D E "> /\ <" B C A "> ( cgrA ` G ) <" E F D "> ) ) <-> ( ( ( A .- B ) = ( D .- E ) /\ ( B .- C ) = ( E .- F ) /\ ( C .- A ) = ( F .- D ) ) /\ ( <" A B C "> ( cgrA ` G ) <" D E F "> /\ <" C A B "> ( cgrA ` G ) <" F D E "> /\ <" B C A "> ( cgrA ` G ) <" E F D "> ) ) ) )
37 35 36 bitrd 
 |-  ( ph -> ( <" A B C "> ( cgrG ` G ) <" D E F "> <-> ( ( ( A .- B ) = ( D .- E ) /\ ( B .- C ) = ( E .- F ) /\ ( C .- A ) = ( F .- D ) ) /\ ( <" A B C "> ( cgrA ` G ) <" D E F "> /\ <" C A B "> ( cgrA ` G ) <" F D E "> /\ <" B C A "> ( cgrA ` G ) <" E F D "> ) ) ) )