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