Theorem cats1len

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

	Ref	Expression
Hypotheses	cats1cld.1	⊢ 𝑇 = ( 𝑆 ++ ⟨“ 𝑋 ”⟩ )
	cats1cli.2	⊢ 𝑆 ∈ Word V
	cats1fvn.3	⊢ ( ♯ ‘ 𝑆 ) = 𝑀
	cats1len.4	⊢ ( 𝑀 + 1 ) = 𝑁
Assertion	cats1len	⊢ ( ♯ ‘ 𝑇 ) = 𝑁

Proof

Step	Hyp	Ref	Expression
1		cats1cld.1	⊢ 𝑇 = ( 𝑆 ++ ⟨“ 𝑋 ”⟩ )
2		cats1cli.2	⊢ 𝑆 ∈ Word V
3		cats1fvn.3	⊢ ( ♯ ‘ 𝑆 ) = 𝑀
4		cats1len.4	⊢ ( 𝑀 + 1 ) = 𝑁
5	1	fveq2i	⊢ ( ♯ ‘ 𝑇 ) = ( ♯ ‘ ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) )
6		s1cli	⊢ ⟨“ 𝑋 ”⟩ ∈ Word V
7		ccatlen	⊢ ( ( 𝑆 ∈ Word V ∧ ⟨“ 𝑋 ”⟩ ∈ Word V ) → ( ♯ ‘ ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) ) = ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) )
8	2 6 7	mp2an	⊢ ( ♯ ‘ ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) ) = ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) )
9		s1len	⊢ ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) = 1
10	3 9	oveq12i	⊢ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑀 + 1 )
11	8 10	eqtri	⊢ ( ♯ ‘ ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑀 + 1 )
12	11 4	eqtri	⊢ ( ♯ ‘ ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) ) = 𝑁
13	5 12	eqtri	⊢ ( ♯ ‘ 𝑇 ) = 𝑁