Theorem cats1len

Description: The length of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Hypotheses	cats1cld.1	|- T = ( S ++ <" X "> )
	cats1cli.2	|- S e. Word _V
	cats1fvn.3	|- ( # ` S ) = M
	cats1len.4	|- ( M + 1 ) = N
Assertion	cats1len	|- ( # ` T ) = N

Proof

Step	Hyp	Ref	Expression
1		cats1cld.1	|- T = ( S ++ <" X "> )
2		cats1cli.2	|- S e. Word _V
3		cats1fvn.3	|- ( # ` S ) = M
4		cats1len.4	|- ( M + 1 ) = N
5	1	fveq2i	|- ( # ` T ) = ( # ` ( S ++ <" X "> ) )
6		s1cli	|- <" X "> e. Word _V
7		ccatlen	|- ( ( S e. Word _V /\ <" X "> e. Word _V ) -> ( # ` ( S ++ <" X "> ) ) = ( ( # ` S ) + ( # ` <" X "> ) ) )
8	2 6 7	mp2an	|- ( # ` ( S ++ <" X "> ) ) = ( ( # ` S ) + ( # ` <" X "> ) )
9		s1len	|- ( # ` <" X "> ) = 1
10	3 9	oveq12i	|- ( ( # ` S ) + ( # ` <" X "> ) ) = ( M + 1 )
11	8 10	eqtri	|- ( # ` ( S ++ <" X "> ) ) = ( M + 1 )
12	11 4	eqtri	|- ( # ` ( S ++ <" X "> ) ) = N
13	5 12	eqtri	|- ( # ` T ) = N