Metamath Proof Explorer

Theorem eqwrds3

Description: A word is equal with a length 3 string iff it has length 3 and the same symbol at each position. (Contributed by AV, 12-May-2021)

Ref Expression
Assertion eqwrds3 ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝑊 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ↔ ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 1 ) = 𝐵 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 s3cl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑉 )
2 eqwrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑉 ) → ( 𝑊 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ↔ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) ) ) )
3 1 2 sylan2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝑊 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ↔ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) ) ) )
4 s3len ⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3
5 4 eqeq2i ⊢ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ↔ ( ♯ ‘ 𝑊 ) = 3 )
6 5 a1i ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ↔ ( ♯ ‘ 𝑊 ) = 3 ) )
7 6 anbi1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) ) ↔ ( ( ♯ ‘ 𝑊 ) = 3 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) ) ) )
8 oveq2 ⊢ ( ( ♯ ‘ 𝑊 ) = 3 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ 3 ) )
9 fzo0to3tp ⊢ ( 0 ..^ 3 ) = { 0 , 1 , 2 }
10 8 9 eqtrdi ⊢ ( ( ♯ ‘ 𝑊 ) = 3 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = { 0 , 1 , 2 } )
11 10 raleqdv ⊢ ( ( ♯ ‘ 𝑊 ) = 3 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ { 0 , 1 , 2 } ( 𝑊 ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) ) )
12 fveq2 ⊢ ( 𝑖 = 0 → ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) )
13 fveq2 ⊢ ( 𝑖 = 0 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) )
14 12 13 eqeq12d ⊢ ( 𝑖 = 0 → ( ( 𝑊 ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) ↔ ( 𝑊 ‘ 0 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ) )
15 s3fv0 ⊢ ( 𝐴 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 )
16 15 3ad2ant1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 )
17 16 eqeq2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝑊 ‘ 0 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ↔ ( 𝑊 ‘ 0 ) = 𝐴 ) )
18 14 17 sylan9bbr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝑖 = 0 ) → ( ( 𝑊 ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) ↔ ( 𝑊 ‘ 0 ) = 𝐴 ) )
19 fveq2 ⊢ ( 𝑖 = 1 → ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 1 ) )
20 fveq2 ⊢ ( 𝑖 = 1 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) )
21 19 20 eqeq12d ⊢ ( 𝑖 = 1 → ( ( 𝑊 ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) ↔ ( 𝑊 ‘ 1 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) )
22 s3fv1 ⊢ ( 𝐵 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) = 𝐵 )
23 22 3ad2ant2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) = 𝐵 )
24 23 eqeq2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝑊 ‘ 1 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ↔ ( 𝑊 ‘ 1 ) = 𝐵 ) )
25 21 24 sylan9bbr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝑖 = 1 ) → ( ( 𝑊 ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) ↔ ( 𝑊 ‘ 1 ) = 𝐵 ) )
26 fveq2 ⊢ ( 𝑖 = 2 → ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 2 ) )
27 fveq2 ⊢ ( 𝑖 = 2 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) )
28 26 27 eqeq12d ⊢ ( 𝑖 = 2 → ( ( 𝑊 ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) ↔ ( 𝑊 ‘ 2 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) )
29 s3fv2 ⊢ ( 𝐶 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 )
30 29 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 )
31 30 eqeq2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝑊 ‘ 2 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ↔ ( 𝑊 ‘ 2 ) = 𝐶 ) )
32 28 31 sylan9bbr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝑖 = 2 ) → ( ( 𝑊 ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) ↔ ( 𝑊 ‘ 2 ) = 𝐶 ) )
33 0zd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → 0 ∈ ℤ )
34 1zzd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → 1 ∈ ℤ )
35 2z ⊢ 2 ∈ ℤ
36 35 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → 2 ∈ ℤ )
37 18 25 32 33 34 36 raltpd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ∀ 𝑖 ∈ { 0 , 1 , 2 } ( 𝑊 ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) ↔ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 1 ) = 𝐵 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) ) )
38 37 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ∀ 𝑖 ∈ { 0 , 1 , 2 } ( 𝑊 ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) ↔ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 1 ) = 𝐵 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) ) )
39 11 38 sylan9bbr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( ♯ ‘ 𝑊 ) = 3 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) ↔ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 1 ) = 𝐵 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) ) )
40 39 pm5.32da ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( ( ♯ ‘ 𝑊 ) = 3 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 𝑖 ) ) ↔ ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 1 ) = 𝐵 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) ) ) )
41 3 7 40 3bitrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝑊 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ↔ ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 1 ) = 𝐵 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) ) ) )