# Metamath Proof Explorer

## Theorem ccats1val2

Description: Value of the symbol concatenated with a word. (Contributed by Alexander van der Vekens, 5-Aug-2018) (Proof shortened by Alexander van der Vekens, 14-Oct-2018)

Ref Expression
Assertion ccats1val2 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {S}\in {V}\wedge {I}=\left|{W}\right|\right)\to \left({W}\mathrm{++}⟨“{S}”⟩\right)\left({I}\right)={S}$

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {S}\in {V}\wedge {I}=\left|{W}\right|\right)\to {W}\in \mathrm{Word}{V}$
2 s1cl ${⊢}{S}\in {V}\to ⟨“{S}”⟩\in \mathrm{Word}{V}$
3 2 3ad2ant2 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {S}\in {V}\wedge {I}=\left|{W}\right|\right)\to ⟨“{S}”⟩\in \mathrm{Word}{V}$
4 lencl ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|\in {ℕ}_{0}$
5 4 nn0zd ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|\in ℤ$
6 elfzomin ${⊢}\left|{W}\right|\in ℤ\to \left|{W}\right|\in \left(\left|{W}\right|..^\left|{W}\right|+1\right)$
7 5 6 syl ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|\in \left(\left|{W}\right|..^\left|{W}\right|+1\right)$
8 s1len ${⊢}\left|⟨“{S}”⟩\right|=1$
9 8 oveq2i ${⊢}\left|{W}\right|+\left|⟨“{S}”⟩\right|=\left|{W}\right|+1$
10 9 oveq2i ${⊢}\left(\left|{W}\right|..^\left|{W}\right|+\left|⟨“{S}”⟩\right|\right)=\left(\left|{W}\right|..^\left|{W}\right|+1\right)$
11 7 10 eleqtrrdi ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|\in \left(\left|{W}\right|..^\left|{W}\right|+\left|⟨“{S}”⟩\right|\right)$
12 11 adantr ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {I}=\left|{W}\right|\right)\to \left|{W}\right|\in \left(\left|{W}\right|..^\left|{W}\right|+\left|⟨“{S}”⟩\right|\right)$
13 eleq1 ${⊢}{I}=\left|{W}\right|\to \left({I}\in \left(\left|{W}\right|..^\left|{W}\right|+\left|⟨“{S}”⟩\right|\right)↔\left|{W}\right|\in \left(\left|{W}\right|..^\left|{W}\right|+\left|⟨“{S}”⟩\right|\right)\right)$
14 13 adantl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {I}=\left|{W}\right|\right)\to \left({I}\in \left(\left|{W}\right|..^\left|{W}\right|+\left|⟨“{S}”⟩\right|\right)↔\left|{W}\right|\in \left(\left|{W}\right|..^\left|{W}\right|+\left|⟨“{S}”⟩\right|\right)\right)$
15 12 14 mpbird ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {I}=\left|{W}\right|\right)\to {I}\in \left(\left|{W}\right|..^\left|{W}\right|+\left|⟨“{S}”⟩\right|\right)$
16 15 3adant2 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {S}\in {V}\wedge {I}=\left|{W}\right|\right)\to {I}\in \left(\left|{W}\right|..^\left|{W}\right|+\left|⟨“{S}”⟩\right|\right)$
17 ccatval2 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge ⟨“{S}”⟩\in \mathrm{Word}{V}\wedge {I}\in \left(\left|{W}\right|..^\left|{W}\right|+\left|⟨“{S}”⟩\right|\right)\right)\to \left({W}\mathrm{++}⟨“{S}”⟩\right)\left({I}\right)=⟨“{S}”⟩\left({I}-\left|{W}\right|\right)$
18 1 3 16 17 syl3anc ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {S}\in {V}\wedge {I}=\left|{W}\right|\right)\to \left({W}\mathrm{++}⟨“{S}”⟩\right)\left({I}\right)=⟨“{S}”⟩\left({I}-\left|{W}\right|\right)$
19 oveq1 ${⊢}{I}=\left|{W}\right|\to {I}-\left|{W}\right|=\left|{W}\right|-\left|{W}\right|$
20 19 3ad2ant3 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {S}\in {V}\wedge {I}=\left|{W}\right|\right)\to {I}-\left|{W}\right|=\left|{W}\right|-\left|{W}\right|$
21 4 nn0cnd ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|\in ℂ$
22 21 subidd ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|-\left|{W}\right|=0$
23 22 3ad2ant1 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {S}\in {V}\wedge {I}=\left|{W}\right|\right)\to \left|{W}\right|-\left|{W}\right|=0$
24 20 23 eqtrd ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {S}\in {V}\wedge {I}=\left|{W}\right|\right)\to {I}-\left|{W}\right|=0$
25 24 fveq2d ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {S}\in {V}\wedge {I}=\left|{W}\right|\right)\to ⟨“{S}”⟩\left({I}-\left|{W}\right|\right)=⟨“{S}”⟩\left(0\right)$
26 s1fv ${⊢}{S}\in {V}\to ⟨“{S}”⟩\left(0\right)={S}$
27 26 3ad2ant2 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {S}\in {V}\wedge {I}=\left|{W}\right|\right)\to ⟨“{S}”⟩\left(0\right)={S}$
28 18 25 27 3eqtrd ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {S}\in {V}\wedge {I}=\left|{W}\right|\right)\to \left({W}\mathrm{++}⟨“{S}”⟩\right)\left({I}\right)={S}$