Theorem ccat2s1len

Description: The length of the concatenation of two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Revised by JJ, 14-Jan-2024)

	Ref	Expression
Assertion	ccat2s1len	⊢ ( ♯ ‘ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) = 2

Proof

Step	Hyp	Ref	Expression
1		s1cli	⊢ ⟨“ 𝑋 ”⟩ ∈ Word V
2		s1cli	⊢ ⟨“ 𝑌 ”⟩ ∈ Word V
3		ccatlen	⊢ ( ( ⟨“ 𝑋 ”⟩ ∈ Word V ∧ ⟨“ 𝑌 ”⟩ ∈ Word V ) → ( ♯ ‘ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) = ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) + ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) ) )
4		s1len	⊢ ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) = 1
5		s1len	⊢ ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) = 1
6	4 5	oveq12i	⊢ ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) + ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) ) = ( 1 + 1 )
7		1p1e2	⊢ ( 1 + 1 ) = 2
8	6 7	eqtri	⊢ ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) + ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) ) = 2
9	3 8	eqtrdi	⊢ ( ( ⟨“ 𝑋 ”⟩ ∈ Word V ∧ ⟨“ 𝑌 ”⟩ ∈ Word V ) → ( ♯ ‘ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) = 2 )
10	1 2 9	mp2an	⊢ ( ♯ ‘ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) = 2