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

Proof

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