Metamath Proof Explorer


Theorem 2swrd2eqwrdeq

Description: Two words of length at least two are equal if and only if they have the same prefix and the same two single symbols suffix. (Contributed by AV, 24-Sep-2018) (Revised by AV, 12-Oct-2022)

Ref Expression
Assertion 2swrd2eqwrdeq ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) → ( 𝑊 = 𝑈 ↔ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∧ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∧ ( lastS ‘ 𝑊 ) = ( lastS ‘ 𝑈 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lencl ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
2 1z 1 ∈ ℤ
3 nn0z ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
4 zltp1le ( ( 1 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℤ ) → ( 1 < ( ♯ ‘ 𝑊 ) ↔ ( 1 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ) )
5 2 3 4 sylancr ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( 1 < ( ♯ ‘ 𝑊 ) ↔ ( 1 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ) )
6 1p1e2 ( 1 + 1 ) = 2
7 6 a1i ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( 1 + 1 ) = 2 )
8 7 breq1d ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( 1 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ↔ 2 ≤ ( ♯ ‘ 𝑊 ) ) )
9 8 biimpd ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( 1 + 1 ) ≤ ( ♯ ‘ 𝑊 ) → 2 ≤ ( ♯ ‘ 𝑊 ) ) )
10 5 9 sylbid ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( 1 < ( ♯ ‘ 𝑊 ) → 2 ≤ ( ♯ ‘ 𝑊 ) ) )
11 10 imp ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 1 < ( ♯ ‘ 𝑊 ) ) → 2 ≤ ( ♯ ‘ 𝑊 ) )
12 2nn0 2 ∈ ℕ0
13 simpl ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 1 < ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
14 nn0sub ( ( 2 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) → ( 2 ≤ ( ♯ ‘ 𝑊 ) ↔ ( ( ♯ ‘ 𝑊 ) − 2 ) ∈ ℕ0 ) )
15 12 13 14 sylancr ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 1 < ( ♯ ‘ 𝑊 ) ) → ( 2 ≤ ( ♯ ‘ 𝑊 ) ↔ ( ( ♯ ‘ 𝑊 ) − 2 ) ∈ ℕ0 ) )
16 11 15 mpbid ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 1 < ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 2 ) ∈ ℕ0 )
17 3 adantr ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 1 < ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℤ )
18 0red ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → 0 ∈ ℝ )
19 1red ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → 1 ∈ ℝ )
20 nn0re ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ 𝑊 ) ∈ ℝ )
21 18 19 20 3jca ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) )
22 0lt1 0 < 1
23 lttr ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) → ( ( 0 < 1 ∧ 1 < ( ♯ ‘ 𝑊 ) ) → 0 < ( ♯ ‘ 𝑊 ) ) )
24 23 expd ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) → ( 0 < 1 → ( 1 < ( ♯ ‘ 𝑊 ) → 0 < ( ♯ ‘ 𝑊 ) ) ) )
25 21 22 24 mpisyl ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( 1 < ( ♯ ‘ 𝑊 ) → 0 < ( ♯ ‘ 𝑊 ) ) )
26 25 imp ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 1 < ( ♯ ‘ 𝑊 ) ) → 0 < ( ♯ ‘ 𝑊 ) )
27 elnnz ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ 0 < ( ♯ ‘ 𝑊 ) ) )
28 17 26 27 sylanbrc ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 1 < ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
29 2rp 2 ∈ ℝ+
30 29 a1i ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → 2 ∈ ℝ+ )
31 20 30 ltsubrpd ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) − 2 ) < ( ♯ ‘ 𝑊 ) )
32 31 adantr ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 1 < ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 2 ) < ( ♯ ‘ 𝑊 ) )
33 elfzo0 ( ( ( ♯ ‘ 𝑊 ) − 2 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( ( ( ♯ ‘ 𝑊 ) − 2 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( ( ♯ ‘ 𝑊 ) − 2 ) < ( ♯ ‘ 𝑊 ) ) )
34 16 28 32 33 syl3anbrc ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 1 < ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 2 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
35 1 34 sylan ( ( 𝑊 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 2 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
36 35 3adant2 ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 2 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
37 pfxsuffeqwrdeq ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) − 2 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 = 𝑈 ↔ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∧ ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) ) )
38 36 37 syld3an3 ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) → ( 𝑊 = 𝑈 ↔ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∧ ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) ) )
39 swrd2lsw ( ( 𝑊 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) → ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ⟨“ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ( lastS ‘ 𝑊 ) ”⟩ )
40 39 3adant2 ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) → ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ⟨“ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ( lastS ‘ 𝑊 ) ”⟩ )
41 40 adantr ( ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ⟨“ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ( lastS ‘ 𝑊 ) ”⟩ )
42 breq2 ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) → ( 1 < ( ♯ ‘ 𝑊 ) ↔ 1 < ( ♯ ‘ 𝑈 ) ) )
43 42 3anbi3d ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) → ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑈 ) ) ) )
44 swrd2lsw ( ( 𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑈 ) ) → ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑈 ) − 2 ) , ( ♯ ‘ 𝑈 ) ⟩ ) = ⟨“ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ( lastS ‘ 𝑈 ) ”⟩ )
45 44 3adant1 ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑈 ) ) → ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑈 ) − 2 ) , ( ♯ ‘ 𝑈 ) ⟩ ) = ⟨“ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ( lastS ‘ 𝑈 ) ”⟩ )
46 43 45 syl6bi ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) → ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) → ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑈 ) − 2 ) , ( ♯ ‘ 𝑈 ) ⟩ ) = ⟨“ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ( lastS ‘ 𝑈 ) ”⟩ ) )
47 46 impcom ( ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑈 ) − 2 ) , ( ♯ ‘ 𝑈 ) ⟩ ) = ⟨“ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ( lastS ‘ 𝑈 ) ”⟩ )
48 oveq1 ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) → ( ( ♯ ‘ 𝑊 ) − 2 ) = ( ( ♯ ‘ 𝑈 ) − 2 ) )
49 id ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) )
50 48 49 opeq12d ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) → ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ = ⟨ ( ( ♯ ‘ 𝑈 ) − 2 ) , ( ♯ ‘ 𝑈 ) ⟩ )
51 50 oveq2d ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) → ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑈 ) − 2 ) , ( ♯ ‘ 𝑈 ) ⟩ ) )
52 51 eqeq1d ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) → ( ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ⟨“ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ( lastS ‘ 𝑈 ) ”⟩ ↔ ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑈 ) − 2 ) , ( ♯ ‘ 𝑈 ) ⟩ ) = ⟨“ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ( lastS ‘ 𝑈 ) ”⟩ ) )
53 52 adantl ( ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ⟨“ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ( lastS ‘ 𝑈 ) ”⟩ ↔ ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑈 ) − 2 ) , ( ♯ ‘ 𝑈 ) ⟩ ) = ⟨“ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ( lastS ‘ 𝑈 ) ”⟩ ) )
54 47 53 mpbird ( ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ⟨“ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ( lastS ‘ 𝑈 ) ”⟩ )
55 41 54 eqeq12d ( ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) ↔ ⟨“ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ( lastS ‘ 𝑊 ) ”⟩ = ⟨“ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ( lastS ‘ 𝑈 ) ”⟩ ) )
56 fvexd ( ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∈ V )
57 fvexd ( ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( lastS ‘ 𝑊 ) ∈ V )
58 fvexd ( ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ∈ V )
59 fvexd ( ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( lastS ‘ 𝑈 ) ∈ V )
60 s2eq2s1eq ( ( ( ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∈ V ∧ ( lastS ‘ 𝑊 ) ∈ V ) ∧ ( ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ∈ V ∧ ( lastS ‘ 𝑈 ) ∈ V ) ) → ( ⟨“ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ( lastS ‘ 𝑊 ) ”⟩ = ⟨“ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ( lastS ‘ 𝑈 ) ”⟩ ↔ ( ⟨“ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ”⟩ = ⟨“ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ”⟩ ∧ ⟨“ ( lastS ‘ 𝑊 ) ”⟩ = ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) ) )
61 56 57 58 59 60 syl22anc ( ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( ⟨“ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ( lastS ‘ 𝑊 ) ”⟩ = ⟨“ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ( lastS ‘ 𝑈 ) ”⟩ ↔ ( ⟨“ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ”⟩ = ⟨“ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ”⟩ ∧ ⟨“ ( lastS ‘ 𝑊 ) ”⟩ = ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) ) )
62 fvex ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∈ V
63 s111 ( ( ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∈ V ∧ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ∈ V ) → ( ⟨“ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ”⟩ = ⟨“ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ”⟩ ↔ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ) )
64 62 58 63 sylancr ( ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( ⟨“ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ”⟩ = ⟨“ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ”⟩ ↔ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ) )
65 fvoveq1 ( ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑊 ) → ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) = ( 𝑈 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) )
66 65 eqcoms ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) → ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) = ( 𝑈 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) )
67 66 adantl ( ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) = ( 𝑈 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) )
68 67 eqeq2d ( ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ↔ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ) )
69 64 68 bitrd ( ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( ⟨“ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ”⟩ = ⟨“ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ”⟩ ↔ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ) )
70 fvex ( lastS ‘ 𝑊 ) ∈ V
71 s111 ( ( ( lastS ‘ 𝑊 ) ∈ V ∧ ( lastS ‘ 𝑈 ) ∈ V ) → ( ⟨“ ( lastS ‘ 𝑊 ) ”⟩ = ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ↔ ( lastS ‘ 𝑊 ) = ( lastS ‘ 𝑈 ) ) )
72 70 59 71 sylancr ( ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( ⟨“ ( lastS ‘ 𝑊 ) ”⟩ = ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ↔ ( lastS ‘ 𝑊 ) = ( lastS ‘ 𝑈 ) ) )
73 69 72 anbi12d ( ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( ( ⟨“ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ”⟩ = ⟨“ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 2 ) ) ”⟩ ∧ ⟨“ ( lastS ‘ 𝑊 ) ”⟩ = ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) ↔ ( ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∧ ( lastS ‘ 𝑊 ) = ( lastS ‘ 𝑈 ) ) ) )
74 55 61 73 3bitrd ( ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) ↔ ( ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∧ ( lastS ‘ 𝑊 ) = ( lastS ‘ 𝑈 ) ) ) )
75 74 anbi2d ( ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∧ ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) ↔ ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∧ ( ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∧ ( lastS ‘ 𝑊 ) = ( lastS ‘ 𝑈 ) ) ) ) )
76 3anass ( ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∧ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∧ ( lastS ‘ 𝑊 ) = ( lastS ‘ 𝑈 ) ) ↔ ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∧ ( ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∧ ( lastS ‘ 𝑊 ) = ( lastS ‘ 𝑈 ) ) ) )
77 75 76 bitr4di ( ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∧ ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) ↔ ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∧ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∧ ( lastS ‘ 𝑊 ) = ( lastS ‘ 𝑈 ) ) ) )
78 77 pm5.32da ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) → ( ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∧ ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) ↔ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∧ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∧ ( lastS ‘ 𝑊 ) = ( lastS ‘ 𝑈 ) ) ) ) )
79 38 78 bitrd ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) → ( 𝑊 = 𝑈 ↔ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 prefix ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∧ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) = ( 𝑈 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ∧ ( lastS ‘ 𝑊 ) = ( lastS ‘ 𝑈 ) ) ) ) )