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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
trgcgrg.m ⊢ − = ( dist ‘ 𝐺 )
trgcgrg.r ⊢ ∼ = ( cgrG ‘ 𝐺 )
trgcgrg.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
trgcgrg.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
trgcgrg.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
trgcgrg.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
trgcgrg.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
trgcgrg.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
trgcgrg.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
Assertion trgcgrg ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) ∧ ( 𝐶 − 𝐴 ) = ( 𝐹 − 𝐷 ) ) ) )

Proof

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