Metamath Proof Explorer

Theorem tgcgr4

Description: Two quadrilaterals to be congruent to each other if one triangle formed by their vertices is, and the additional points are equidistant too. (Contributed by Thierry Arnoux, 8-Oct-2020)

Ref Expression
Hypotheses tgcgrxfr.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgcgrxfr.m ⊢ − = ( dist ‘ 𝐺 )
tgcgrxfr.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgcgrxfr.r ⊢ ∼ = ( cgrG ‘ 𝐺 )
tgcgrxfr.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgcgr4.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
tgcgr4.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
tgcgr4.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
tgcgr4.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
tgcgr4.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
tgcgr4.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
tgcgr4.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
tgcgr4.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
Assertion tgcgr4 ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ∼ ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝑊 𝑋 𝑌 ”⟩ ∧ ( ( 𝐴 − 𝐷 ) = ( 𝑊 − 𝑍 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑋 − 𝑍 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑌 − 𝑍 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 tgcgrxfr.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgcgrxfr.m ⊢ − = ( dist ‘ 𝐺 )
3 tgcgrxfr.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tgcgrxfr.r ⊢ ∼ = ( cgrG ‘ 𝐺 )
5 tgcgrxfr.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 tgcgr4.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 tgcgr4.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 tgcgr4.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9 tgcgr4.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
10 tgcgr4.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
11 tgcgr4.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
12 tgcgr4.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
13 tgcgr4.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
14 fzo0ssnn0 ⊢ ( 0 ..^ 4 ) ⊆ ℕ0
15 nn0ssre ⊢ ℕ0 ⊆ ℝ
16 14 15 sstri ⊢ ( 0 ..^ 4 ) ⊆ ℝ
17 16 a1i ⊢ ( 𝜑 → ( 0 ..^ 4 ) ⊆ ℝ )
18 6 7 8 9 s4cld ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ∈ Word 𝑃 )
19 wrdf ⊢ ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ∈ Word 𝑃 → ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) ) ⟶ 𝑃 )
20 18 19 syl ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) ) ⟶ 𝑃 )
21 s4len ⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) = 4
22 21 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) ) = ( 0 ..^ 4 )
23 22 feq2i ⊢ ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) ) ⟶ 𝑃 ↔ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ : ( 0 ..^ 4 ) ⟶ 𝑃 )
24 20 23 sylib ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ : ( 0 ..^ 4 ) ⟶ 𝑃 )
25 10 11 12 13 s4cld ⊢ ( 𝜑 → ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ∈ Word 𝑃 )
26 wrdf ⊢ ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ∈ Word 𝑃 → ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ) ) ⟶ 𝑃 )
27 25 26 syl ⊢ ( 𝜑 → ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ) ) ⟶ 𝑃 )
28 s4len ⊢ ( ♯ ‘ ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ) = 4
29 28 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ) ) = ( 0 ..^ 4 )
30 29 feq2i ⊢ ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ) ) ⟶ 𝑃 ↔ ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ : ( 0 ..^ 4 ) ⟶ 𝑃 )
31 27 30 sylib ⊢ ( 𝜑 → ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ : ( 0 ..^ 4 ) ⟶ 𝑃 )
32 1 2 4 5 17 24 31 iscgrglt ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ∼ ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ↔ ∀ 𝑖 ∈ dom ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ∀ 𝑗 ∈ dom ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ) )
33 24 fdmd ⊢ ( 𝜑 → dom ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ = ( 0 ..^ 4 ) )
34 3p1e4 ⊢ ( 3 + 1 ) = 4
35 34 oveq2i ⊢ ( 0 ..^ ( 3 + 1 ) ) = ( 0 ..^ 4 )
36 3nn0 ⊢ 3 ∈ ℕ0
37 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
38 36 37 eleqtri ⊢ 3 ∈ ( ℤ≥ ‘ 0 )
39 fzosplitsn ⊢ ( 3 ∈ ( ℤ≥ ‘ 0 ) → ( 0 ..^ ( 3 + 1 ) ) = ( ( 0 ..^ 3 ) ∪ { 3 } ) )
40 38 39 ax-mp ⊢ ( 0 ..^ ( 3 + 1 ) ) = ( ( 0 ..^ 3 ) ∪ { 3 } )
41 35 40 eqtr3i ⊢ ( 0 ..^ 4 ) = ( ( 0 ..^ 3 ) ∪ { 3 } )
42 33 41 eqtrdi ⊢ ( 𝜑 → dom ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ = ( ( 0 ..^ 3 ) ∪ { 3 } ) )
43 42 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑗 ∈ dom ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ↔ ∀ 𝑗 ∈ ( ( 0 ..^ 3 ) ∪ { 3 } ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ) )
44 breq2 ⊢ ( 𝑗 = 3 → ( 𝑖 < 𝑗 ↔ 𝑖 < 3 ) )
45 fveq2 ⊢ ( 𝑗 = 3 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) )
46 45 oveq2d ⊢ ( 𝑗 = 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) )
47 fveq2 ⊢ ( 𝑗 = 3 → ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) = ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) )
48 47 oveq2d ⊢ ( 𝑗 = 3 → ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) )
49 46 48 eqeq12d ⊢ ( 𝑗 = 3 → ( ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ↔ ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) )
50 44 49 imbi12d ⊢ ( 𝑗 = 3 → ( ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ↔ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) )
51 50 ralunsn ⊢ ( 3 ∈ ℕ0 → ( ∀ 𝑗 ∈ ( ( 0 ..^ 3 ) ∪ { 3 } ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ↔ ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) ) )
52 36 51 ax-mp ⊢ ( ∀ 𝑗 ∈ ( ( 0 ..^ 3 ) ∪ { 3 } ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ↔ ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) )
53 43 52 bitrdi ⊢ ( 𝜑 → ( ∀ 𝑗 ∈ dom ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ↔ ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) ) )
54 53 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ dom ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ∀ 𝑗 ∈ dom ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ↔ ∀ 𝑖 ∈ dom ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) ) )
55 42 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ dom ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) ↔ ∀ 𝑖 ∈ ( ( 0 ..^ 3 ) ∪ { 3 } ) ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) ) )
56 fzo0ssnn0 ⊢ ( 0 ..^ 3 ) ⊆ ℕ0
57 56 15 sstri ⊢ ( 0 ..^ 3 ) ⊆ ℝ
58 simpr ⊢ ( ( 𝑖 = 3 ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) → 𝑗 ∈ ( 0 ..^ 3 ) )
59 57 58 sseldi ⊢ ( ( 𝑖 = 3 ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) → 𝑗 ∈ ℝ )
60 simpl ⊢ ( ( 𝑖 = 3 ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) → 𝑖 = 3 )
61 3re ⊢ 3 ∈ ℝ
62 60 61 eqeltrdi ⊢ ( ( 𝑖 = 3 ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) → 𝑖 ∈ ℝ )
63 elfzolt2 ⊢ ( 𝑗 ∈ ( 0 ..^ 3 ) → 𝑗 < 3 )
64 63 adantl ⊢ ( ( 𝑖 = 3 ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) → 𝑗 < 3 )
65 64 60 breqtrrd ⊢ ( ( 𝑖 = 3 ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) → 𝑗 < 𝑖 )
66 59 62 65 ltnsymd ⊢ ( ( 𝑖 = 3 ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) → ¬ 𝑖 < 𝑗 )
67 66 pm2.21d ⊢ ( ( 𝑖 = 3 ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) → ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) )
68 tbtru ⊢ ( ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ↔ ( ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ↔ ⊤ ) )
69 67 68 sylib ⊢ ( ( 𝑖 = 3 ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) → ( ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ↔ ⊤ ) )
70 69 ralbidva ⊢ ( 𝑖 = 3 → ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ↔ ∀ 𝑗 ∈ ( 0 ..^ 3 ) ⊤ ) )
71 3nn ⊢ 3 ∈ ℕ
72 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 3 ) ↔ 3 ∈ ℕ )
73 71 72 mpbir ⊢ 0 ∈ ( 0 ..^ 3 )
74 73 ne0ii ⊢ ( 0 ..^ 3 ) ≠ ∅
75 r19.3rzv ⊢ ( ( 0 ..^ 3 ) ≠ ∅ → ( ⊤ ↔ ∀ 𝑗 ∈ ( 0 ..^ 3 ) ⊤ ) )
76 74 75 ax-mp ⊢ ( ⊤ ↔ ∀ 𝑗 ∈ ( 0 ..^ 3 ) ⊤ )
77 70 76 bitr4di ⊢ ( 𝑖 = 3 → ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ↔ ⊤ ) )
78 breq1 ⊢ ( 𝑖 = 3 → ( 𝑖 < 3 ↔ 3 < 3 ) )
79 61 ltnri ⊢ ¬ 3 < 3
80 79 bifal ⊢ ( 3 < 3 ↔ ⊥ )
81 78 80 bitrdi ⊢ ( 𝑖 = 3 → ( 𝑖 < 3 ↔ ⊥ ) )
82 81 imbi1d ⊢ ( 𝑖 = 3 → ( ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ↔ ( ⊥ → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) )
83 falim ⊢ ( ⊥ → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) )
84 83 bitru ⊢ ( ( ⊥ → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ↔ ⊤ )
85 82 84 bitrdi ⊢ ( 𝑖 = 3 → ( ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ↔ ⊤ ) )
86 77 85 anbi12d ⊢ ( 𝑖 = 3 → ( ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) ↔ ( ⊤ ∧ ⊤ ) ) )
87 anidm ⊢ ( ( ⊤ ∧ ⊤ ) ↔ ⊤ )
88 86 87 bitrdi ⊢ ( 𝑖 = 3 → ( ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) ↔ ⊤ ) )
89 88 ralunsn ⊢ ( 3 ∈ ℕ0 → ( ∀ 𝑖 ∈ ( ( 0 ..^ 3 ) ∪ { 3 } ) ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ 3 ) ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) ∧ ⊤ ) ) )
90 36 89 ax-mp ⊢ ( ∀ 𝑖 ∈ ( ( 0 ..^ 3 ) ∪ { 3 } ) ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ 3 ) ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) ∧ ⊤ ) )
91 ancom ⊢ ( ( ∀ 𝑖 ∈ ( 0 ..^ 3 ) ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) ∧ ⊤ ) ↔ ( ⊤ ∧ ∀ 𝑖 ∈ ( 0 ..^ 3 ) ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) ) )
92 truan ⊢ ( ( ⊤ ∧ ∀ 𝑖 ∈ ( 0 ..^ 3 ) ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 3 ) ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) )
93 90 91 92 3bitri ⊢ ( ∀ 𝑖 ∈ ( ( 0 ..^ 3 ) ∪ { 3 } ) ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 3 ) ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) )
94 55 93 bitrdi ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ dom ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 3 ) ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) ) )
95 54 94 bitrd ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ dom ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ∀ 𝑗 ∈ dom ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 3 ) ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) ) )
96 r19.26 ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ 3 ) ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ 3 ) ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 3 ) ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) )
97 6 7 8 s3cld ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 )
98 wrdf ⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ) ⟶ 𝑃 )
99 97 98 syl ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ) ⟶ 𝑃 )
100 s3len ⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3
101 100 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ) = ( 0 ..^ 3 )
102 101 feq2i ⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ) ⟶ 𝑃 ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ..^ 3 ) ⟶ 𝑃 )
103 99 102 sylib ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ..^ 3 ) ⟶ 𝑃 )
104 103 fdmd ⊢ ( 𝜑 → dom ⟨“ 𝐴 𝐵 𝐶 ”⟩ = ( 0 ..^ 3 ) )
105 104 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑗 ∈ dom ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑗 ) ) ) ↔ ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑗 ) ) ) ) )
106 104 105 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ dom ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∀ 𝑗 ∈ dom ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑗 ) ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 3 ) ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑗 ) ) ) ) )
107 57 a1i ⊢ ( 𝜑 → ( 0 ..^ 3 ) ⊆ ℝ )
108 10 11 12 s3cld ⊢ ( 𝜑 → ⟨“ 𝑊 𝑋 𝑌 ”⟩ ∈ Word 𝑃 )
109 wrdf ⊢ ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ∈ Word 𝑃 → ⟨“ 𝑊 𝑋 𝑌 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝑊 𝑋 𝑌 ”⟩ ) ) ⟶ 𝑃 )
110 108 109 syl ⊢ ( 𝜑 → ⟨“ 𝑊 𝑋 𝑌 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝑊 𝑋 𝑌 ”⟩ ) ) ⟶ 𝑃 )
111 s3len ⊢ ( ♯ ‘ ⟨“ 𝑊 𝑋 𝑌 ”⟩ ) = 3
112 111 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑊 𝑋 𝑌 ”⟩ ) ) = ( 0 ..^ 3 )
113 112 feq2i ⊢ ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝑊 𝑋 𝑌 ”⟩ ) ) ⟶ 𝑃 ↔ ⟨“ 𝑊 𝑋 𝑌 ”⟩ : ( 0 ..^ 3 ) ⟶ 𝑃 )
114 110 113 sylib ⊢ ( 𝜑 → ⟨“ 𝑊 𝑋 𝑌 ”⟩ : ( 0 ..^ 3 ) ⟶ 𝑃 )
115 1 2 4 5 107 103 114 iscgrglt ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝑊 𝑋 𝑌 ”⟩ ↔ ∀ 𝑖 ∈ dom ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∀ 𝑗 ∈ dom ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑗 ) ) ) ) )
116 df-s4 ⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ )
117 116 fveq1i ⊢ ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) = ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ ) ‘ 𝑖 )
118 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → 𝐴 ∈ 𝑃 )
119 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → 𝐵 ∈ 𝑃 )
120 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → 𝐶 ∈ 𝑃 )
121 118 119 120 s3cld ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 )
122 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → 𝐷 ∈ 𝑃 )
123 122 s1cld ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → ⟨“ 𝐷 ”⟩ ∈ Word 𝑃 )
124 simprl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → 𝑖 ∈ ( 0 ..^ 3 ) )
125 124 101 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ) )
126 ccatval1 ⊢ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 ∧ ⟨“ 𝐷 ”⟩ ∈ Word 𝑃 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ) ) → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ ) ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) )
127 121 123 125 126 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ ) ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) )
128 117 127 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) )
129 116 fveq1i ⊢ ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) = ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ ) ‘ 𝑗 )
130 simprr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → 𝑗 ∈ ( 0 ..^ 3 ) )
131 130 101 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ) )
132 ccatval1 ⊢ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 ∧ ⟨“ 𝐷 ”⟩ ∈ Word 𝑃 ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ) ) → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ ) ‘ 𝑗 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑗 ) )
133 121 123 131 132 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ ) ‘ 𝑗 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑗 ) )
134 129 133 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑗 ) )
135 128 134 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑗 ) ) )
136 df-s4 ⊢ ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ = ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ++ ⟨“ 𝑍 ”⟩ )
137 136 fveq1i ⊢ ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) = ( ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 )
138 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → 𝑊 ∈ 𝑃 )
139 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → 𝑋 ∈ 𝑃 )
140 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → 𝑌 ∈ 𝑃 )
141 138 139 140 s3cld ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → ⟨“ 𝑊 𝑋 𝑌 ”⟩ ∈ Word 𝑃 )
142 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → 𝑍 ∈ 𝑃 )
143 142 s1cld ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → ⟨“ 𝑍 ”⟩ ∈ Word 𝑃 )
144 124 112 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑊 𝑋 𝑌 ”⟩ ) ) )
145 ccatval1 ⊢ ( ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ∈ Word 𝑃 ∧ ⟨“ 𝑍 ”⟩ ∈ Word 𝑃 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑊 𝑋 𝑌 ”⟩ ) ) ) → ( ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) = ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑖 ) )
146 141 143 144 145 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → ( ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) = ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑖 ) )
147 137 146 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑖 ) )
148 136 fveq1i ⊢ ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) = ( ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑗 )
149 130 112 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑊 𝑋 𝑌 ”⟩ ) ) )
150 ccatval1 ⊢ ( ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ∈ Word 𝑃 ∧ ⟨“ 𝑍 ”⟩ ∈ Word 𝑃 ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑊 𝑋 𝑌 ”⟩ ) ) ) → ( ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑗 ) = ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑗 ) )
151 141 143 149 150 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → ( ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑗 ) = ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑗 ) )
152 148 151 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) = ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑗 ) )
153 147 152 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑗 ) ) )
154 135 153 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → ( ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ↔ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑗 ) ) ) )
155 154 imbi2d ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 3 ) ∧ 𝑗 ∈ ( 0 ..^ 3 ) ) ) → ( ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ↔ ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑗 ) ) ) ) )
156 155 2ralbidva ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ( 0 ..^ 3 ) ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 3 ) ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 ”⟩ ‘ 𝑗 ) ) ) ) )
157 106 115 156 3bitr4rd ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ( 0 ..^ 3 ) ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝑊 𝑋 𝑌 ”⟩ ) )
158 fzo0to3tp ⊢ ( 0 ..^ 3 ) = { 0 , 1 , 2 }
159 158 raleqi ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ 3 ) ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ↔ ∀ 𝑖 ∈ { 0 , 1 , 2 } ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) )
160 3pos ⊢ 0 < 3
161 breq1 ⊢ ( 𝑖 = 0 → ( 𝑖 < 3 ↔ 0 < 3 ) )
162 160 161 mpbiri ⊢ ( 𝑖 = 0 → 𝑖 < 3 )
163 162 adantl ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → 𝑖 < 3 )
164 biimt ⊢ ( 𝑖 < 3 → ( ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ↔ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) )
165 163 164 syl ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ↔ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) )
166 fveq2 ⊢ ( 𝑖 = 0 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 0 ) )
167 s4fv0 ⊢ ( 𝐴 ∈ 𝑃 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 0 ) = 𝐴 )
168 6 167 syl ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 0 ) = 𝐴 )
169 166 168 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) = 𝐴 )
170 s4fv3 ⊢ ( 𝐷 ∈ 𝑃 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) = 𝐷 )
171 9 170 syl ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) = 𝐷 )
172 171 adantr ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) = 𝐷 )
173 169 172 oveq12d ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( 𝐴 − 𝐷 ) )
174 fveq2 ⊢ ( 𝑖 = 0 → ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 0 ) )
175 s4fv0 ⊢ ( 𝑊 ∈ 𝑃 → ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 0 ) = 𝑊 )
176 10 175 syl ⊢ ( 𝜑 → ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 0 ) = 𝑊 )
177 174 176 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) = 𝑊 )
178 s4fv3 ⊢ ( 𝑍 ∈ 𝑃 → ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) = 𝑍 )
179 13 178 syl ⊢ ( 𝜑 → ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) = 𝑍 )
180 179 adantr ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) = 𝑍 )
181 177 180 oveq12d ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) = ( 𝑊 − 𝑍 ) )
182 173 181 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ↔ ( 𝐴 − 𝐷 ) = ( 𝑊 − 𝑍 ) ) )
183 165 182 bitr3d ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ↔ ( 𝐴 − 𝐷 ) = ( 𝑊 − 𝑍 ) ) )
184 1lt3 ⊢ 1 < 3
185 breq1 ⊢ ( 𝑖 = 1 → ( 𝑖 < 3 ↔ 1 < 3 ) )
186 184 185 mpbiri ⊢ ( 𝑖 = 1 → 𝑖 < 3 )
187 186 adantl ⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → 𝑖 < 3 )
188 187 164 syl ⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → ( ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ↔ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) )
189 fveq2 ⊢ ( 𝑖 = 1 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 1 ) )
190 s4fv1 ⊢ ( 𝐵 ∈ 𝑃 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 1 ) = 𝐵 )
191 7 190 syl ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 1 ) = 𝐵 )
192 189 191 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) = 𝐵 )
193 171 adantr ⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) = 𝐷 )
194 192 193 oveq12d ⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( 𝐵 − 𝐷 ) )
195 fveq2 ⊢ ( 𝑖 = 1 → ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 1 ) )
196 s4fv1 ⊢ ( 𝑋 ∈ 𝑃 → ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 1 ) = 𝑋 )
197 11 196 syl ⊢ ( 𝜑 → ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 1 ) = 𝑋 )
198 195 197 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) = 𝑋 )
199 179 adantr ⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) = 𝑍 )
200 198 199 oveq12d ⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) = ( 𝑋 − 𝑍 ) )
201 194 200 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → ( ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ↔ ( 𝐵 − 𝐷 ) = ( 𝑋 − 𝑍 ) ) )
202 188 201 bitr3d ⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → ( ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ↔ ( 𝐵 − 𝐷 ) = ( 𝑋 − 𝑍 ) ) )
203 2lt3 ⊢ 2 < 3
204 breq1 ⊢ ( 𝑖 = 2 → ( 𝑖 < 3 ↔ 2 < 3 ) )
205 203 204 mpbiri ⊢ ( 𝑖 = 2 → 𝑖 < 3 )
206 205 adantl ⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → 𝑖 < 3 )
207 206 164 syl ⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → ( ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ↔ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) )
208 fveq2 ⊢ ( 𝑖 = 2 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 2 ) )
209 s4fv2 ⊢ ( 𝐶 ∈ 𝑃 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 2 ) = 𝐶 )
210 8 209 syl ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 2 ) = 𝐶 )
211 208 210 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) = 𝐶 )
212 171 adantr ⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) = 𝐷 )
213 211 212 oveq12d ⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( 𝐶 − 𝐷 ) )
214 fveq2 ⊢ ( 𝑖 = 2 → ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 2 ) )
215 s4fv2 ⊢ ( 𝑌 ∈ 𝑃 → ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 2 ) = 𝑌 )
216 12 215 syl ⊢ ( 𝜑 → ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 2 ) = 𝑌 )
217 214 216 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) = 𝑌 )
218 179 adantr ⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) = 𝑍 )
219 217 218 oveq12d ⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) = ( 𝑌 − 𝑍 ) )
220 213 219 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → ( ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ↔ ( 𝐶 − 𝐷 ) = ( 𝑌 − 𝑍 ) ) )
221 207 220 bitr3d ⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → ( ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ↔ ( 𝐶 − 𝐷 ) = ( 𝑌 − 𝑍 ) ) )
222 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
223 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
224 2re ⊢ 2 ∈ ℝ
225 224 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
226 183 202 221 222 223 225 raltpd ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ { 0 , 1 , 2 } ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ↔ ( ( 𝐴 − 𝐷 ) = ( 𝑊 − 𝑍 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑋 − 𝑍 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑌 − 𝑍 ) ) ) )
227 159 226 syl5bb ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ( 0 ..^ 3 ) ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ↔ ( ( 𝐴 − 𝐷 ) = ( 𝑊 − 𝑍 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑋 − 𝑍 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑌 − 𝑍 ) ) ) )
228 157 227 anbi12d ⊢ ( 𝜑 → ( ( ∀ 𝑖 ∈ ( 0 ..^ 3 ) ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 3 ) ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝑊 𝑋 𝑌 ”⟩ ∧ ( ( 𝐴 − 𝐷 ) = ( 𝑊 − 𝑍 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑋 − 𝑍 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑌 − 𝑍 ) ) ) ) )
229 96 228 syl5bb ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ( 0 ..^ 3 ) ( ∀ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑖 < 𝑗 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑗 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑗 ) ) ) ∧ ( 𝑖 < 3 → ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) ) = ( ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 𝑖 ) − ( ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ‘ 3 ) ) ) ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝑊 𝑋 𝑌 ”⟩ ∧ ( ( 𝐴 − 𝐷 ) = ( 𝑊 − 𝑍 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑋 − 𝑍 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑌 − 𝑍 ) ) ) ) )
230 32 95 229 3bitrd ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ∼ ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝑊 𝑋 𝑌 ”⟩ ∧ ( ( 𝐴 − 𝐷 ) = ( 𝑊 − 𝑍 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑋 − 𝑍 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑌 − 𝑍 ) ) ) ) )