Metamath Proof Explorer

Theorem trgcgrg

Description: The property for two triangles to be congruent to each other. (Contributed by Thierry Arnoux, 3-Apr-2019)

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

Proof

Step Hyp Ref Expression
1 trgcgrg.p 
 |-  P = ( Base ` G )
2 trgcgrg.m 
 |-  .- = ( dist ` G )
3 trgcgrg.r 
 |-  .~ = ( cgrG ` G )
4 trgcgrg.g 
 |-  ( ph -> G e. TarskiG )
5 trgcgrg.a 
 |-  ( ph -> A e. P )
6 trgcgrg.b 
 |-  ( ph -> B e. P )
7 trgcgrg.c 
 |-  ( ph -> C e. P )
8 trgcgrg.d 
 |-  ( ph -> D e. P )
9 trgcgrg.e 
 |-  ( ph -> E e. P )
10 trgcgrg.f 
 |-  ( ph -> F e. P )
11 5 6 7 s3cld 
 |-  ( ph -> <" A B C "> e. Word P )
12 wrdf 
 |-  ( <" A B C "> e. Word P -> <" A B C "> : ( 0 ..^ ( # ` <" A B C "> ) ) --> P )
13 11 12 syl 
 |-  ( ph -> <" A B C "> : ( 0 ..^ ( # ` <" A B C "> ) ) --> P )
14 s3len 
 |-  ( # ` <" A B C "> ) = 3
15 14 oveq2i 
 |-  ( 0 ..^ ( # ` <" A B C "> ) ) = ( 0 ..^ 3 )
16 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
17 15 16 eqtri 
 |-  ( 0 ..^ ( # ` <" A B C "> ) ) = { 0 , 1 , 2 }
18 17 feq2i 
 |-  ( <" A B C "> : ( 0 ..^ ( # ` <" A B C "> ) ) --> P <-> <" A B C "> : { 0 , 1 , 2 } --> P )
19 13 18 sylib 
 |-  ( ph -> <" A B C "> : { 0 , 1 , 2 } --> P )
20 19 fdmd 
 |-  ( ph -> dom <" A B C "> = { 0 , 1 , 2 } )
21 20 raleqdv 
 |-  ( ph -> ( A. j e. dom <" A B C "> ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" D E F "> ` i ) .- ( <" D E F "> ` j ) ) <-> A. j e. { 0 , 1 , 2 } ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" D E F "> ` i ) .- ( <" D E F "> ` j ) ) ) )
22 20 21 raleqbidv 
 |-  ( ph -> ( A. i e. dom <" A B C "> A. j e. dom <" A B C "> ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" D E F "> ` i ) .- ( <" D E F "> ` j ) ) <-> A. i e. { 0 , 1 , 2 } A. j e. { 0 , 1 , 2 } ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" D E F "> ` i ) .- ( <" D E F "> ` j ) ) ) )
23 0re 
 |-  0 e. RR
24 1re 
 |-  1 e. RR
25 2re 
 |-  2 e. RR
26 tpssi 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ 2 e. RR ) -> { 0 , 1 , 2 } C_ RR )
27 23 24 25 26 mp3an 
 |-  { 0 , 1 , 2 } C_ RR
28 27 a1i 
 |-  ( ph -> { 0 , 1 , 2 } C_ RR )
29 8 9 10 s3cld 
 |-  ( ph -> <" D E F "> e. Word P )
30 wrdf 
 |-  ( <" D E F "> e. Word P -> <" D E F "> : ( 0 ..^ ( # ` <" D E F "> ) ) --> P )
31 29 30 syl 
 |-  ( ph -> <" D E F "> : ( 0 ..^ ( # ` <" D E F "> ) ) --> P )
32 s3len 
 |-  ( # ` <" D E F "> ) = 3
33 32 oveq2i 
 |-  ( 0 ..^ ( # ` <" D E F "> ) ) = ( 0 ..^ 3 )
34 33 16 eqtri 
 |-  ( 0 ..^ ( # ` <" D E F "> ) ) = { 0 , 1 , 2 }
35 34 feq2i 
 |-  ( <" D E F "> : ( 0 ..^ ( # ` <" D E F "> ) ) --> P <-> <" D E F "> : { 0 , 1 , 2 } --> P )
36 31 35 sylib 
 |-  ( ph -> <" D E F "> : { 0 , 1 , 2 } --> P )
37 1 2 3 4 28 19 36 iscgrgd 
 |-  ( ph -> ( <" A B C "> .~ <" D E F "> <-> A. i e. dom <" A B C "> A. j e. dom <" A B C "> ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" D E F "> ` i ) .- ( <" D E F "> ` j ) ) ) )
38 fveq2 
 |-  ( j = 0 -> ( <" A B C "> ` j ) = ( <" A B C "> ` 0 ) )
39 s3fv0 
 |-  ( A e. P -> ( <" A B C "> ` 0 ) = A )
40 5 39 syl 
 |-  ( ph -> ( <" A B C "> ` 0 ) = A )
41 38 40 sylan9eqr 
 |-  ( ( ph /\ j = 0 ) -> ( <" A B C "> ` j ) = A )
42 41 oveq2d 
 |-  ( ( ph /\ j = 0 ) -> ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" A B C "> ` i ) .- A ) )
43 fveq2 
 |-  ( j = 0 -> ( <" D E F "> ` j ) = ( <" D E F "> ` 0 ) )
44 s3fv0 
 |-  ( D e. P -> ( <" D E F "> ` 0 ) = D )
45 8 44 syl 
 |-  ( ph -> ( <" D E F "> ` 0 ) = D )
46 43 45 sylan9eqr 
 |-  ( ( ph /\ j = 0 ) -> ( <" D E F "> ` j ) = D )
47 46 oveq2d 
 |-  ( ( ph /\ j = 0 ) -> ( ( <" D E F "> ` i ) .- ( <" D E F "> ` j ) ) = ( ( <" D E F "> ` i ) .- D ) )
48 42 47 eqeq12d 
 |-  ( ( ph /\ j = 0 ) -> ( ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" D E F "> ` i ) .- ( <" D E F "> ` j ) ) <-> ( ( <" A B C "> ` i ) .- A ) = ( ( <" D E F "> ` i ) .- D ) ) )
49 fveq2 
 |-  ( j = 1 -> ( <" A B C "> ` j ) = ( <" A B C "> ` 1 ) )
50 s3fv1 
 |-  ( B e. P -> ( <" A B C "> ` 1 ) = B )
51 6 50 syl 
 |-  ( ph -> ( <" A B C "> ` 1 ) = B )
52 49 51 sylan9eqr 
 |-  ( ( ph /\ j = 1 ) -> ( <" A B C "> ` j ) = B )
53 52 oveq2d 
 |-  ( ( ph /\ j = 1 ) -> ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" A B C "> ` i ) .- B ) )
54 fveq2 
 |-  ( j = 1 -> ( <" D E F "> ` j ) = ( <" D E F "> ` 1 ) )
55 s3fv1 
 |-  ( E e. P -> ( <" D E F "> ` 1 ) = E )
56 9 55 syl 
 |-  ( ph -> ( <" D E F "> ` 1 ) = E )
57 54 56 sylan9eqr 
 |-  ( ( ph /\ j = 1 ) -> ( <" D E F "> ` j ) = E )
58 57 oveq2d 
 |-  ( ( ph /\ j = 1 ) -> ( ( <" D E F "> ` i ) .- ( <" D E F "> ` j ) ) = ( ( <" D E F "> ` i ) .- E ) )
59 53 58 eqeq12d 
 |-  ( ( ph /\ j = 1 ) -> ( ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" D E F "> ` i ) .- ( <" D E F "> ` j ) ) <-> ( ( <" A B C "> ` i ) .- B ) = ( ( <" D E F "> ` i ) .- E ) ) )
60 fveq2 
 |-  ( j = 2 -> ( <" A B C "> ` j ) = ( <" A B C "> ` 2 ) )
61 s3fv2 
 |-  ( C e. P -> ( <" A B C "> ` 2 ) = C )
62 7 61 syl 
 |-  ( ph -> ( <" A B C "> ` 2 ) = C )
63 60 62 sylan9eqr 
 |-  ( ( ph /\ j = 2 ) -> ( <" A B C "> ` j ) = C )
64 63 oveq2d 
 |-  ( ( ph /\ j = 2 ) -> ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" A B C "> ` i ) .- C ) )
65 fveq2 
 |-  ( j = 2 -> ( <" D E F "> ` j ) = ( <" D E F "> ` 2 ) )
66 s3fv2 
 |-  ( F e. P -> ( <" D E F "> ` 2 ) = F )
67 10 66 syl 
 |-  ( ph -> ( <" D E F "> ` 2 ) = F )
68 65 67 sylan9eqr 
 |-  ( ( ph /\ j = 2 ) -> ( <" D E F "> ` j ) = F )
69 68 oveq2d 
 |-  ( ( ph /\ j = 2 ) -> ( ( <" D E F "> ` i ) .- ( <" D E F "> ` j ) ) = ( ( <" D E F "> ` i ) .- F ) )
70 64 69 eqeq12d 
 |-  ( ( ph /\ j = 2 ) -> ( ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" D E F "> ` i ) .- ( <" D E F "> ` j ) ) <-> ( ( <" A B C "> ` i ) .- C ) = ( ( <" D E F "> ` i ) .- F ) ) )
71 0red 
 |-  ( ph -> 0 e. RR )
72 1red 
 |-  ( ph -> 1 e. RR )
73 25 a1i 
 |-  ( ph -> 2 e. RR )
74 48 59 70 71 72 73 raltpd 
 |-  ( ph -> ( A. j e. { 0 , 1 , 2 } ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" D E F "> ` i ) .- ( <" D E F "> ` j ) ) <-> ( ( ( <" A B C "> ` i ) .- A ) = ( ( <" D E F "> ` i ) .- D ) /\ ( ( <" A B C "> ` i ) .- B ) = ( ( <" D E F "> ` i ) .- E ) /\ ( ( <" A B C "> ` i ) .- C ) = ( ( <" D E F "> ` i ) .- F ) ) ) )
