This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑆 ∈ Word 𝐵 → ( 𝑆 ++ ∅ ) = 𝑆 )

Proof

Step Hyp Ref Expression
1 wrd0 ⊢ ∅ ∈ Word 𝐵
2 ccatvalfn ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ ∅ ∈ Word 𝐵 ) → ( 𝑆 ++ ∅ ) Fn ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ∅ ) ) ) )
3 1 2 mpan2 ⊢ ( 𝑆 ∈ Word 𝐵 → ( 𝑆 ++ ∅ ) Fn ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ∅ ) ) ) )
4 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
5 4 oveq2i ⊢ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ∅ ) ) = ( ( ♯ ‘ 𝑆 ) + 0 )
6 lencl ⊢ ( 𝑆 ∈ Word 𝐵 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
7 6 nn0cnd ⊢ ( 𝑆 ∈ Word 𝐵 → ( ♯ ‘ 𝑆 ) ∈ ℂ )
8 7 addridd ⊢ ( 𝑆 ∈ Word 𝐵 → ( ( ♯ ‘ 𝑆 ) + 0 ) = ( ♯ ‘ 𝑆 ) )
9 5 8 eqtr2id ⊢ ( 𝑆 ∈ Word 𝐵 → ( ♯ ‘ 𝑆 ) = ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ∅ ) ) )
10 9 oveq2d ⊢ ( 𝑆 ∈ Word 𝐵 → ( 0 ..^ ( ♯ ‘ 𝑆 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ∅ ) ) ) )
11 10 fneq2d ⊢ ( 𝑆 ∈ Word 𝐵 → ( ( 𝑆 ++ ∅ ) Fn ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ↔ ( 𝑆 ++ ∅ ) Fn ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ∅ ) ) ) ) )
12 3 11 mpbird ⊢ ( 𝑆 ∈ Word 𝐵 → ( 𝑆 ++ ∅ ) Fn ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
13 wrdfn ⊢ ( 𝑆 ∈ Word 𝐵 → 𝑆 Fn ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
14 ccatval1 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ ∅ ∈ Word 𝐵 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 ++ ∅ ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
15 1 14 mp3an2 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 ++ ∅ ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
16 12 13 15 eqfnfvd ⊢ ( 𝑆 ∈ Word 𝐵 → ( 𝑆 ++ ∅ ) = 𝑆 )