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∈WordV∧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”⟩∈WordV
2 eqwrd ⊢W∈WordV∧⟨“ABC”⟩∈WordV→W=⟨“ABC”⟩↔W=⟨“ABC”⟩∧∀i∈0..^WW⁡i=⟨“ABC”⟩⁡i
3 1 2 sylan2 ⊢W∈WordV∧A∈V∧B∈V∧C∈V→W=⟨“ABC”⟩↔W=⟨“ABC”⟩∧∀i∈0..^WW⁡i=⟨“ABC”⟩⁡i
4 s3len ⊢⟨“ABC”⟩=3
5 4 eqeq2i ⊢W=⟨“ABC”⟩↔W=3
6 5 a1i ⊢W∈WordV∧A∈V∧B∈V∧C∈V→W=⟨“ABC”⟩↔W=3
7 6 anbi1d ⊢W∈WordV∧A∈V∧B∈V∧C∈V→W=⟨“ABC”⟩∧∀i∈0..^WW⁡i=⟨“ABC”⟩⁡i↔W=3∧∀i∈0..^WW⁡i=⟨“ABC”⟩⁡i
8 oveq2 ⊢W=3→0..^W=0..^3
9 fzo0to3tp ⊢0..^3=012
10 8 9 eqtrdi ⊢W=3→0..^W=012
11 10 raleqdv ⊢W=3→∀i∈0..^WW⁡i=⟨“ABC”⟩⁡i↔∀i∈012W⁡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∈012W⁡i=⟨“ABC”⟩⁡i↔W⁡0=A∧W⁡1=B∧W⁡2=C
38 37 adantl ⊢W∈WordV∧A∈V∧B∈V∧C∈V→∀i∈012W⁡i=⟨“ABC”⟩⁡i↔W⁡0=A∧W⁡1=B∧W⁡2=C
39 11 38 sylan9bbr ⊢W∈WordV∧A∈V∧B∈V∧C∈V∧W=3→∀i∈0..^WW⁡i=⟨“ABC”⟩⁡i↔W⁡0=A∧W⁡1=B∧W⁡2=C
40 39 pm5.32da ⊢W∈WordV∧A∈V∧B∈V∧C∈V→W=3∧∀i∈0..^WW⁡i=⟨“ABC”⟩⁡i↔W=3∧W⁡0=A∧W⁡1=B∧W⁡2=C
41 3 7 40 3bitrd ⊢W∈WordV∧A∈V∧B∈V∧C∈V→W=⟨“ABC”⟩↔W=3∧W⁡0=A∧W⁡1=B∧W⁡2=C