75 74 adantr 
 |-  ( ( ph /\ i = 0 ) -> ( A. j e. { 0 , 1 , 2 } ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" D E F "> ` i ) .- ( <" D E F "> ` j ) ) <-> ( ( ( <" A B C "> ` i ) .- A ) = ( ( <" D E F "> ` i ) .- D ) /\ ( ( <" A B C "> ` i ) .- B ) = ( ( <" D E F "> ` i ) .- E ) /\ ( ( <" A B C "> ` i ) .- C ) = ( ( <" D E F "> ` i ) .- F ) ) ) )
76 fveq2 
 |-  ( i = 0 -> ( <" A B C "> ` i ) = ( <" A B C "> ` 0 ) )
77 76 adantl 
 |-  ( ( ph /\ i = 0 ) -> ( <" A B C "> ` i ) = ( <" A B C "> ` 0 ) )
78 40 adantr 
 |-  ( ( ph /\ i = 0 ) -> ( <" A B C "> ` 0 ) = A )
79 77 78 eqtr2d 
 |-  ( ( ph /\ i = 0 ) -> A = ( <" A B C "> ` i ) )
80 79 oveq1d 
 |-  ( ( ph /\ i = 0 ) -> ( A .- A ) = ( ( <" A B C "> ` i ) .- A ) )
81 fveq2 
 |-  ( i = 0 -> ( <" D E F "> ` i ) = ( <" D E F "> ` 0 ) )
82 81 adantl 
 |-  ( ( ph /\ i = 0 ) -> ( <" D E F "> ` i ) = ( <" D E F "> ` 0 ) )
83 45 adantr 
 |-  ( ( ph /\ i = 0 ) -> ( <" D E F "> ` 0 ) = D )
84 82 83 eqtr2d 
 |-  ( ( ph /\ i = 0 ) -> D = ( <" D E F "> ` i ) )
85 84 oveq1d 
 |-  ( ( ph /\ i = 0 ) -> ( D .- D ) = ( ( <" D E F "> ` i ) .- D ) )
