Theorem ccat2s1fvwALT

Description: Alternate proof of ccat2s1fvw using words of length 2, see df-s2 . A symbol of the concatenation of a word with two single symbols corresponding to the symbol of the word. (Contributed by AV, 22-Sep-2018) (Proof shortened by Mario Carneiro/AV, 21-Oct-2018) (Revised by AV, 28-Jan-2024) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	ccat2s1fvwALT	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		ccatw2s1ccatws2	⊢ ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) = ( 𝑊 ++ ⟨“ 𝑋 𝑌 ”⟩ ) )
2	1	fveq1d	⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝐼 ) = ( ( 𝑊 ++ ⟨“ 𝑋 𝑌 ”⟩ ) ‘ 𝐼 ) )
3	2	3ad2ant1	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝐼 ) = ( ( 𝑊 ++ ⟨“ 𝑋 𝑌 ”⟩ ) ‘ 𝐼 ) )
4		simp1	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 𝑊 ∈ Word 𝑉 )
5		s2cli	⊢ ⟨“ 𝑋 𝑌 ”⟩ ∈ Word V
6	5	a1i	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ⟨“ 𝑋 𝑌 ”⟩ ∈ Word V )
7		simp2	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 𝐼 ∈ ℕ0 )
8		lencl	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
9	8	nn0zd	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
10	9	3ad2ant1	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℤ )
11		simp3	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 𝐼 < ( ♯ ‘ 𝑊 ) )
12		elfzo0z	⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) )
13	7 10 11 12	syl3anbrc	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
14		ccatval1	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑋 𝑌 ”⟩ ∈ Word V ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 𝑌 ”⟩ ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) )
15	4 6 13 14	syl3anc	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 𝑌 ”⟩ ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) )
16	3 15	eqtrd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) )