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 ( ( 𝑈 ∈ Word 𝑆 ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝑈 = 𝑊 ↔ ( ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑊 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ( 𝑈 ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) ) ) )

Proof

Step Hyp Ref Expression
1 wrdfn ⊢ ( 𝑈 ∈ Word 𝑆 → 𝑈 Fn ( 0 ..^ ( ♯ ‘ 𝑈 ) ) )
2 wrdfn ⊢ ( 𝑊 ∈ Word 𝑇 → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
3 eqfnfv2 ⊢ ( ( 𝑈 Fn ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ∧ 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑈 = 𝑊 ↔ ( ( 0 ..^ ( ♯ ‘ 𝑈 ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ( 𝑈 ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) ) ) )
4 1 2 3 syl2an ⊢ ( ( 𝑈 ∈ Word 𝑆 ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝑈 = 𝑊 ↔ ( ( 0 ..^ ( ♯ ‘ 𝑈 ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ( 𝑈 ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) ) ) )
5 fveq2 ⊢ ( ( 0 ..^ ( ♯ ‘ 𝑈 ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
6 lencl ⊢ ( 𝑈 ∈ Word 𝑆 → ( ♯ ‘ 𝑈 ) ∈ ℕ0 )
7 hashfzo0 ⊢ ( ( ♯ ‘ 𝑈 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ) = ( ♯ ‘ 𝑈 ) )
8 6 7 syl ⊢ ( 𝑈 ∈ Word 𝑆 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ) = ( ♯ ‘ 𝑈 ) )
9 lencl ⊢ ( 𝑊 ∈ Word 𝑇 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
10 hashfzo0 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) = ( ♯ ‘ 𝑊 ) )
11 9 10 syl ⊢ ( 𝑊 ∈ Word 𝑇 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) = ( ♯ ‘ 𝑊 ) )
12 8 11 eqeqan12d ⊢ ( ( 𝑈 ∈ Word 𝑆 ∧ 𝑊 ∈ Word 𝑇 ) → ( ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ↔ ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑊 ) ) )
13 5 12 syl5ib ⊢ ( ( 𝑈 ∈ Word 𝑆 ∧ 𝑊 ∈ Word 𝑇 ) → ( ( 0 ..^ ( ♯ ‘ 𝑈 ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑊 ) ) )
14 oveq2 ⊢ ( ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑊 ) → ( 0 ..^ ( ♯ ‘ 𝑈 ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
15 13 14 impbid1 ⊢ ( ( 𝑈 ∈ Word 𝑆 ∧ 𝑊 ∈ Word 𝑇 ) → ( ( 0 ..^ ( ♯ ‘ 𝑈 ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑊 ) ) )
16 15 anbi1d ⊢ ( ( 𝑈 ∈ Word 𝑆 ∧ 𝑊 ∈ Word 𝑇 ) → ( ( ( 0 ..^ ( ♯ ‘ 𝑈 ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ( 𝑈 ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) ) ↔ ( ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑊 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ( 𝑈 ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) ) ) )
17 4 16 bitrd ⊢ ( ( 𝑈 ∈ Word 𝑆 ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝑈 = 𝑊 ↔ ( ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑊 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ( 𝑈 ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) ) ) )