86 80 85 eqeq12d 
 |-  ( ( ph /\ i = 0 ) -> ( ( A .- A ) = ( D .- D ) <-> ( ( <" A B C "> ` i ) .- A ) = ( ( <" D E F "> ` i ) .- D ) ) )
87 79 oveq1d 
 |-  ( ( ph /\ i = 0 ) -> ( A .- B ) = ( ( <" A B C "> ` i ) .- B ) )
88 84 oveq1d 
 |-  ( ( ph /\ i = 0 ) -> ( D .- E ) = ( ( <" D E F "> ` i ) .- E ) )
89 87 88 eqeq12d 
 |-  ( ( ph /\ i = 0 ) -> ( ( A .- B ) = ( D .- E ) <-> ( ( <" A B C "> ` i ) .- B ) = ( ( <" D E F "> ` i ) .- E ) ) )
90 79 oveq1d 
 |-  ( ( ph /\ i = 0 ) -> ( A .- C ) = ( ( <" A B C "> ` i ) .- C ) )
91 84 oveq1d 
 |-  ( ( ph /\ i = 0 ) -> ( D .- F ) = ( ( <" D E F "> ` i ) .- F ) )
92 90 91 eqeq12d 
 |-  ( ( ph /\ i = 0 ) -> ( ( A .- C ) = ( D .- F ) <-> ( ( <" A B C "> ` i ) .- C ) = ( ( <" D E F "> ` i ) .- F ) ) )
