Metamath Proof Explorer

Theorem eqwrd

Description: Two words are equal iff they have the same length and the same symbol at each position. (Contributed by AV, 13-Apr-2018) (Revised by JJ, 30-Dec-2023)

Ref Expression
Assertion eqwrd ⊢ U ∈ Word S ∧ W ∈ Word T → U = W ↔ U = W ∧ ∀ i ∈ 0 ..^ U U ⁡ i = W ⁡ i

Proof

Step Hyp Ref Expression
1 wrdfn ⊢ U ∈ Word S → U Fn 0 ..^ U
2 wrdfn ⊢ W ∈ Word T → W Fn 0 ..^ W
3 eqfnfv2 ⊢ U Fn 0 ..^ U ∧ W Fn 0 ..^ W → U = W ↔ 0 ..^ U = 0 ..^ W ∧ ∀ i ∈ 0 ..^ U U ⁡ i = W ⁡ i
4 1 2 3 syl2an ⊢ U ∈ Word S ∧ W ∈ Word T → U = W ↔ 0 ..^ U = 0 ..^ W ∧ ∀ i ∈ 0 ..^ U U ⁡ i = W ⁡ i
5 fveq2 ⊢ 0 ..^ U = 0 ..^ W → 0 ..^ U = 0 ..^ W
6 lencl ⊢ U ∈ Word S → U ∈ ℕ 0
7 hashfzo0 ⊢ U ∈ ℕ 0 → 0 ..^ U = U
8 6 7 syl ⊢ U ∈ Word S → 0 ..^ U = U
9 lencl ⊢ W ∈ Word T → W ∈ ℕ 0
10 hashfzo0 ⊢ W ∈ ℕ 0 → 0 ..^ W = W
11 9 10 syl ⊢ W ∈ Word T → 0 ..^ W = W
12 8 11 eqeqan12d ⊢ U ∈ Word S ∧ W ∈ Word T → 0 ..^ U = 0 ..^ W ↔ U = W
13 5 12 imbitrid ⊢ U ∈ Word S ∧ W ∈ Word T → 0 ..^ U = 0 ..^ W → U = W
14 oveq2 ⊢ U = W → 0 ..^ U = 0 ..^ W
15 13 14 impbid1 ⊢ U ∈ Word S ∧ W ∈ Word T → 0 ..^ U = 0 ..^ W ↔ U = W
16 15 anbi1d ⊢ U ∈ Word S ∧ W ∈ Word T → 0 ..^ U = 0 ..^ W ∧ ∀ i ∈ 0 ..^ U U ⁡ i = W ⁡ i ↔ U = W ∧ ∀ i ∈ 0 ..^ U U ⁡ i = W ⁡ i
17 4 16 bitrd ⊢ U ∈ Word S ∧ W ∈ Word T → U = W ↔ U = W ∧ ∀ i ∈ 0 ..^ U U ⁡ i = W ⁡ i