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∈WordB→S++∅=S

Proof

Step Hyp Ref Expression
1 wrd0 ⊢∅∈WordB
2 ccatvalfn ⊢S∈WordB∧∅∈WordB→S++∅Fn0..^S+∅
3 1 2 mpan2 ⊢S∈WordB→S++∅Fn0..^S+∅
4 hash0 ⊢∅=0
5 4 oveq2i ⊢S+∅=S+0
6 lencl ⊢S∈WordB→S∈ℕ0
7 6 nn0cnd ⊢S∈WordB→S∈ℂ
8 7 addridd ⊢S∈WordB→S+0=S
9 5 8 eqtr2id ⊢S∈WordB→S=S+∅
10 9 oveq2d ⊢S∈WordB→0..^S=0..^S+∅
11 10 fneq2d ⊢S∈WordB→S++∅Fn0..^S↔S++∅Fn0..^S+∅
12 3 11 mpbird ⊢S∈WordB→S++∅Fn0..^S
13 wrdfn ⊢S∈WordB→SFn0..^S
14 ccatval1 ⊢S∈WordB∧∅∈WordB∧x∈0..^S→S++∅⁡x=S⁡x
15 1 14 mp3an2 ⊢S∈WordB∧x∈0..^S→S++∅⁡x=S⁡x
16 12 13 15 eqfnfvd ⊢S∈WordB→S++∅=S