93 86 89 92 3anbi123d 
 |-  ( ( ph /\ i = 0 ) -> ( ( ( A .- A ) = ( D .- D ) /\ ( A .- B ) = ( D .- E ) /\ ( A .- C ) = ( D .- F ) ) <-> ( ( ( <" A B C "> ` i ) .- A ) = ( ( <" D E F "> ` i ) .- D ) /\ ( ( <" A B C "> ` i ) .- B ) = ( ( <" D E F "> ` i ) .- E ) /\ ( ( <" A B C "> ` i ) .- C ) = ( ( <" D E F "> ` i ) .- F ) ) ) )
94 75 93 bitr4d 
 |-  ( ( ph /\ i = 0 ) -> ( A. j e. { 0 , 1 , 2 } ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" D E F "> ` i ) .- ( <" D E F "> ` j ) ) <-> ( ( A .- A ) = ( D .- D ) /\ ( A .- B ) = ( D .- E ) /\ ( A .- C ) = ( D .- F ) ) ) )
95 74 adantr 
 |-  ( ( ph /\ i = 1 ) -> ( A. j e. { 0 , 1 , 2 } ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" D E F "> ` i ) .- ( <" D E F "> ` j ) ) <-> ( ( ( <" A B C "> ` i ) .- A ) = ( ( <" D E F "> ` i ) .- D ) /\ ( ( <" A B C "> ` i ) .- B ) = ( ( <" D E F "> ` i ) .- E ) /\ ( ( <" A B C "> ` i ) .- C ) = ( ( <" D E F "> ` i ) .- F ) ) ) )
96 fveq2 
 |-  ( i = 1 -> ( <" A B C "> ` i ) = ( <" A B C "> ` 1 ) )
97 96 adantl 
 |-  ( ( ph /\ i = 1 ) -> ( <" A B C "> ` i ) = ( <" A B C "> ` 1 ) )
98 51 adantr 
 |-  ( ( ph /\ i = 1 ) -> ( <" A B C "> ` 1 ) = B )
99 97 98 eqtr2d 
 |-  ( ( ph /\ i = 1 ) -> B = ( <" A B C "> ` i ) )
100 99 oveq1d 
 |-  ( ( ph /\ i = 1 ) -> ( B .- A ) = ( ( <" A B C "> ` i ) .- A ) )
101 fveq2 
 |-  ( i = 1 -> ( <" D E F "> ` i ) = ( <" D E F "> ` 1 ) )
102 101 adantl 
 |-  ( ( ph /\ i = 1 ) -> ( <" D E F "> ` i ) = ( <" D E F "> ` 1 ) )
103 56 adantr 
 |-  ( ( ph /\ i = 1 ) -> ( <" D E F "> ` 1 ) = E )
104 102 103 eqtr2d 
 |-  ( ( ph /\ i = 1 ) -> E = ( <" D E F "> ` i ) )
105 104 oveq1d 
 |-  ( ( ph /\ i = 1 ) -> ( E .- D ) = ( ( <" D E F "> ` i ) .- D ) )
106 100 105 eqeq12d 
 |-  ( ( ph /\ i = 1 ) -> ( ( B .- A ) = ( E .- D ) <-> ( ( <" A B C "> ` i ) .- A ) = ( ( <" D E F "> ` i ) .- D ) ) )
107 99 oveq1d 
 |-  ( ( ph /\ i = 1 ) -> ( B .- B ) = ( ( <" A B C "> ` i ) .- B ) )
108 104 oveq1d 
 |-  ( ( ph /\ i = 1 ) -> ( E .- E ) = ( ( <" D E F "> ` i ) .- E ) )
