Theorem ccat2s1lenOLD

Description: Obsolete version of ccat2s1len as of 14-Jan-2024. The length of the concatenation of two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ccat2s1lenOLD	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ♯ ‘ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) = 2 )

Proof

Step	Hyp	Ref	Expression
1		s1cl	⊢ ( 𝑋 ∈ 𝑉 → ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 )
2		s1cl	⊢ ( 𝑌 ∈ 𝑉 → ⟨“ 𝑌 ”⟩ ∈ Word 𝑉 )
3		ccatlenOLD	⊢ ( ( ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 ∧ ⟨“ 𝑌 ”⟩ ∈ Word 𝑉 ) → ( ♯ ‘ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) = ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) + ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) ) )
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 𝑉 ∧ ⟨“ 𝑌 ”⟩ ∈ Word 𝑉 ) → ( ♯ ‘ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) = 2 )
10	1 2 9	syl2an	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ♯ ‘ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) = 2 )