# Metamath Proof Explorer

## Theorem ccatrid

Description: Concatenation of a word by the empty word on the right. (Contributed by Stefan O'Rear, 15-Aug-2015) (Proof shortened by AV, 1-May-2020)

Ref Expression
Assertion ccatrid ${⊢}{S}\in \mathrm{Word}{B}\to {S}\mathrm{++}\varnothing ={S}$

### Proof

Step Hyp Ref Expression
1 wrd0 ${⊢}\varnothing \in \mathrm{Word}{B}$
2 ccatvalfn ${⊢}\left({S}\in \mathrm{Word}{B}\wedge \varnothing \in \mathrm{Word}{B}\right)\to \left({S}\mathrm{++}\varnothing \right)Fn\left(0..^\left|{S}\right|+\left|\varnothing \right|\right)$
3 1 2 mpan2 ${⊢}{S}\in \mathrm{Word}{B}\to \left({S}\mathrm{++}\varnothing \right)Fn\left(0..^\left|{S}\right|+\left|\varnothing \right|\right)$
4 hash0 ${⊢}\left|\varnothing \right|=0$
5 4 oveq2i ${⊢}\left|{S}\right|+\left|\varnothing \right|=\left|{S}\right|+0$
6 lencl ${⊢}{S}\in \mathrm{Word}{B}\to \left|{S}\right|\in {ℕ}_{0}$
7 6 nn0cnd ${⊢}{S}\in \mathrm{Word}{B}\to \left|{S}\right|\in ℂ$
8 7 addid1d ${⊢}{S}\in \mathrm{Word}{B}\to \left|{S}\right|+0=\left|{S}\right|$
9 5 8 syl5req ${⊢}{S}\in \mathrm{Word}{B}\to \left|{S}\right|=\left|{S}\right|+\left|\varnothing \right|$
10 9 oveq2d ${⊢}{S}\in \mathrm{Word}{B}\to \left(0..^\left|{S}\right|\right)=\left(0..^\left|{S}\right|+\left|\varnothing \right|\right)$
11 10 fneq2d ${⊢}{S}\in \mathrm{Word}{B}\to \left(\left({S}\mathrm{++}\varnothing \right)Fn\left(0..^\left|{S}\right|\right)↔\left({S}\mathrm{++}\varnothing \right)Fn\left(0..^\left|{S}\right|+\left|\varnothing \right|\right)\right)$
12 3 11 mpbird ${⊢}{S}\in \mathrm{Word}{B}\to \left({S}\mathrm{++}\varnothing \right)Fn\left(0..^\left|{S}\right|\right)$
13 wrdfn ${⊢}{S}\in \mathrm{Word}{B}\to {S}Fn\left(0..^\left|{S}\right|\right)$
14 ccatval1 ${⊢}\left({S}\in \mathrm{Word}{B}\wedge \varnothing \in \mathrm{Word}{B}\wedge {x}\in \left(0..^\left|{S}\right|\right)\right)\to \left({S}\mathrm{++}\varnothing \right)\left({x}\right)={S}\left({x}\right)$
15 1 14 mp3an2 ${⊢}\left({S}\in \mathrm{Word}{B}\wedge {x}\in \left(0..^\left|{S}\right|\right)\right)\to \left({S}\mathrm{++}\varnothing \right)\left({x}\right)={S}\left({x}\right)$
16 12 13 15 eqfnfvd ${⊢}{S}\in \mathrm{Word}{B}\to {S}\mathrm{++}\varnothing ={S}$