109 107 108 eqeq12d 
 |-  ( ( ph /\ i = 1 ) -> ( ( B .- B ) = ( E .- E ) <-> ( ( <" A B C "> ` i ) .- B ) = ( ( <" D E F "> ` i ) .- E ) ) )
110 99 oveq1d 
 |-  ( ( ph /\ i = 1 ) -> ( B .- C ) = ( ( <" A B C "> ` i ) .- C ) )
111 104 oveq1d 
 |-  ( ( ph /\ i = 1 ) -> ( E .- F ) = ( ( <" D E F "> ` i ) .- F ) )
112 110 111 eqeq12d 
 |-  ( ( ph /\ i = 1 ) -> ( ( B .- C ) = ( E .- F ) <-> ( ( <" A B C "> ` i ) .- C ) = ( ( <" D E F "> ` i ) .- F ) ) )
113 106 109 112 3anbi123d 
 |-  ( ( ph /\ i = 1 ) -> ( ( ( B .- A ) = ( E .- D ) /\ ( B .- B ) = ( E .- E ) /\ ( B .- C ) = ( E .- F ) ) <-> ( ( ( <" A B C "> ` i ) .- A ) = ( ( <" D E F "> ` i ) .- D ) /\ ( ( <" A B C "> ` i ) .- B ) = ( ( <" D E F "> ` i ) .- E ) /\ ( ( <" A B C "> ` i ) .- C ) = ( ( <" D E F "> ` i ) .- F ) ) ) )
114 95 113 bitr4d 
 |-  ( ( ph /\ i = 1 ) -> ( A. j e. { 0 , 1 , 2 } ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" D E F "> ` i ) .- ( <" D E F "> ` j ) ) <-> ( ( B .- A ) = ( E .- D ) /\ ( B .- B ) = ( E .- E ) /\ ( B .- C ) = ( E .- F ) ) ) )
115 74 adantr 
 |-  ( ( ph /\ i = 2 ) -> ( A. j e. { 0 , 1 , 2 } ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" D E F "> ` i ) .- ( <" D E F "> ` j ) ) <-> ( ( ( <" A B C "> ` i ) .- A ) = ( ( <" D E F "> ` i ) .- D ) /\ ( ( <" A B C "> ` i ) .- B ) = ( ( <" D E F "> ` i ) .- E ) /\ ( ( <" A B C "> ` i ) .- C ) = ( ( <" D E F "> ` i ) .- F ) ) ) )
116 fveq2 
 |-  ( i = 2 -> ( <" A B C "> ` i ) = ( <" A B C "> ` 2 ) )
117 116 adantl 
 |-  ( ( ph /\ i = 2 ) -> ( <" A B C "> ` i ) = ( <" A B C "> ` 2 ) )
118 62 adantr 
 |-  ( ( ph /\ i = 2 ) -> ( <" A B C "> ` 2 ) = C )
119 117 118 eqtr2d 
 |-  ( ( ph /\ i = 2 ) -> C = ( <" A B C "> ` i ) )
120 119 oveq1d 
 |-  ( ( ph /\ i = 2 ) -> ( C .- A ) = ( ( <" A B C "> ` i ) .- A ) )
121 fveq2 
 |-  ( i = 2 -> ( <" D E F "> ` i ) = ( <" D E F "> ` 2 ) )
122 121 adantl 
 |-  ( ( ph /\ i = 2 ) -> ( <" D E F "> ` i ) = ( <" D E F "> ` 2 ) )
123 67 adantr 
 |-  ( ( ph /\ i = 2 ) -> ( <" D E F "> ` 2 ) = F )
124 122 123 eqtr2d 
 |-  ( ( ph /\ i = 2 ) -> F = ( <" D E F "> ` i ) )
125 124 oveq1d 
 |-  ( ( ph /\ i = 2 ) -> ( F .- D ) = ( ( <" D E F "> ` i ) .- D ) )
126 120 125 eqeq12d 
 |-  ( ( ph /\ i = 2 ) -> ( ( C .- A ) = ( F .- D ) <-> ( ( <" A B C "> ` i ) .- A ) = ( ( <" D E F "> ` i ) .- D ) ) )
