Theorem ccat2s1fvwALTOLD

Description: Obsolete version of ccat2s1fvwALT as of 28-Jan-2024. Alternate proof of ccat2s1fvwOLD 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) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 𝑊 ∈ Word 𝑉 )
2	1	anim1i	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) )
3		3anass	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) )
4	2 3	sylibr	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) )
5		ccatw2s1ccatws2OLD	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) = ( 𝑊 ++ ⟨“ 𝑋 𝑌 ”⟩ ) )
6	5	fveq1d	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝐼 ) = ( ( 𝑊 ++ ⟨“ 𝑋 𝑌 ”⟩ ) ‘ 𝐼 ) )
7	4 6	syl	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝐼 ) = ( ( 𝑊 ++ ⟨“ 𝑋 𝑌 ”⟩ ) ‘ 𝐼 ) )
8	1	adantr	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝑊 ∈ Word 𝑉 )
9		s2cl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ⟨“ 𝑋 𝑌 ”⟩ ∈ Word 𝑉 )
10	9	adantl	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ⟨“ 𝑋 𝑌 ”⟩ ∈ Word 𝑉 )
11		simp2	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 𝐼 ∈ ℕ0 )
12		lencl	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
13	12	nn0zd	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
14	13	3ad2ant1	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℤ )
15		simp3	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 𝐼 < ( ♯ ‘ 𝑊 ) )
16		elfzo0z	⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) )
17	11 14 15 16	syl3anbrc	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
18	17	adantr	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
19		ccatval1	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑋 𝑌 ”⟩ ∈ Word 𝑉 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 𝑌 ”⟩ ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) )
20	8 10 18 19	syl3anc	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 𝑌 ”⟩ ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) )
21	7 20	eqtrd	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) )