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 ⊢ W ∈ Word V ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → W = ⟨“ ABC ”⟩ ↔ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 1 = B ∧ W ⁡ 2 = C

Proof

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