127 119 oveq1d 
 |-  ( ( ph /\ i = 2 ) -> ( C .- B ) = ( ( <" A B C "> ` i ) .- B ) )
128 124 oveq1d 
 |-  ( ( ph /\ i = 2 ) -> ( F .- E ) = ( ( <" D E F "> ` i ) .- E ) )
129 127 128 eqeq12d 
 |-  ( ( ph /\ i = 2 ) -> ( ( C .- B ) = ( F .- E ) <-> ( ( <" A B C "> ` i ) .- B ) = ( ( <" D E F "> ` i ) .- E ) ) )
130 119 oveq1d 
 |-  ( ( ph /\ i = 2 ) -> ( C .- C ) = ( ( <" A B C "> ` i ) .- C ) )
131 124 oveq1d 
 |-  ( ( ph /\ i = 2 ) -> ( F .- F ) = ( ( <" D E F "> ` i ) .- F ) )
132 130 131 eqeq12d 
 |-  ( ( ph /\ i = 2 ) -> ( ( C .- C ) = ( F .- F ) <-> ( ( <" A B C "> ` i ) .- C ) = ( ( <" D E F "> ` i ) .- F ) ) )
133 126 129 132 3anbi123d 
 |-  ( ( ph /\ i = 2 ) -> ( ( ( C .- A ) = ( F .- D ) /\ ( C .- B ) = ( F .- E ) /\ ( C .- C ) = ( F .- F ) ) <-> ( ( ( <" A B C "> ` i ) .- A ) = ( ( <" D E F "> ` i ) .- D ) /\ ( ( <" A B C "> ` i ) .- B ) = ( ( <" D E F "> ` i ) .- E ) /\ ( ( <" A B C "> ` i ) .- C ) = ( ( <" D E F "> ` i ) .- F ) ) ) )
134 115 133 bitr4d 
 |-  ( ( ph /\ i = 2 ) -> ( A. j e. { 0 , 1 , 2 } ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" D E F "> ` i ) .- ( <" D E F "> ` j ) ) <-> ( ( C .- A ) = ( F .- D ) /\ ( C .- B ) = ( F .- E ) /\ ( C .- C ) = ( F .- F ) ) ) )
135 94 114 134 71 72 73 raltpd 
 |-  ( ph -> ( A. i e. { 0 , 1 , 2 } A. j e. { 0 , 1 , 2 } ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" D E F "> ` i ) .- ( <" D E F "> ` j ) ) <-> ( ( ( A .- A ) = ( D .- D ) /\ ( A .- B ) = ( D .- E ) /\ ( A .- C ) = ( D .- F ) ) /\ ( ( B .- A ) = ( E .- D ) /\ ( B .- B ) = ( E .- E ) /\ ( B .- C ) = ( E .- F ) ) /\ ( ( C .- A ) = ( F .- D ) /\ ( C .- B ) = ( F .- E ) /\ ( C .- C ) = ( F .- F ) ) ) ) )
136 an33rean 
 |-  ( ( ( ( A .- A ) = ( D .- D ) /\ ( A .- B ) = ( D .- E ) /\ ( A .- C ) = ( D .- F ) ) /\ ( ( B .- A ) = ( E .- D ) /\ ( B .- B ) = ( E .- E ) /\ ( B .- C ) = ( E .- F ) ) /\ ( ( C .- A ) = ( F .- D ) /\ ( C .- B ) = ( F .- E ) /\ ( C .- C ) = ( F .- F ) ) ) <-> ( ( ( A .- A ) = ( D .- D ) /\ ( B .- B ) = ( E .- E ) /\ ( C .- C ) = ( F .- F ) ) /\ ( ( ( A .- B ) = ( D .- E ) /\ ( B .- A ) = ( E .- D ) ) /\ ( ( B .- C ) = ( E .- F ) /\ ( C .- B ) = ( F .- E ) ) /\ ( ( A .- C ) = ( D .- F ) /\ ( C .- A ) = ( F .- D ) ) ) ) )
137 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
138 1 2 137 4 5 8 tgcgrtriv 
 |-  ( ph -> ( A .- A ) = ( D .- D ) )
139 1 2 137 4 6 9 tgcgrtriv 
 |-  ( ph -> ( B .- B ) = ( E .- E ) )
140 1 2 137 4 7 10 tgcgrtriv 
 |-  ( ph -> ( C .- C ) = ( F .- F ) )
