# Metamath Proof Explorer

## Theorem repswsymballbi

Description: A word is a "repeated symbol word" iff each of its symbols equals the first symbol of the word. (Contributed by AV, 10-Nov-2018)

Ref Expression
Assertion repswsymballbi ${⊢}{W}\in \mathrm{Word}{V}\to \left({W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|↔\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$

### Proof

Step Hyp Ref Expression
1 fveq2 ${⊢}{W}=\varnothing \to \left|{W}\right|=\left|\varnothing \right|$
2 hash0 ${⊢}\left|\varnothing \right|=0$
3 1 2 syl6eq ${⊢}{W}=\varnothing \to \left|{W}\right|=0$
4 fvex ${⊢}{W}\left(0\right)\in \mathrm{V}$
5 repsw0 ${⊢}{W}\left(0\right)\in \mathrm{V}\to {W}\left(0\right)\mathrm{repeatS}0=\varnothing$
6 4 5 ax-mp ${⊢}{W}\left(0\right)\mathrm{repeatS}0=\varnothing$
7 6 eqcomi ${⊢}\varnothing ={W}\left(0\right)\mathrm{repeatS}0$
8 simpr ${⊢}\left(\left|{W}\right|=0\wedge {W}=\varnothing \right)\to {W}=\varnothing$
9 oveq2 ${⊢}\left|{W}\right|=0\to {W}\left(0\right)\mathrm{repeatS}\left|{W}\right|={W}\left(0\right)\mathrm{repeatS}0$
10 9 adantr ${⊢}\left(\left|{W}\right|=0\wedge {W}=\varnothing \right)\to {W}\left(0\right)\mathrm{repeatS}\left|{W}\right|={W}\left(0\right)\mathrm{repeatS}0$
11 7 8 10 3eqtr4a ${⊢}\left(\left|{W}\right|=0\wedge {W}=\varnothing \right)\to {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|$
12 ral0 ${⊢}\forall {i}\in \varnothing \phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)$
13 oveq2 ${⊢}\left|{W}\right|=0\to \left(0..^\left|{W}\right|\right)=\left(0..^0\right)$
14 fzo0 ${⊢}\left(0..^0\right)=\varnothing$
15 13 14 syl6eq ${⊢}\left|{W}\right|=0\to \left(0..^\left|{W}\right|\right)=\varnothing$
16 15 raleqdv ${⊢}\left|{W}\right|=0\to \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)↔\forall {i}\in \varnothing \phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
17 12 16 mpbiri ${⊢}\left|{W}\right|=0\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)$
18 17 adantr ${⊢}\left(\left|{W}\right|=0\wedge {W}=\varnothing \right)\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)$
19 11 18 2thd ${⊢}\left(\left|{W}\right|=0\wedge {W}=\varnothing \right)\to \left({W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|↔\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
20 3 19 mpancom ${⊢}{W}=\varnothing \to \left({W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|↔\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
21 20 a1d ${⊢}{W}=\varnothing \to \left({W}\in \mathrm{Word}{V}\to \left({W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|↔\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)\right)$
22 df-3an ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|=\left|{W}\right|\wedge \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)↔\left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|=\left|{W}\right|\right)\wedge \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
23 22 a1i ${⊢}\left({W}\ne \varnothing \wedge {W}\in \mathrm{Word}{V}\right)\to \left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|=\left|{W}\right|\wedge \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)↔\left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|=\left|{W}\right|\right)\wedge \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)\right)$
24 fstwrdne ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {W}\ne \varnothing \right)\to {W}\left(0\right)\in {V}$
25 24 ancoms ${⊢}\left({W}\ne \varnothing \wedge {W}\in \mathrm{Word}{V}\right)\to {W}\left(0\right)\in {V}$
26 lencl ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|\in {ℕ}_{0}$
27 26 adantl ${⊢}\left({W}\ne \varnothing \wedge {W}\in \mathrm{Word}{V}\right)\to \left|{W}\right|\in {ℕ}_{0}$
28 repsdf2 ${⊢}\left({W}\left(0\right)\in {V}\wedge \left|{W}\right|\in {ℕ}_{0}\right)\to \left({W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|↔\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|=\left|{W}\right|\wedge \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)\right)$
29 25 27 28 syl2anc ${⊢}\left({W}\ne \varnothing \wedge {W}\in \mathrm{Word}{V}\right)\to \left({W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|↔\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|=\left|{W}\right|\wedge \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)\right)$
30 simpr ${⊢}\left({W}\ne \varnothing \wedge {W}\in \mathrm{Word}{V}\right)\to {W}\in \mathrm{Word}{V}$
31 eqidd ${⊢}\left({W}\ne \varnothing \wedge {W}\in \mathrm{Word}{V}\right)\to \left|{W}\right|=\left|{W}\right|$
32 30 31 jca ${⊢}\left({W}\ne \varnothing \wedge {W}\in \mathrm{Word}{V}\right)\to \left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|=\left|{W}\right|\right)$
33 32 biantrurd ${⊢}\left({W}\ne \varnothing \wedge {W}\in \mathrm{Word}{V}\right)\to \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)↔\left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|=\left|{W}\right|\right)\wedge \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)\right)$
34 23 29 33 3bitr4d ${⊢}\left({W}\ne \varnothing \wedge {W}\in \mathrm{Word}{V}\right)\to \left({W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|↔\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
35 34 ex ${⊢}{W}\ne \varnothing \to \left({W}\in \mathrm{Word}{V}\to \left({W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|↔\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)\right)$
36 21 35 pm2.61ine ${⊢}{W}\in \mathrm{Word}{V}\to \left({W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|↔\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$