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 ‘ 𝑈 ) ) ) ) )