141 138 139 140 3jca 
 |-  ( ph -> ( ( A .- A ) = ( D .- D ) /\ ( B .- B ) = ( E .- E ) /\ ( C .- C ) = ( F .- F ) ) )
142 141 biantrurd 
 |-  ( ph -> ( ( ( ( A .- B ) = ( D .- E ) /\ ( B .- A ) = ( E .- D ) ) /\ ( ( B .- C ) = ( E .- F ) /\ ( C .- B ) = ( F .- E ) ) /\ ( ( A .- C ) = ( D .- F ) /\ ( C .- A ) = ( F .- D ) ) ) <-> ( ( ( A .- A ) = ( D .- D ) /\ ( B .- B ) = ( E .- E ) /\ ( C .- C ) = ( F .- F ) ) /\ ( ( ( A .- B ) = ( D .- E ) /\ ( B .- A ) = ( E .- D ) ) /\ ( ( B .- C ) = ( E .- F ) /\ ( C .- B ) = ( F .- E ) ) /\ ( ( A .- C ) = ( D .- F ) /\ ( C .- A ) = ( F .- D ) ) ) ) ) )
143 simprl 
 |-  ( ( ph /\ ( ( A .- B ) = ( D .- E ) /\ ( B .- A ) = ( E .- D ) ) ) -> ( A .- B ) = ( D .- E ) )
144 simpr 
 |-  ( ( ph /\ ( A .- B ) = ( D .- E ) ) -> ( A .- B ) = ( D .- E ) )
145 4 adantr 
 |-  ( ( ph /\ ( A .- B ) = ( D .- E ) ) -> G e. TarskiG )
146 5 adantr 
 |-  ( ( ph /\ ( A .- B ) = ( D .- E ) ) -> A e. P )
147 6 adantr 
 |-  ( ( ph /\ ( A .- B ) = ( D .- E ) ) -> B e. P )
148 8 adantr 
 |-  ( ( ph /\ ( A .- B ) = ( D .- E ) ) -> D e. P )
149 9 adantr 
 |-  ( ( ph /\ ( A .- B ) = ( D .- E ) ) -> E e. P )
150 1 2 137 145 146 147 148 149 144 tgcgrcomlr 
 |-  ( ( ph /\ ( A .- B ) = ( D .- E ) ) -> ( B .- A ) = ( E .- D ) )
151 144 150 jca 
 |-  ( ( ph /\ ( A .- B ) = ( D .- E ) ) -> ( ( A .- B ) = ( D .- E ) /\ ( B .- A ) = ( E .- D ) ) )
152 143 151 impbida 
 |-  ( ph -> ( ( ( A .- B ) = ( D .- E ) /\ ( B .- A ) = ( E .- D ) ) <-> ( A .- B ) = ( D .- E ) ) )
153 simprl 
 |-  ( ( ph /\ ( ( B .- C ) = ( E .- F ) /\ ( C .- B ) = ( F .- E ) ) ) -> ( B .- C ) = ( E .- F ) )
154 simpr 
 |-  ( ( ph /\ ( B .- C ) = ( E .- F ) ) -> ( B .- C ) = ( E .- F ) )
155 4 adantr 
 |-  ( ( ph /\ ( B .- C ) = ( E .- F ) ) -> G e. TarskiG )
156 6 adantr 
 |-  ( ( ph /\ ( B .- C ) = ( E .- F ) ) -> B e. P )
157 7 adantr 
 |-  ( ( ph /\ ( B .- C ) = ( E .- F ) ) -> C e. P )
158 9 adantr 
 |-  ( ( ph /\ ( B .- C ) = ( E .- F ) ) -> E e. P )
159 10 adantr 
 |-  ( ( ph /\ ( B .- C ) = ( E .- F ) ) -> F e. P )
160 1 2 137 155 156 157 158 159 154 tgcgrcomlr 
 |-  ( ( ph /\ ( B .- C ) = ( E .- F ) ) -> ( C .- B ) = ( F .- E ) )
161 154 160 jca 
 |-  ( ( ph /\ ( B .- C ) = ( E .- F ) ) -> ( ( B .- C ) = ( E .- F ) /\ ( C .- B ) = ( F .- E ) ) )
162 153 161 impbida 
 |-  ( ph -> ( ( ( B .- C ) = ( E .- F ) /\ ( C .- B ) = ( F .- E ) ) <-> ( B .- C ) = ( E .- F ) ) )
