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 ⊢W∈WordV∧U∈WordV∧1<W→W=U↔W=U∧WprefixW−2=UprefixW−2∧W⁡W−2=U⁡W−2∧lastS⁡W=lastS⁡U

Proof

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