Theorem ccatlid

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

	Ref	Expression
Assertion	ccatlid	⊢ ( 𝑆 ∈ Word 𝐵 → ( ∅ ++ 𝑆 ) = 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		wrd0	⊢ ∅ ∈ Word 𝐵
2		ccatvalfn	⊢ ( ( ∅ ∈ Word 𝐵 ∧ 𝑆 ∈ Word 𝐵 ) → ( ∅ ++ 𝑆 ) Fn ( 0 ..^ ( ( ♯ ‘ ∅ ) + ( ♯ ‘ 𝑆 ) ) ) )
3	1 2	mpan	⊢ ( 𝑆 ∈ Word 𝐵 → ( ∅ ++ 𝑆 ) Fn ( 0 ..^ ( ( ♯ ‘ ∅ ) + ( ♯ ‘ 𝑆 ) ) ) )
4		hash0	⊢ ( ♯ ‘ ∅ ) = 0
5	4	oveq1i	⊢ ( ( ♯ ‘ ∅ ) + ( ♯ ‘ 𝑆 ) ) = ( 0 + ( ♯ ‘ 𝑆 ) )
6		lencl	⊢ ( 𝑆 ∈ Word 𝐵 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
7	6	nn0cnd	⊢ ( 𝑆 ∈ Word 𝐵 → ( ♯ ‘ 𝑆 ) ∈ ℂ )
8	7	addid2d	⊢ ( 𝑆 ∈ Word 𝐵 → ( 0 + ( ♯ ‘ 𝑆 ) ) = ( ♯ ‘ 𝑆 ) )
9	5 8	eqtrid	⊢ ( 𝑆 ∈ Word 𝐵 → ( ( ♯ ‘ ∅ ) + ( ♯ ‘ 𝑆 ) ) = ( ♯ ‘ 𝑆 ) )
10	9	eqcomd	⊢ ( 𝑆 ∈ Word 𝐵 → ( ♯ ‘ 𝑆 ) = ( ( ♯ ‘ ∅ ) + ( ♯ ‘ 𝑆 ) ) )
11	10	oveq2d	⊢ ( 𝑆 ∈ Word 𝐵 → ( 0 ..^ ( ♯ ‘ 𝑆 ) ) = ( 0 ..^ ( ( ♯ ‘ ∅ ) + ( ♯ ‘ 𝑆 ) ) ) )
12	11	fneq2d	⊢ ( 𝑆 ∈ Word 𝐵 → ( ( ∅ ++ 𝑆 ) Fn ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ↔ ( ∅ ++ 𝑆 ) Fn ( 0 ..^ ( ( ♯ ‘ ∅ ) + ( ♯ ‘ 𝑆 ) ) ) ) )
13	3 12	mpbird	⊢ ( 𝑆 ∈ Word 𝐵 → ( ∅ ++ 𝑆 ) Fn ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
14		wrdfn	⊢ ( 𝑆 ∈ Word 𝐵 → 𝑆 Fn ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
15	4	a1i	⊢ ( 𝑆 ∈ Word 𝐵 → ( ♯ ‘ ∅ ) = 0 )
16	15 9	oveq12d	⊢ ( 𝑆 ∈ Word 𝐵 → ( ( ♯ ‘ ∅ ) ..^ ( ( ♯ ‘ ∅ ) + ( ♯ ‘ 𝑆 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
17	16	eleq2d	⊢ ( 𝑆 ∈ Word 𝐵 → ( 𝑥 ∈ ( ( ♯ ‘ ∅ ) ..^ ( ( ♯ ‘ ∅ ) + ( ♯ ‘ 𝑆 ) ) ) ↔ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) )
18	17	biimpar	⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → 𝑥 ∈ ( ( ♯ ‘ ∅ ) ..^ ( ( ♯ ‘ ∅ ) + ( ♯ ‘ 𝑆 ) ) ) )
19		ccatval2	⊢ ( ( ∅ ∈ Word 𝐵 ∧ 𝑆 ∈ Word 𝐵 ∧ 𝑥 ∈ ( ( ♯ ‘ ∅ ) ..^ ( ( ♯ ‘ ∅ ) + ( ♯ ‘ 𝑆 ) ) ) ) → ( ( ∅ ++ 𝑆 ) ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝑥 − ( ♯ ‘ ∅ ) ) ) )
20	1 19	mp3an1	⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑥 ∈ ( ( ♯ ‘ ∅ ) ..^ ( ( ♯ ‘ ∅ ) + ( ♯ ‘ 𝑆 ) ) ) ) → ( ( ∅ ++ 𝑆 ) ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝑥 − ( ♯ ‘ ∅ ) ) ) )
21	18 20	syldan	⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( ∅ ++ 𝑆 ) ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝑥 − ( ♯ ‘ ∅ ) ) ) )
22	4	oveq2i	⊢ ( 𝑥 − ( ♯ ‘ ∅ ) ) = ( 𝑥 − 0 )
23		elfzoelz	⊢ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) → 𝑥 ∈ ℤ )
24	23	adantl	⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → 𝑥 ∈ ℤ )
25	24	zcnd	⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → 𝑥 ∈ ℂ )
26	25	subid1d	⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( 𝑥 − 0 ) = 𝑥 )
27	22 26	eqtrid	⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( 𝑥 − ( ♯ ‘ ∅ ) ) = 𝑥 )
28	27	fveq2d	⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 ‘ ( 𝑥 − ( ♯ ‘ ∅ ) ) ) = ( 𝑆 ‘ 𝑥 ) )
29	21 28	eqtrd	⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( ∅ ++ 𝑆 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
30	13 14 29	eqfnfvd	⊢ ( 𝑆 ∈ Word 𝐵 → ( ∅ ++ 𝑆 ) = 𝑆 )