163 simprr 
 |-  ( ( ph /\ ( ( A .- C ) = ( D .- F ) /\ ( C .- A ) = ( F .- D ) ) ) -> ( C .- A ) = ( F .- D ) )
164 4 adantr 
 |-  ( ( ph /\ ( C .- A ) = ( F .- D ) ) -> G e. TarskiG )
165 7 adantr 
 |-  ( ( ph /\ ( C .- A ) = ( F .- D ) ) -> C e. P )
166 5 adantr 
 |-  ( ( ph /\ ( C .- A ) = ( F .- D ) ) -> A e. P )
167 10 adantr 
 |-  ( ( ph /\ ( C .- A ) = ( F .- D ) ) -> F e. P )
168 8 adantr 
 |-  ( ( ph /\ ( C .- A ) = ( F .- D ) ) -> D e. P )
169 simpr 
 |-  ( ( ph /\ ( C .- A ) = ( F .- D ) ) -> ( C .- A ) = ( F .- D ) )
170 1 2 137 164 165 166 167 168 169 tgcgrcomlr 
 |-  ( ( ph /\ ( C .- A ) = ( F .- D ) ) -> ( A .- C ) = ( D .- F ) )
171 170 169 jca 
 |-  ( ( ph /\ ( C .- A ) = ( F .- D ) ) -> ( ( A .- C ) = ( D .- F ) /\ ( C .- A ) = ( F .- D ) ) )
172 163 171 impbida 
 |-  ( ph -> ( ( ( A .- C ) = ( D .- F ) /\ ( C .- A ) = ( F .- D ) ) <-> ( C .- A ) = ( F .- D ) ) )
173 152 162 172 3anbi123d 
 |-  ( ph -> ( ( ( ( A .- B ) = ( D .- E ) /\ ( B .- A ) = ( E .- D ) ) /\ ( ( B .- C ) = ( E .- F ) /\ ( C .- B ) = ( F .- E ) ) /\ ( ( A .- C ) = ( D .- F ) /\ ( C .- A ) = ( F .- D ) ) ) <-> ( ( A .- B ) = ( D .- E ) /\ ( B .- C ) = ( E .- F ) /\ ( C .- A ) = ( F .- D ) ) ) )
174 142 173 bitr3d 
 |-  ( ph -> ( ( ( ( A .- A ) = ( D .- D ) /\ ( B .- B ) = ( E .- E ) /\ ( C .- C ) = ( F .- F ) ) /\ ( ( ( A .- B ) = ( D .- E ) /\ ( B .- A ) = ( E .- D ) ) /\ ( ( B .- C ) = ( E .- F ) /\ ( C .- B ) = ( F .- E ) ) /\ ( ( A .- C ) = ( D .- F ) /\ ( C .- A ) = ( F .- D ) ) ) ) <-> ( ( A .- B ) = ( D .- E ) /\ ( B .- C ) = ( E .- F ) /\ ( C .- A ) = ( F .- D ) ) ) )
175 136 174 syl5bb 
 |-  ( ph -> ( ( ( ( A .- A ) = ( D .- D ) /\ ( A .- B ) = ( D .- E ) /\ ( A .- C ) = ( D .- F ) ) /\ ( ( B .- A ) = ( E .- D ) /\ ( B .- B ) = ( E .- E ) /\ ( B .- C ) = ( E .- F ) ) /\ ( ( C .- A ) = ( F .- D ) /\ ( C .- B ) = ( F .- E ) /\ ( C .- C ) = ( F .- F ) ) ) <-> ( ( A .- B ) = ( D .- E ) /\ ( B .- C ) = ( E .- F ) /\ ( C .- A ) = ( F .- D ) ) ) )
176 135 175 bitr2d 
 |-  ( ph -> ( ( ( A .- B ) = ( D .- E ) /\ ( B .- C ) = ( E .- F ) /\ ( C .- A ) = ( F .- D ) ) <-> A. i e. { 0 , 1 , 2 } A. j e. { 0 , 1 , 2 } ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" D E F "> ` i ) .- ( <" D E F "> ` j ) ) ) )
177 22 37 176 3bitr4d 
 |-  ( ph -> ( <" A B C "> .~ <" D E F "> <-> ( ( A .- B ) = ( D .- E ) /\ ( B .- C ) = ( E .- F ) /\ ( C .- A ) = ( F .- D ) ) ) )