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

Proof

Step	Hyp	Ref	Expression
1		wrd0	|- (/) e. Word B
2		ccatvalfn	|- ( ( S e. Word B /\ (/) e. Word B ) -> ( S ++ (/) ) Fn ( 0 ..^ ( ( # ` S ) + ( # ` (/) ) ) ) )
3	1 2	mpan2	|- ( S e. Word B -> ( S ++ (/) ) Fn ( 0 ..^ ( ( # ` S ) + ( # ` (/) ) ) ) )
4		hash0	|- ( # ` (/) ) = 0
5	4	oveq2i	|- ( ( # ` S ) + ( # ` (/) ) ) = ( ( # ` S ) + 0 )
6		lencl	|- ( S e. Word B -> ( # ` S ) e. NN0 )
7	6	nn0cnd	|- ( S e. Word B -> ( # ` S ) e. CC )
8	7	addid1d	|- ( S e. Word B -> ( ( # ` S ) + 0 ) = ( # ` S ) )
9	5 8	syl5req	|- ( S e. Word B -> ( # ` S ) = ( ( # ` S ) + ( # ` (/) ) ) )
10	9	oveq2d	|- ( S e. Word B -> ( 0 ..^ ( # ` S ) ) = ( 0 ..^ ( ( # ` S ) + ( # ` (/) ) ) ) )
11	10	fneq2d	|- ( S e. Word B -> ( ( S ++ (/) ) Fn ( 0 ..^ ( # ` S ) ) <-> ( S ++ (/) ) Fn ( 0 ..^ ( ( # ` S ) + ( # ` (/) ) ) ) ) )
12	3 11	mpbird	|- ( S e. Word B -> ( S ++ (/) ) Fn ( 0 ..^ ( # ` S ) ) )
13		wrdfn	|- ( S e. Word B -> S Fn ( 0 ..^ ( # ` S ) ) )
14		ccatval1	|- ( ( S e. Word B /\ (/) e. Word B /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( ( S ++ (/) ) ` x ) = ( S ` x ) )
15	1 14	mp3an2	|- ( ( S e. Word B /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( ( S ++ (/) ) ` x ) = ( S ` x ) )
16	12 13 15	eqfnfvd	|- ( S e. Word B -> ( S ++ (/) ) = S )