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	|- ( S e. Word B -> ( (/) ++ S ) = S )

Proof

Step	Hyp	Ref	Expression
1		wrd0	|- (/) e. Word B
2		ccatvalfn	|- ( ( (/) e. Word B /\ S e. Word B ) -> ( (/) ++ S ) Fn ( 0 ..^ ( ( # ` (/) ) + ( # ` S ) ) ) )
3	1 2	mpan	|- ( S e. Word B -> ( (/) ++ S ) Fn ( 0 ..^ ( ( # ` (/) ) + ( # ` S ) ) ) )
4		hash0	|- ( # ` (/) ) = 0
5	4	oveq1i	|- ( ( # ` (/) ) + ( # ` S ) ) = ( 0 + ( # ` S ) )
6		lencl	|- ( S e. Word B -> ( # ` S ) e. NN0 )
7	6	nn0cnd	|- ( S e. Word B -> ( # ` S ) e. CC )
8	7	addid2d	|- ( S e. Word B -> ( 0 + ( # ` S ) ) = ( # ` S ) )
9	5 8	eqtrid	|- ( S e. Word B -> ( ( # ` (/) ) + ( # ` S ) ) = ( # ` S ) )
10	9	eqcomd	|- ( S e. Word B -> ( # ` S ) = ( ( # ` (/) ) + ( # ` S ) ) )
11	10	oveq2d	|- ( S e. Word B -> ( 0 ..^ ( # ` S ) ) = ( 0 ..^ ( ( # ` (/) ) + ( # ` S ) ) ) )
12	11	fneq2d	|- ( S e. Word B -> ( ( (/) ++ S ) Fn ( 0 ..^ ( # ` S ) ) <-> ( (/) ++ S ) Fn ( 0 ..^ ( ( # ` (/) ) + ( # ` S ) ) ) ) )
13	3 12	mpbird	|- ( S e. Word B -> ( (/) ++ S ) Fn ( 0 ..^ ( # ` S ) ) )
14		wrdfn	|- ( S e. Word B -> S Fn ( 0 ..^ ( # ` S ) ) )
15	4	a1i	|- ( S e. Word B -> ( # ` (/) ) = 0 )
16	15 9	oveq12d	|- ( S e. Word B -> ( ( # ` (/) ) ..^ ( ( # ` (/) ) + ( # ` S ) ) ) = ( 0 ..^ ( # ` S ) ) )
17	16	eleq2d	|- ( S e. Word B -> ( x e. ( ( # ` (/) ) ..^ ( ( # ` (/) ) + ( # ` S ) ) ) <-> x e. ( 0 ..^ ( # ` S ) ) ) )
18	17	biimpar	|- ( ( S e. Word B /\ x e. ( 0 ..^ ( # ` S ) ) ) -> x e. ( ( # ` (/) ) ..^ ( ( # ` (/) ) + ( # ` S ) ) ) )
19		ccatval2	|- ( ( (/) e. Word B /\ S e. Word B /\ x e. ( ( # ` (/) ) ..^ ( ( # ` (/) ) + ( # ` S ) ) ) ) -> ( ( (/) ++ S ) ` x ) = ( S ` ( x - ( # ` (/) ) ) ) )
20	1 19	mp3an1	|- ( ( S e. Word B /\ x e. ( ( # ` (/) ) ..^ ( ( # ` (/) ) + ( # ` S ) ) ) ) -> ( ( (/) ++ S ) ` x ) = ( S ` ( x - ( # ` (/) ) ) ) )
21	18 20	syldan	|- ( ( S e. Word B /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( ( (/) ++ S ) ` x ) = ( S ` ( x - ( # ` (/) ) ) ) )
22	4	oveq2i	|- ( x - ( # ` (/) ) ) = ( x - 0 )
23		elfzoelz	|- ( x e. ( 0 ..^ ( # ` S ) ) -> x e. ZZ )
24	23	adantl	|- ( ( S e. Word B /\ x e. ( 0 ..^ ( # ` S ) ) ) -> x e. ZZ )
25	24	zcnd	|- ( ( S e. Word B /\ x e. ( 0 ..^ ( # ` S ) ) ) -> x e. CC )
26	25	subid1d	|- ( ( S e. Word B /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( x - 0 ) = x )
27	22 26	eqtrid	|- ( ( S e. Word B /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( x - ( # ` (/) ) ) = x )
28	27	fveq2d	|- ( ( S e. Word B /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( S ` ( x - ( # ` (/) ) ) ) = ( S ` x ) )
29	21 28	eqtrd	|- ( ( S e. Word B /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( ( (/) ++ S ) ` x ) = ( S ` x ) )
30	13 14 29	eqfnfvd	|- ( S e. Word B -> ( (/) ++ S ) = S )